Global Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(54001 entries)

Notation Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(1931 entries)

Module Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(1658 entries)

Variable Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(7199 entries)

Library Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(97 entries)

Lemma Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(15214 entries)

Axiom Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(75 entries)

Constructor Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(224 entries)

Inductive Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(132 entries)

Projection Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(2371 entries)

Section Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(2266 entries)

Abbreviation Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(732 entries)

Definition Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(21455 entries)

Record Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(647 entries)

---

R

r [abbreviation, in mathcomp.character.mxabelem]
R [abbreviation, in mathcomp.field.finfield]
R [abbreviation, in mathcomp.field.finfield]
ract [definition, in mathcomp.fingroup.action]
ractE [lemma, in mathcomp.fingroup.action]
raction [definition, in mathcomp.fingroup.action]
ractpermE [lemma, in mathcomp.fingroup.action]
ract_groupAction [definition, in mathcomp.fingroup.action]
ract_is_groupAction [lemma, in mathcomp.fingroup.action]
ract_is_action [lemma, in mathcomp.fingroup.action]
rad [definition, in mathcomp.algebra.sesquilinear]
raddfMz [lemma, in mathcomp.algebra.ssrint]
raddf_int_scalable [lemma, in mathcomp.algebra.ssrint]
radmx [abbreviation, in mathcomp.algebra.sesquilinear]
radmxE [lemma, in mathcomp.algebra.sesquilinear]
radv [abbreviation, in mathcomp.algebra.sesquilinear]
rad_ker [lemma, in mathcomp.algebra.sesquilinear]
range [abbreviation, in mathcomp.fingroup.action]
rank [definition, in mathcomp.solvable.abelian]
rankJ [lemma, in mathcomp.solvable.abelian]
rankS [lemma, in mathcomp.solvable.abelian]
rank_mx_group [lemma, in mathcomp.character.mxabelem]
rank_Wedderburn_subring [lemma, in mathcomp.character.mxrepresentation]
rank_irr_comp [lemma, in mathcomp.character.mxrepresentation]
rank_irr1 [lemma, in mathcomp.character.mxrepresentation]
rank_cycle [lemma, in mathcomp.solvable.abelian]
rank_abelian_pgroup [lemma, in mathcomp.solvable.abelian]
rank_Ohm1 [lemma, in mathcomp.solvable.abelian]
rank_geP [lemma, in mathcomp.solvable.abelian]
rank_abelem [lemma, in mathcomp.solvable.abelian]
rank_Sylow [lemma, in mathcomp.solvable.abelian]
rank_pgroup [lemma, in mathcomp.solvable.abelian]
rank_witness [lemma, in mathcomp.solvable.abelian]
rank_gt0 [lemma, in mathcomp.solvable.abelian]
rank_ortho [lemma, in mathcomp.algebra.spectral]
rank_DnQ [lemma, in mathcomp.solvable.extraspecial]
rank_Dn [lemma, in mathcomp.solvable.extraspecial]
rank_orthomx [lemma, in mathcomp.algebra.sesquilinear]
rank_normal [lemma, in mathcomp.algebra.sesquilinear]
rank_mxdiag [lemma, in mathcomp.algebra.mxalgebra]
rank_diag_block_mx [lemma, in mathcomp.algebra.mxalgebra]
rank_row_0mx [lemma, in mathcomp.algebra.mxalgebra]
rank_row_mx0 [lemma, in mathcomp.algebra.mxalgebra]
rank_col_0mx [lemma, in mathcomp.algebra.mxalgebra]
rank_col_mx0 [lemma, in mathcomp.algebra.mxalgebra]
rank_copid_mx [lemma, in mathcomp.algebra.mxalgebra]
rank_pid_mx [lemma, in mathcomp.algebra.mxalgebra]
rank_ltmx [lemma, in mathcomp.algebra.mxalgebra]
rank_rV [lemma, in mathcomp.algebra.mxalgebra]
rank_leq_col [lemma, in mathcomp.algebra.mxalgebra]
rank_leq_row [lemma, in mathcomp.algebra.mxalgebra]
rank1 [lemma, in mathcomp.solvable.abelian]
rat [record, in mathcomp.algebra.rat]
rat [library]
ratArchimedean [module, in mathcomp.algebra.rat]
ratArchimedean.is_intE [lemma, in mathcomp.algebra.rat]
ratArchimedean.is_natE [lemma, in mathcomp.algebra.rat]
ratArchimedean.ratArchimedean [section, in mathcomp.algebra.rat]
ratArchimedean.ratArchimedean.is_nat [variable, in mathcomp.algebra.rat]
ratArchimedean.ratArchimedean.trunc [variable, in mathcomp.algebra.rat]
ratArchimedean.truncP [lemma, in mathcomp.algebra.rat]
ratCK [lemma, in mathcomp.field.algC]
Ratio [definition, in mathcomp.algebra.fraction]
ratio [record, in mathcomp.algebra.fraction]
RatioNonNull [constructor, in mathcomp.algebra.fraction]
RatioNull [constructor, in mathcomp.algebra.fraction]
RatioP [lemma, in mathcomp.algebra.fraction]
Ratio_numden [lemma, in mathcomp.algebra.fraction]
Ratio_spec [inductive, in mathcomp.algebra.fraction]
ratio_sind [definition, in mathcomp.algebra.fraction]
ratio_rec [definition, in mathcomp.algebra.fraction]
ratio_ind [definition, in mathcomp.algebra.fraction]
ratio_rect [definition, in mathcomp.algebra.fraction]
Ratio0 [lemma, in mathcomp.algebra.fraction]
ratio0 [definition, in mathcomp.algebra.fraction]
RatK [lemma, in mathcomp.algebra.rat]
ratP [lemma, in mathcomp.algebra.rat]
ratr [definition, in mathcomp.algebra.rat]
ratr_norm [lemma, in mathcomp.algebra.rat]
ratr_sg [lemma, in mathcomp.algebra.rat]
ratr_is_multiplicative [lemma, in mathcomp.algebra.rat]
ratr_is_additive [lemma, in mathcomp.algebra.rat]
ratr_nat [lemma, in mathcomp.algebra.rat]
ratr_int [lemma, in mathcomp.algebra.rat]
ratz [definition, in mathcomp.algebra.rat]
ratzD [lemma, in mathcomp.algebra.rat]
ratzE [lemma, in mathcomp.algebra.rat]
ratzM [lemma, in mathcomp.algebra.rat]
ratzN [lemma, in mathcomp.algebra.rat]
ratz_frac [lemma, in mathcomp.algebra.rat]
rat_poly_scale [lemma, in mathcomp.algebra.intdiv]
rat_algebraic_decidable [lemma, in mathcomp.field.algebraics_fundamentals]
rat_algebraic_archimedean [lemma, in mathcomp.field.algebraics_fundamentals]
rat_vm_compute [lemma, in mathcomp.algebra.rat]
rat_field_theory [lemma, in mathcomp.algebra.rat]
rat_ring_theory [lemma, in mathcomp.algebra.rat]
rat_ratr__canonical__GRing_RMorphism [definition, in mathcomp.algebra.rat]
rat_ratr__canonical__GRing_Additive [definition, in mathcomp.algebra.rat]
rat_linear [lemma, in mathcomp.algebra.rat]
rat_rat__canonical__Num_ArchiRealField [definition, in mathcomp.algebra.rat]
rat_rat__canonical__Num_ArchiNumField [definition, in mathcomp.algebra.rat]
rat_rat__canonical__Num_ArchiRealDomain [definition, in mathcomp.algebra.rat]
rat_rat__canonical__Num_ArchiNumDomain [definition, in mathcomp.algebra.rat]
rat_rat__canonical__Num_RealField [definition, in mathcomp.algebra.rat]
rat_rat__canonical__Num_NumField [definition, in mathcomp.algebra.rat]
rat_rat__canonical__Num_RealDomain [definition, in mathcomp.algebra.rat]
rat_rat__canonical__Num_NumDomain [definition, in mathcomp.algebra.rat]
rat_rat__canonical__Num_NormedZmodule [definition, in mathcomp.algebra.rat]
rat_rat__canonical__Order_Total [definition, in mathcomp.algebra.rat]
rat_rat__canonical__Order_DistrLattice [definition, in mathcomp.algebra.rat]
rat_rat__canonical__Order_Lattice [definition, in mathcomp.algebra.rat]
rat_rat__canonical__Order_MeetSemilattice [definition, in mathcomp.algebra.rat]
rat_rat__canonical__Order_JoinSemilattice [definition, in mathcomp.algebra.rat]
rat_rat__canonical__Num_POrderedZmodule [definition, in mathcomp.algebra.rat]
rat_rat__canonical__Order_POrder [definition, in mathcomp.algebra.rat]
Rat_spec [constructor, in mathcomp.algebra.rat]
rat_spec [inductive, in mathcomp.algebra.rat]
rat_rat__canonical__CountRing_Field [definition, in mathcomp.algebra.rat]
rat_rat__canonical__GRing_Field [definition, in mathcomp.algebra.rat]
rat_rat__canonical__CountRing_IntegralDomain [definition, in mathcomp.algebra.rat]
rat_rat__canonical__GRing_IntegralDomain [definition, in mathcomp.algebra.rat]
rat_rat__canonical__CountRing_ComUnitRing [definition, in mathcomp.algebra.rat]
rat_rat__canonical__GRing_ComUnitRing [definition, in mathcomp.algebra.rat]
rat_rat__canonical__CountRing_UnitRing [definition, in mathcomp.algebra.rat]
rat_rat__canonical__GRing_UnitRing [definition, in mathcomp.algebra.rat]
rat_rat__canonical__CountRing_ComRing [definition, in mathcomp.algebra.rat]
rat_rat__canonical__GRing_ComRing [definition, in mathcomp.algebra.rat]
rat_rat__canonical__CountRing_ComSemiRing [definition, in mathcomp.algebra.rat]
rat_rat__canonical__GRing_ComSemiRing [definition, in mathcomp.algebra.rat]
rat_rat__canonical__CountRing_Ring [definition, in mathcomp.algebra.rat]
rat_rat__canonical__GRing_Ring [definition, in mathcomp.algebra.rat]
rat_rat__canonical__CountRing_SemiRing [definition, in mathcomp.algebra.rat]
rat_rat__canonical__GRing_SemiRing [definition, in mathcomp.algebra.rat]
rat_rat__canonical__CountRing_Zmodule [definition, in mathcomp.algebra.rat]
rat_rat__canonical__GRing_Zmodule [definition, in mathcomp.algebra.rat]
rat_rat__canonical__CountRing_Nmodule [definition, in mathcomp.algebra.rat]
rat_rat__canonical__GRing_Nmodule [definition, in mathcomp.algebra.rat]
rat_eq [lemma, in mathcomp.algebra.rat]
rat_eqE [lemma, in mathcomp.algebra.rat]
rat_rat__canonical__choice_SubCountable [definition, in mathcomp.algebra.rat]
rat_rat__canonical__choice_Countable [definition, in mathcomp.algebra.rat]
rat_rat__canonical__choice_SubChoice [definition, in mathcomp.algebra.rat]
rat_rat__canonical__choice_Choice [definition, in mathcomp.algebra.rat]
rat_rat__canonical__eqtype_SubEquality [definition, in mathcomp.algebra.rat]
rat_rat__canonical__eqtype_Equality [definition, in mathcomp.algebra.rat]
rat_rat__canonical__eqtype_SubType [definition, in mathcomp.algebra.rat]
rat_isSub [definition, in mathcomp.algebra.rat]
rat0 [lemma, in mathcomp.algebra.rat]
rat1 [lemma, in mathcomp.algebra.rat]
RawAction [section, in mathcomp.fingroup.action]
RawAction.ActsSetop [section, in mathcomp.fingroup.action]
RawAction.ActsSetop.A [variable, in mathcomp.fingroup.action]
RawAction.ActsSetop.AactS [variable, in mathcomp.fingroup.action]
RawAction.ActsSetop.AactT [variable, in mathcomp.fingroup.action]
RawAction.ActsSetop.S [variable, in mathcomp.fingroup.action]
RawAction.ActsSetop.T [variable, in mathcomp.fingroup.action]
RawAction.aT [variable, in mathcomp.fingroup.action]
RawAction.D [variable, in mathcomp.fingroup.action]
RawAction.Reindex [section, in mathcomp.fingroup.action]
RawAction.Reindex.idx [variable, in mathcomp.fingroup.action]
RawAction.Reindex.op [variable, in mathcomp.fingroup.action]
RawAction.Reindex.S [variable, in mathcomp.fingroup.action]
RawAction.Reindex.vT [variable, in mathcomp.fingroup.action]
RawAction.rT [variable, in mathcomp.fingroup.action]
RawAction.to [variable, in mathcomp.fingroup.action]
RawGroupAction [section, in mathcomp.fingroup.action]
RawGroupAction.A [variable, in mathcomp.fingroup.action]
RawGroupAction.a [variable, in mathcomp.fingroup.action]
RawGroupAction.aT [variable, in mathcomp.fingroup.action]
RawGroupAction.B [variable, in mathcomp.fingroup.action]
RawGroupAction.D [variable, in mathcomp.fingroup.action]
RawGroupAction.Da [variable, in mathcomp.fingroup.action]
RawGroupAction.R [variable, in mathcomp.fingroup.action]
RawGroupAction.rT [variable, in mathcomp.fingroup.action]
RawGroupAction.S [variable, in mathcomp.fingroup.action]
RawGroupAction.sAD [variable, in mathcomp.fingroup.action]
RawGroupAction.sSR [variable, in mathcomp.fingroup.action]
RawGroupAction.to [variable, in mathcomp.fingroup.action]
rcent [definition, in mathcomp.character.mxrepresentation]
rcenter [definition, in mathcomp.character.mxrepresentation]
rcenter_normal [lemma, in mathcomp.character.mxrepresentation]
rcenter_group [definition, in mathcomp.character.mxrepresentation]
rcenter_group_set [lemma, in mathcomp.character.mxrepresentation]
rcent_map [lemma, in mathcomp.character.mxrepresentation]
rcent_quo [lemma, in mathcomp.character.mxrepresentation]
rcent_conj [lemma, in mathcomp.character.mxrepresentation]
rcent_eqg [lemma, in mathcomp.character.mxrepresentation]
rcent_subg [lemma, in mathcomp.character.mxrepresentation]
rcent_group [definition, in mathcomp.character.mxrepresentation]
rcent_group_set [lemma, in mathcomp.character.mxrepresentation]
rcent_sub [lemma, in mathcomp.character.mxrepresentation]
rconj_mxJ [lemma, in mathcomp.character.mxrepresentation]
rconj_mxE [lemma, in mathcomp.character.mxrepresentation]
rconj_repr [definition, in mathcomp.character.mxrepresentation]
rconj_mx_repr [lemma, in mathcomp.character.mxrepresentation]
rconj_mx [definition, in mathcomp.character.mxrepresentation]
rcons [definition, in mathcomp.ssreflect.seq]
rcons_bseq [definition, in mathcomp.ssreflect.tuple]
rcons_bseqP [lemma, in mathcomp.ssreflect.tuple]
rcons_tuple [definition, in mathcomp.ssreflect.tuple]
rcons_tupleP [lemma, in mathcomp.ssreflect.tuple]
rcons_uniq [lemma, in mathcomp.ssreflect.seq]
rcons_injr [lemma, in mathcomp.ssreflect.seq]
rcons_injl [lemma, in mathcomp.ssreflect.seq]
rcons_inj [lemma, in mathcomp.ssreflect.seq]
rcons_cat [lemma, in mathcomp.ssreflect.seq]
rcons_cons [lemma, in mathcomp.ssreflect.seq]
rcons_path [lemma, in mathcomp.ssreflect.path]
rcons2_infix [lemma, in mathcomp.ssreflect.seq]
rcoset [definition, in mathcomp.fingroup.fingroup]
rcosetE [lemma, in mathcomp.fingroup.fingroup]
rcosetK [lemma, in mathcomp.fingroup.fingroup]
rcosetKV [lemma, in mathcomp.fingroup.fingroup]
rcosetM [lemma, in mathcomp.fingroup.fingroup]
rcosetP [lemma, in mathcomp.fingroup.fingroup]
RcosetReprSpec [constructor, in mathcomp.fingroup.fingroup]
rcosetS [lemma, in mathcomp.fingroup.fingroup]
rcosets [definition, in mathcomp.fingroup.fingroup]
rcosetsP [lemma, in mathcomp.fingroup.fingroup]
rcosets_cycle_transversal [lemma, in mathcomp.solvable.finmodule]
rcosets_cycle_partition [lemma, in mathcomp.solvable.finmodule]
rcosets_partition [lemma, in mathcomp.fingroup.fingroup]
rcosets_partition_mul [lemma, in mathcomp.fingroup.fingroup]
rcosets_id [lemma, in mathcomp.fingroup.fingroup]
rcoset_kercosetP [lemma, in mathcomp.fingroup.quotient]
rcoset_action [definition, in mathcomp.fingroup.action]
rcoset_is_action [lemma, in mathcomp.fingroup.action]
rcoset_index2 [lemma, in mathcomp.fingroup.fingroup]
rcoset_mul [lemma, in mathcomp.fingroup.fingroup]
rcoset_repr [lemma, in mathcomp.fingroup.fingroup]
rcoset_repr_spec [inductive, in mathcomp.fingroup.fingroup]
rcoset_id [lemma, in mathcomp.fingroup.fingroup]
rcoset_trans [lemma, in mathcomp.fingroup.fingroup]
rcoset_transl [lemma, in mathcomp.fingroup.fingroup]
rcoset_eqP [lemma, in mathcomp.fingroup.fingroup]
rcoset_sym [lemma, in mathcomp.fingroup.fingroup]
rcoset_refl [lemma, in mathcomp.fingroup.fingroup]
rcoset_inj [lemma, in mathcomp.fingroup.fingroup]
rcoset_kerP [lemma, in mathcomp.fingroup.morphism]
rcoset1 [lemma, in mathcomp.fingroup.fingroup]
rdegree [projection, in mathcomp.character.character]
realmx [section, in mathcomp.algebra.spectral]
realmx [abbreviation, in mathcomp.algebra.spectral]
realmxC [lemma, in mathcomp.algebra.spectral]
realmxD [lemma, in mathcomp.algebra.spectral]
realsym_hermsym [lemma, in mathcomp.algebra.spectral]
realz [lemma, in mathcomp.algebra.ssrint]
real_similar [lemma, in mathcomp.algebra.spectral]
reducebig [definition, in mathcomp.ssreflect.bigop]
reducible_Socle1 [lemma, in mathcomp.character.mxrepresentation]
reducible_Socle [lemma, in mathcomp.character.mxrepresentation]
RefBaseField [section, in mathcomp.field.fieldext]
refBaseField [module, in mathcomp.field.fieldext]
refBaseField_unlockable [definition, in mathcomp.field.fieldext]
refBaseField_unlock_subterm [definition, in mathcomp.field.fieldext]
refBaseField_Locked.unlock [axiom, in mathcomp.field.fieldext]
refBaseField_Locked.body [axiom, in mathcomp.field.fieldext]
refBaseField_Locked [module, in mathcomp.field.fieldext]
RefBaseField.bF [variable, in mathcomp.field.fieldext]
refBaseField.body [definition, in mathcomp.field.fieldext]
RefBaseField.coordF [variable, in mathcomp.field.fieldext]
RefBaseField.F [variable, in mathcomp.field.fieldext]
RefBaseField.F0 [variable, in mathcomp.field.fieldext]
RefBaseField.L [variable, in mathcomp.field.fieldext]
RefBaseField.n [variable, in mathcomp.field.fieldext]
refBaseField.unlock [definition, in mathcomp.field.fieldext]
ReflectProp [section, in mathcomp.fingroup.morphism]
ReflectProp.aT [variable, in mathcomp.fingroup.morphism]
ReflectProp.Defs [section, in mathcomp.fingroup.morphism]
ReflectProp.Defs.A [variable, in mathcomp.fingroup.morphism]
ReflectProp.Defs.B [variable, in mathcomp.fingroup.morphism]
ReflectProp.Defs.MorphicProps [section, in mathcomp.fingroup.morphism]
ReflectProp.Defs.MorphicProps.f [variable, in mathcomp.fingroup.morphism]
ReflectProp.f [variable, in mathcomp.fingroup.morphism]
ReflectProp.G [variable, in mathcomp.fingroup.morphism]
ReflectProp.Main [section, in mathcomp.fingroup.morphism]
ReflectProp.Main.f [variable, in mathcomp.fingroup.morphism]
ReflectProp.Main.G [variable, in mathcomp.fingroup.morphism]
ReflectProp.Main.H [variable, in mathcomp.fingroup.morphism]
ReflectProp.Main.isoGH [variable, in mathcomp.fingroup.morphism]
ReflectProp.rT [variable, in mathcomp.fingroup.morphism]
_ \isog _ [notation, in mathcomp.fingroup.morphism]
RegularVectType [section, in mathcomp.algebra.vector]
RegularVectType.R [variable, in mathcomp.algebra.vector]
regular_splittingAxiom [lemma, in mathcomp.field.galois]
regular_norm_coprime [lemma, in mathcomp.solvable.frobenius]
regular_norm_dvd_pred [lemma, in mathcomp.solvable.frobenius]
regular_op_inj [lemma, in mathcomp.character.mxrepresentation]
regular_module_ideal [lemma, in mathcomp.character.mxrepresentation]
regular_mx_faithful [lemma, in mathcomp.character.mxrepresentation]
regular_repr [definition, in mathcomp.character.mxrepresentation]
regular_mx_repr [lemma, in mathcomp.character.mxrepresentation]
regular_mx [definition, in mathcomp.character.mxrepresentation]
regular_vect_iso [lemma, in mathcomp.algebra.vector]
regular_fullv [lemma, in mathcomp.field.falgebra]
reindex [lemma, in mathcomp.ssreflect.bigop]
reindex_perm [abbreviation, in mathcomp.fingroup.perm]
reindex_cfclass [lemma, in mathcomp.character.inertia]
reindex_acts [lemma, in mathcomp.fingroup.action]
reindex_astabs [lemma, in mathcomp.fingroup.action]
reindex_dprod [lemma, in mathcomp.character.classfun]
reindex_bigcprod [lemma, in mathcomp.fingroup.gproduct]
reindex_irr_class [lemma, in mathcomp.character.character]
reindex_inj [lemma, in mathcomp.ssreflect.bigop]
reindex_onto [lemma, in mathcomp.ssreflect.bigop]
reindex_omap [lemma, in mathcomp.ssreflect.bigop]
RelAdjunction [section, in mathcomp.ssreflect.fingraph]
RelAdjunction.a [variable, in mathcomp.ssreflect.fingraph]
RelAdjunction.ccl_a [variable, in mathcomp.ssreflect.fingraph]
RelAdjunction.cl_a [variable, in mathcomp.ssreflect.fingraph]
RelAdjunction.e [variable, in mathcomp.ssreflect.fingraph]
RelAdjunction.e' [variable, in mathcomp.ssreflect.fingraph]
RelAdjunction.h [variable, in mathcomp.ssreflect.fingraph]
RelAdjunction.sym_e' [variable, in mathcomp.ssreflect.fingraph]
RelAdjunction.sym_e [variable, in mathcomp.ssreflect.fingraph]
RelAdjunction.T [variable, in mathcomp.ssreflect.fingraph]
RelAdjunction.T' [variable, in mathcomp.ssreflect.fingraph]
relpre_trans [lemma, in mathcomp.ssreflect.ssrbool]
relU_sym [lemma, in mathcomp.ssreflect.fingraph]
rel_base [definition, in mathcomp.ssreflect.path]
rel_adjunction [abbreviation, in mathcomp.ssreflect.fingraph]
rel_adjunction [abbreviation, in mathcomp.ssreflect.fingraph]
rel_functor [projection, in mathcomp.ssreflect.fingraph]
rel_unit [projection, in mathcomp.ssreflect.fingraph]
rel_adjunction_mem [record, in mathcomp.ssreflect.fingraph]
rem [definition, in mathcomp.ssreflect.seq]
Rem [section, in mathcomp.ssreflect.seq]
remE [lemma, in mathcomp.ssreflect.seq]
remgr [definition, in mathcomp.fingroup.gproduct]
remgrM [lemma, in mathcomp.fingroup.gproduct]
remgrMid [lemma, in mathcomp.fingroup.gproduct]
remgrMl [lemma, in mathcomp.fingroup.gproduct]
remgrP [lemma, in mathcomp.fingroup.gproduct]
remgr_id [lemma, in mathcomp.fingroup.gproduct]
remgr1 [lemma, in mathcomp.fingroup.gproduct]
Remx_rect [lemma, in mathcomp.algebra.spectral]
rem_filter [lemma, in mathcomp.ssreflect.seq]
rem_mem [lemma, in mathcomp.ssreflect.seq]
rem_uniq [lemma, in mathcomp.ssreflect.seq]
rem_subseq [lemma, in mathcomp.ssreflect.seq]
rem_id [lemma, in mathcomp.ssreflect.seq]
rem_cons [lemma, in mathcomp.ssreflect.seq]
Rem.T [variable, in mathcomp.ssreflect.seq]
Rem.x [variable, in mathcomp.ssreflect.seq]
repr [module, in mathcomp.ssreflect.generic_quotient]
repr [definition, in mathcomp.fingroup.fingroup]
Repr [section, in mathcomp.fingroup.fingroup]
representation [record, in mathcomp.character.character]
reprG [abbreviation, in mathcomp.character.mxrepresentation]
reprG [abbreviation, in mathcomp.character.character]
reprG [abbreviation, in mathcomp.character.character]
reprGLm [definition, in mathcomp.character.mxabelem]
reprGLmM [lemma, in mathcomp.character.mxabelem]
reprGL_morphism [definition, in mathcomp.character.mxabelem]
reprK [lemma, in mathcomp.ssreflect.generic_quotient]
repr_coset_norm [lemma, in mathcomp.fingroup.quotient]
repr_coset1 [lemma, in mathcomp.fingroup.quotient]
repr_unlock [definition, in mathcomp.ssreflect.generic_quotient]
repr_unlock_subterm [definition, in mathcomp.ssreflect.generic_quotient]
repr_Locked.unlock [axiom, in mathcomp.ssreflect.generic_quotient]
repr_Locked.body [axiom, in mathcomp.ssreflect.generic_quotient]
repr_Locked [module, in mathcomp.ssreflect.generic_quotient]
repr_ofK [lemma, in mathcomp.ssreflect.generic_quotient]
repr_ofK_subproof [definition, in mathcomp.ssreflect.generic_quotient]
repr_of [definition, in mathcomp.ssreflect.generic_quotient]
repr_mem_transversal [lemma, in mathcomp.ssreflect.finset]
repr_mem_pblock [lemma, in mathcomp.ssreflect.finset]
repr_classesP [lemma, in mathcomp.fingroup.fingroup]
repr_class [lemma, in mathcomp.fingroup.fingroup]
repr_rcosetP [lemma, in mathcomp.fingroup.fingroup]
repr_group [lemma, in mathcomp.fingroup.fingroup]
repr_set0 [lemma, in mathcomp.fingroup.fingroup]
repr_set1 [lemma, in mathcomp.fingroup.fingroup]
repr_mx_free [lemma, in mathcomp.character.mxrepresentation]
repr_mxX [lemma, in mathcomp.character.mxrepresentation]
repr_mx_unitr [lemma, in mathcomp.character.mxrepresentation]
repr_mxVr [lemma, in mathcomp.character.mxrepresentation]
repr_mxMr [lemma, in mathcomp.character.mxrepresentation]
repr_mxV [lemma, in mathcomp.character.mxrepresentation]
repr_mx_unit [lemma, in mathcomp.character.mxrepresentation]
repr_mxKV [lemma, in mathcomp.character.mxrepresentation]
repr_mxK [lemma, in mathcomp.character.mxrepresentation]
repr_mxM [lemma, in mathcomp.character.mxrepresentation]
repr_mx1 [lemma, in mathcomp.character.mxrepresentation]
repr_mx [projection, in mathcomp.character.mxrepresentation]
repr_irr_classK [lemma, in mathcomp.character.character]
repr_rsim_diag [lemma, in mathcomp.character.character]
repr.body [definition, in mathcomp.ssreflect.generic_quotient]
Repr.gT [variable, in mathcomp.fingroup.fingroup]
repr.unlock [definition, in mathcomp.ssreflect.generic_quotient]
reshape [definition, in mathcomp.ssreflect.seq]
reshapeKl [lemma, in mathcomp.ssreflect.seq]
reshapeKr [lemma, in mathcomp.ssreflect.seq]
reshape_leq [lemma, in mathcomp.ssreflect.seq]
reshape_indexK [lemma, in mathcomp.ssreflect.seq]
reshape_offsetP [lemma, in mathcomp.ssreflect.seq]
reshape_indexP [lemma, in mathcomp.ssreflect.seq]
reshape_rcons [lemma, in mathcomp.ssreflect.seq]
reshape_offset [definition, in mathcomp.ssreflect.seq]
reshape_index [definition, in mathcomp.ssreflect.seq]
resize_mask [lemma, in mathcomp.ssreflect.seq]
Restrict [section, in mathcomp.solvable.alt]
Restrict [section, in mathcomp.fingroup.action]
Restrict [section, in mathcomp.character.classfun]
Restrict [section, in mathcomp.character.character]
RestrictActionTheory [section, in mathcomp.fingroup.action]
RestrictActionTheory.A [variable, in mathcomp.fingroup.action]
RestrictActionTheory.aT [variable, in mathcomp.fingroup.action]
RestrictActionTheory.D [variable, in mathcomp.fingroup.action]
RestrictActionTheory.rT [variable, in mathcomp.fingroup.action]
RestrictActionTheory.sAD [variable, in mathcomp.fingroup.action]
RestrictActionTheory.to [variable, in mathcomp.fingroup.action]
RestrictedMorphism [section, in mathcomp.fingroup.morphism]
RestrictedMorphism.A [variable, in mathcomp.fingroup.morphism]
RestrictedMorphism.aT [variable, in mathcomp.fingroup.morphism]
RestrictedMorphism.D [variable, in mathcomp.fingroup.morphism]
RestrictedMorphism.Props [section, in mathcomp.fingroup.morphism]
RestrictedMorphism.Props.f [variable, in mathcomp.fingroup.morphism]
RestrictedMorphism.Props.sAD [variable, in mathcomp.fingroup.morphism]
RestrictedMorphism.rT [variable, in mathcomp.fingroup.morphism]
restrictmx [abbreviation, in mathcomp.algebra.mxpoly]
restrictmx [abbreviation, in mathcomp.algebra.mxpoly]
restrictmx [abbreviation, in mathcomp.algebra.mxred]
restrictmx [abbreviation, in mathcomp.algebra.mxred]
RestrictPerm [section, in mathcomp.fingroup.action]
RestrictPerm.S [variable, in mathcomp.fingroup.action]
RestrictPerm.T [variable, in mathcomp.fingroup.action]
restrict_aut_to_normal_num_field [lemma, in mathcomp.field.algnum]
restrict_aut_to_num_field [lemma, in mathcomp.field.algnum]
Restrict.A [variable, in mathcomp.fingroup.action]
Restrict.A [variable, in mathcomp.character.classfun]
Restrict.aT [variable, in mathcomp.fingroup.action]
Restrict.B [variable, in mathcomp.character.classfun]
Restrict.card_T [variable, in mathcomp.solvable.alt]
Restrict.D [variable, in mathcomp.fingroup.action]
Restrict.G [variable, in mathcomp.character.character]
Restrict.gT [variable, in mathcomp.character.classfun]
Restrict.gT [variable, in mathcomp.character.character]
Restrict.H [variable, in mathcomp.character.character]
Restrict.rT [variable, in mathcomp.fingroup.action]
Restrict.sAD [variable, in mathcomp.fingroup.action]
Restrict.T [variable, in mathcomp.solvable.alt]
Restrict.to [variable, in mathcomp.fingroup.action]
Restrict.x [variable, in mathcomp.solvable.alt]
restrm [definition, in mathcomp.fingroup.morphism]
restrmEsub [lemma, in mathcomp.fingroup.morphism]
restrmP [lemma, in mathcomp.fingroup.morphism]
restrm_quotientE [lemma, in mathcomp.fingroup.quotient]
restrm_morphism [definition, in mathcomp.fingroup.morphism]
restr_perm_isom [lemma, in mathcomp.fingroup.action]
restr_perm_Aut [lemma, in mathcomp.fingroup.action]
restr_perm_commute [lemma, in mathcomp.fingroup.action]
restr_permE [lemma, in mathcomp.fingroup.action]
restr_perm_on [lemma, in mathcomp.fingroup.action]
restr_perm_morphism [definition, in mathcomp.fingroup.action]
restr_perm [definition, in mathcomp.fingroup.action]
restr_isom [lemma, in mathcomp.fingroup.morphism]
restr_isom_to [lemma, in mathcomp.fingroup.morphism]
resultant [definition, in mathcomp.algebra.mxpoly]
Resultant [section, in mathcomp.algebra.mxpoly]
resultant_eq0 [lemma, in mathcomp.algebra.mxpoly]
resultant_in_ideal [lemma, in mathcomp.algebra.mxpoly]
Resultant.dS [variable, in mathcomp.algebra.mxpoly]
Resultant.p [variable, in mathcomp.algebra.mxpoly]
Resultant.q [variable, in mathcomp.algebra.mxpoly]
Resultant.R [variable, in mathcomp.algebra.mxpoly]
Res_sdprod_irr [lemma, in mathcomp.character.character]
Res_Iirr0 [lemma, in mathcomp.character.character]
Res_Iirr [definition, in mathcomp.character.character]
Res_irr_neq0 [lemma, in mathcomp.character.character]
rev [definition, in mathcomp.ssreflect.seq]
revK [lemma, in mathcomp.ssreflect.seq]
rev_bseq [definition, in mathcomp.ssreflect.tuple]
rev_bseqP [lemma, in mathcomp.ssreflect.tuple]
rev_tuple [definition, in mathcomp.ssreflect.tuple]
rev_tupleP [lemma, in mathcomp.ssreflect.tuple]
rev_reshape [lemma, in mathcomp.ssreflect.seq]
rev_flatten [lemma, in mathcomp.ssreflect.seq]
rev_zip [lemma, in mathcomp.ssreflect.seq]
rev_mask [lemma, in mathcomp.ssreflect.seq]
rev_rot [lemma, in mathcomp.ssreflect.seq]
rev_rotr [lemma, in mathcomp.ssreflect.seq]
rev_drop [lemma, in mathcomp.ssreflect.seq]
rev_take [lemma, in mathcomp.ssreflect.seq]
rev_pivot [lemma, in mathcomp.ssreflect.seq]
rev_uniq [lemma, in mathcomp.ssreflect.seq]
rev_nseq [lemma, in mathcomp.ssreflect.seq]
rev_rcons [lemma, in mathcomp.ssreflect.seq]
rev_cat [lemma, in mathcomp.ssreflect.seq]
rev_nilp [lemma, in mathcomp.ssreflect.seq]
rev_cons [lemma, in mathcomp.ssreflect.seq]
rev_sorted [lemma, in mathcomp.ssreflect.path]
rev_cycle [lemma, in mathcomp.ssreflect.path]
rev_path [lemma, in mathcomp.ssreflect.path]
rev_ord_inj [lemma, in mathcomp.ssreflect.fintype]
rev_ordK [lemma, in mathcomp.ssreflect.fintype]
rev_ord [definition, in mathcomp.ssreflect.fintype]
rev_ord_proof [lemma, in mathcomp.ssreflect.fintype]
rev_big_rev [lemma, in mathcomp.ssreflect.bigop]
rfd [definition, in mathcomp.solvable.alt]
rfdP [lemma, in mathcomp.solvable.alt]
rfd_iso [lemma, in mathcomp.solvable.alt]
rfd_odd [lemma, in mathcomp.solvable.alt]
rfd_morphism [definition, in mathcomp.solvable.alt]
rfd_morph [lemma, in mathcomp.solvable.alt]
rfd_fun [definition, in mathcomp.solvable.alt]
rfd_funP [lemma, in mathcomp.solvable.alt]
rfix_pgroup_char [lemma, in mathcomp.character.mxabelem]
rfix_abelem [lemma, in mathcomp.character.mxabelem]
rfix_regular [lemma, in mathcomp.character.mxrepresentation]
rfix_quo [lemma, in mathcomp.character.mxrepresentation]
rfix_conj [lemma, in mathcomp.character.mxrepresentation]
rfix_factmod [lemma, in mathcomp.character.mxrepresentation]
rfix_submod [lemma, in mathcomp.character.mxrepresentation]
rfix_morphim [lemma, in mathcomp.character.mxrepresentation]
rfix_morphpre [lemma, in mathcomp.character.mxrepresentation]
rfix_eqg [lemma, in mathcomp.character.mxrepresentation]
rfix_subg [lemma, in mathcomp.character.mxrepresentation]
rfix_mx_rstabC [lemma, in mathcomp.character.mxrepresentation]
rfix_mx_module [lemma, in mathcomp.character.mxrepresentation]
rfix_mx_conjsg [lemma, in mathcomp.character.mxrepresentation]
rfix_mxS [lemma, in mathcomp.character.mxrepresentation]
rfix_mx_id [lemma, in mathcomp.character.mxrepresentation]
rfix_mxP [lemma, in mathcomp.character.mxrepresentation]
rfix_mx [definition, in mathcomp.character.mxrepresentation]
rG [abbreviation, in mathcomp.character.mxabelem]
rG [abbreviation, in mathcomp.character.mxrepresentation]
rG [abbreviation, in mathcomp.character.mxrepresentation]
rGB [abbreviation, in mathcomp.character.mxrepresentation]
rGB [abbreviation, in mathcomp.character.mxrepresentation]
rgd [definition, in mathcomp.solvable.alt]
rgdP [lemma, in mathcomp.solvable.alt]
rgd_fun [definition, in mathcomp.solvable.alt]
rGf [abbreviation, in mathcomp.character.mxrepresentation]
rGf [abbreviation, in mathcomp.character.mxrepresentation]
rGf [abbreviation, in mathcomp.character.mxrepresentation]
rGf [abbreviation, in mathcomp.character.mxrepresentation]
rGH [abbreviation, in mathcomp.character.mxrepresentation]
rGH [abbreviation, in mathcomp.character.mxrepresentation]
rgraph [definition, in mathcomp.ssreflect.fingraph]
rgraphK [lemma, in mathcomp.ssreflect.fingraph]
rH [abbreviation, in mathcomp.character.mxabelem]
rH [abbreviation, in mathcomp.character.mxrepresentation]
rH [abbreviation, in mathcomp.character.mxrepresentation]
rH [abbreviation, in mathcomp.character.mxrepresentation]
rH [abbreviation, in mathcomp.character.mxrepresentation]
rHG [abbreviation, in mathcomp.character.mxabelem]
right_trans [lemma, in mathcomp.ssreflect.generic_quotient]
right_arc [lemma, in mathcomp.ssreflect.path]
right_mx_ideal [definition, in mathcomp.algebra.mxalgebra]
ringmx_ind [lemma, in mathcomp.algebra.matrix]
ringQuotient [section, in mathcomp.algebra.ring_quotient]
RingQuotient [module, in mathcomp.algebra.ring_quotient]
RingQuotientElpiOperations [module, in mathcomp.algebra.ring_quotient]
ringQuotient.addT [variable, in mathcomp.algebra.ring_quotient]
RingQuotient.axioms_ [record, in mathcomp.algebra.ring_quotient]
RingQuotient.choice_hasChoice_mixin [projection, in mathcomp.algebra.ring_quotient]
RingQuotient.class [projection, in mathcomp.algebra.ring_quotient]
ringQuotient.eqT [variable, in mathcomp.algebra.ring_quotient]
RingQuotient.eqtype_hasDecEq_mixin [projection, in mathcomp.algebra.ring_quotient]
RingQuotient.Exports [module, in mathcomp.algebra.ring_quotient]
RingQuotient.Exports.join_ring_quotient_RingQuotient_between_GRing_Ring_and_ring_quotient_ZmodQuotient [definition, in mathcomp.algebra.ring_quotient]
RingQuotient.Exports.join_ring_quotient_RingQuotient_between_GRing_SemiRing_and_ring_quotient_ZmodQuotient [definition, in mathcomp.algebra.ring_quotient]
RingQuotient.Exports.join_ring_quotient_RingQuotient_between_generic_quotient_EqQuotient_and_GRing_Ring [definition, in mathcomp.algebra.ring_quotient]
RingQuotient.Exports.join_ring_quotient_RingQuotient_between_generic_quotient_EqQuotient_and_GRing_SemiRing [definition, in mathcomp.algebra.ring_quotient]
RingQuotient.Exports.join_ring_quotient_RingQuotient_between_generic_quotient_Quotient_and_GRing_Ring [definition, in mathcomp.algebra.ring_quotient]
RingQuotient.Exports.join_ring_quotient_RingQuotient_between_generic_quotient_Quotient_and_GRing_SemiRing [definition, in mathcomp.algebra.ring_quotient]
RingQuotient.Exports.ring_quotient_RingQuotient__to__GRing_Ring [definition, in mathcomp.algebra.ring_quotient]
RingQuotient.Exports.ring_quotient_RingQuotient_class__to__GRing_Ring_class [definition, in mathcomp.algebra.ring_quotient]
RingQuotient.Exports.ring_quotient_RingQuotient__to__ring_quotient_ZmodQuotient [definition, in mathcomp.algebra.ring_quotient]
RingQuotient.Exports.ring_quotient_RingQuotient_class__to__ring_quotient_ZmodQuotient_class [definition, in mathcomp.algebra.ring_quotient]
RingQuotient.Exports.ring_quotient_RingQuotient__to__GRing_Zmodule [definition, in mathcomp.algebra.ring_quotient]
RingQuotient.Exports.ring_quotient_RingQuotient_class__to__GRing_Zmodule_class [definition, in mathcomp.algebra.ring_quotient]
RingQuotient.Exports.ring_quotient_RingQuotient__to__GRing_SemiRing [definition, in mathcomp.algebra.ring_quotient]
RingQuotient.Exports.ring_quotient_RingQuotient_class__to__GRing_SemiRing_class [definition, in mathcomp.algebra.ring_quotient]
RingQuotient.Exports.ring_quotient_RingQuotient__to__GRing_Nmodule [definition, in mathcomp.algebra.ring_quotient]
RingQuotient.Exports.ring_quotient_RingQuotient_class__to__GRing_Nmodule_class [definition, in mathcomp.algebra.ring_quotient]
RingQuotient.Exports.ring_quotient_RingQuotient__to__choice_Choice [definition, in mathcomp.algebra.ring_quotient]
RingQuotient.Exports.ring_quotient_RingQuotient_class__to__choice_Choice_class [definition, in mathcomp.algebra.ring_quotient]
RingQuotient.Exports.ring_quotient_RingQuotient__to__generic_quotient_EqQuotient [definition, in mathcomp.algebra.ring_quotient]
RingQuotient.Exports.ring_quotient_RingQuotient_class__to__generic_quotient_EqQuotient_class [definition, in mathcomp.algebra.ring_quotient]
RingQuotient.Exports.ring_quotient_RingQuotient__to__eqtype_Equality [definition, in mathcomp.algebra.ring_quotient]
RingQuotient.Exports.ring_quotient_RingQuotient_class__to__eqtype_Equality_class [definition, in mathcomp.algebra.ring_quotient]
RingQuotient.Exports.ring_quotient_RingQuotient__to__generic_quotient_Quotient [definition, in mathcomp.algebra.ring_quotient]
RingQuotient.Exports.ring_quotient_RingQuotient_class__to__generic_quotient_Quotient_class [definition, in mathcomp.algebra.ring_quotient]
RingQuotient.generic_quotient_isEqQuotient_mixin [projection, in mathcomp.algebra.ring_quotient]
RingQuotient.generic_quotient_isQuotient_mixin [projection, in mathcomp.algebra.ring_quotient]
RingQuotient.GRing_Nmodule_isZmodule_mixin [projection, in mathcomp.algebra.ring_quotient]
RingQuotient.GRing_Nmodule_isSemiRing_mixin [projection, in mathcomp.algebra.ring_quotient]
RingQuotient.GRing_isNmodule_mixin [projection, in mathcomp.algebra.ring_quotient]
ringQuotient.mulT [variable, in mathcomp.algebra.ring_quotient]
ringQuotient.oneT [variable, in mathcomp.algebra.ring_quotient]
ringQuotient.oppT [variable, in mathcomp.algebra.ring_quotient]
RingQuotient.pack_ [definition, in mathcomp.algebra.ring_quotient]
RingQuotient.phant_on_ [definition, in mathcomp.algebra.ring_quotient]
RingQuotient.phant_clone [definition, in mathcomp.algebra.ring_quotient]
RingQuotient.ring_quotient_isRingQuotient_mixin [projection, in mathcomp.algebra.ring_quotient]
RingQuotient.ring_quotient_isZmodQuotient_mixin [projection, in mathcomp.algebra.ring_quotient]
RingQuotient.sort [projection, in mathcomp.algebra.ring_quotient]
ringQuotient.T [variable, in mathcomp.algebra.ring_quotient]
RingQuotient.type [record, in mathcomp.algebra.ring_quotient]
ringQuotient.zeroT [variable, in mathcomp.algebra.ring_quotient]
RingRepr [section, in mathcomp.character.mxrepresentation]
RingRepr.ChangeGroup [section, in mathcomp.character.mxrepresentation]
RingRepr.ChangeGroup.G [variable, in mathcomp.character.mxrepresentation]
RingRepr.ChangeGroup.gT [variable, in mathcomp.character.mxrepresentation]
RingRepr.ChangeGroup.H [variable, in mathcomp.character.mxrepresentation]
RingRepr.ChangeGroup.n [variable, in mathcomp.character.mxrepresentation]
RingRepr.ChangeGroup.rG [variable, in mathcomp.character.mxrepresentation]
RingRepr.ChangeGroup.SameGroup [section, in mathcomp.character.mxrepresentation]
RingRepr.ChangeGroup.SameGroup.eqGH [variable, in mathcomp.character.mxrepresentation]
RingRepr.ChangeGroup.SameGroup.Stabiliser [section, in mathcomp.character.mxrepresentation]
RingRepr.ChangeGroup.SameGroup.Stabiliser.m [variable, in mathcomp.character.mxrepresentation]
RingRepr.ChangeGroup.SameGroup.Stabiliser.U [variable, in mathcomp.character.mxrepresentation]
RingRepr.ChangeGroup.SubGroup [section, in mathcomp.character.mxrepresentation]
RingRepr.ChangeGroup.SubGroup.sHG [variable, in mathcomp.character.mxrepresentation]
RingRepr.ChangeGroup.SubGroup.Stabiliser [section, in mathcomp.character.mxrepresentation]
RingRepr.ChangeGroup.SubGroup.Stabiliser.m [variable, in mathcomp.character.mxrepresentation]
RingRepr.ChangeGroup.SubGroup.Stabiliser.U [variable, in mathcomp.character.mxrepresentation]
RingRepr.Conjugate [section, in mathcomp.character.mxrepresentation]
RingRepr.Conjugate.B [variable, in mathcomp.character.mxrepresentation]
RingRepr.Conjugate.G [variable, in mathcomp.character.mxrepresentation]
RingRepr.Conjugate.gT [variable, in mathcomp.character.mxrepresentation]
RingRepr.Conjugate.n [variable, in mathcomp.character.mxrepresentation]
RingRepr.Conjugate.rG [variable, in mathcomp.character.mxrepresentation]
RingRepr.Conjugate.uB [variable, in mathcomp.character.mxrepresentation]
RingRepr.Morphim [section, in mathcomp.character.mxrepresentation]
RingRepr.Morphim.aT [variable, in mathcomp.character.mxrepresentation]
RingRepr.Morphim.D [variable, in mathcomp.character.mxrepresentation]
RingRepr.Morphim.f [variable, in mathcomp.character.mxrepresentation]
RingRepr.Morphim.G [variable, in mathcomp.character.mxrepresentation]
RingRepr.Morphim.n [variable, in mathcomp.character.mxrepresentation]
RingRepr.Morphim.rGf [variable, in mathcomp.character.mxrepresentation]
RingRepr.Morphim.rT [variable, in mathcomp.character.mxrepresentation]
RingRepr.Morphim.sGD [variable, in mathcomp.character.mxrepresentation]
RingRepr.Morphim.sG_f'fG [variable, in mathcomp.character.mxrepresentation]
RingRepr.Morphim.Stabiliser [section, in mathcomp.character.mxrepresentation]
RingRepr.Morphim.Stabiliser.m [variable, in mathcomp.character.mxrepresentation]
RingRepr.Morphim.Stabiliser.U [variable, in mathcomp.character.mxrepresentation]
RingRepr.Morphpre [section, in mathcomp.character.mxrepresentation]
RingRepr.Morphpre.aT [variable, in mathcomp.character.mxrepresentation]
RingRepr.Morphpre.D [variable, in mathcomp.character.mxrepresentation]
RingRepr.Morphpre.f [variable, in mathcomp.character.mxrepresentation]
RingRepr.Morphpre.G [variable, in mathcomp.character.mxrepresentation]
RingRepr.Morphpre.n [variable, in mathcomp.character.mxrepresentation]
RingRepr.Morphpre.rG [variable, in mathcomp.character.mxrepresentation]
RingRepr.Morphpre.rT [variable, in mathcomp.character.mxrepresentation]
RingRepr.Morphpre.Stabiliser [section, in mathcomp.character.mxrepresentation]
RingRepr.Morphpre.Stabiliser.m [variable, in mathcomp.character.mxrepresentation]
RingRepr.Morphpre.Stabiliser.U [variable, in mathcomp.character.mxrepresentation]
RingRepr.OneRepresentation [section, in mathcomp.character.mxrepresentation]
RingRepr.OneRepresentation.CentHom [section, in mathcomp.character.mxrepresentation]
RingRepr.OneRepresentation.CentHom.f [variable, in mathcomp.character.mxrepresentation]
RingRepr.OneRepresentation.G [variable, in mathcomp.character.mxrepresentation]
RingRepr.OneRepresentation.gT [variable, in mathcomp.character.mxrepresentation]
RingRepr.OneRepresentation.n [variable, in mathcomp.character.mxrepresentation]
RingRepr.OneRepresentation.rG [variable, in mathcomp.character.mxrepresentation]
RingRepr.OneRepresentation.Stabiliser [section, in mathcomp.character.mxrepresentation]
RingRepr.OneRepresentation.Stabiliser.m [variable, in mathcomp.character.mxrepresentation]
RingRepr.OneRepresentation.Stabiliser.U [variable, in mathcomp.character.mxrepresentation]
RingRepr.Proper [section, in mathcomp.character.mxrepresentation]
RingRepr.Proper.G [variable, in mathcomp.character.mxrepresentation]
RingRepr.Proper.gT [variable, in mathcomp.character.mxrepresentation]
RingRepr.Proper.n' [variable, in mathcomp.character.mxrepresentation]
RingRepr.Proper.rG [variable, in mathcomp.character.mxrepresentation]
RingRepr.Quotient [section, in mathcomp.character.mxrepresentation]
RingRepr.Quotient.G [variable, in mathcomp.character.mxrepresentation]
RingRepr.Quotient.gT [variable, in mathcomp.character.mxrepresentation]
RingRepr.Quotient.n [variable, in mathcomp.character.mxrepresentation]
RingRepr.Quotient.rG [variable, in mathcomp.character.mxrepresentation]
RingRepr.Quotient.SubQuotient [section, in mathcomp.character.mxrepresentation]
RingRepr.Quotient.SubQuotient.H [variable, in mathcomp.character.mxrepresentation]
RingRepr.Quotient.SubQuotient.krH [variable, in mathcomp.character.mxrepresentation]
RingRepr.Quotient.SubQuotient.nHG [variable, in mathcomp.character.mxrepresentation]
RingRepr.Quotient.SubQuotient.nHGs [variable, in mathcomp.character.mxrepresentation]
RingRepr.R [variable, in mathcomp.character.mxrepresentation]
RingRepr.Regular [section, in mathcomp.character.mxrepresentation]
RingRepr.Regular.G [variable, in mathcomp.character.mxrepresentation]
RingRepr.Regular.GringMx [section, in mathcomp.character.mxrepresentation]
RingRepr.Regular.GringMx.n [variable, in mathcomp.character.mxrepresentation]
RingRepr.Regular.GringMx.rG [variable, in mathcomp.character.mxrepresentation]
RingRepr.Regular.GringOp [section, in mathcomp.character.mxrepresentation]
RingRepr.Regular.GringOp.n [variable, in mathcomp.character.mxrepresentation]
RingRepr.Regular.GringOp.rG [variable, in mathcomp.character.mxrepresentation]
RingRepr.Regular.gT [variable, in mathcomp.character.mxrepresentation]
RingRepr.Regular.hb_instance_6.x [variable, in mathcomp.character.mxrepresentation]
RingRepr.Regular.hb_instance_6.hb_instance_6 [section, in mathcomp.character.mxrepresentation]
ring_display [lemma, in mathcomp.algebra.ssrnum]
ring_quotient [library]
RintMod [section, in mathcomp.algebra.ssrint]
RintMod.R [variable, in mathcomp.algebra.ssrint]
rker [definition, in mathcomp.character.mxrepresentation]
rkerP [lemma, in mathcomp.character.mxrepresentation]
rker_abelem [lemma, in mathcomp.character.mxabelem]
rker_map [lemma, in mathcomp.character.mxrepresentation]
rker_mx_rsim [lemma, in mathcomp.character.mxrepresentation]
rker_factmod [lemma, in mathcomp.character.mxrepresentation]
rker_submod [lemma, in mathcomp.character.mxrepresentation]
rker_quo [lemma, in mathcomp.character.mxrepresentation]
rker_conj [lemma, in mathcomp.character.mxrepresentation]
rker_morphim [lemma, in mathcomp.character.mxrepresentation]
rker_morphpre [lemma, in mathcomp.character.mxrepresentation]
rker_eqg [lemma, in mathcomp.character.mxrepresentation]
rker_subg [lemma, in mathcomp.character.mxrepresentation]
rker_linear [lemma, in mathcomp.character.mxrepresentation]
rker_normal [lemma, in mathcomp.character.mxrepresentation]
rker_norm [lemma, in mathcomp.character.mxrepresentation]
rker_group [definition, in mathcomp.character.mxrepresentation]
rmorphK [lemma, in mathcomp.algebra.sesquilinear]
rmorphMz [lemma, in mathcomp.algebra.ssrint]
rmorphXz [lemma, in mathcomp.algebra.ssrint]
rmorphzP [lemma, in mathcomp.algebra.ssrint]
rmorphZ_num [lemma, in mathcomp.field.algnum]
rmorph_int [lemma, in mathcomp.algebra.ssrint]
rmorph_unity_root [lemma, in mathcomp.algebra.poly]
rmorph_root [lemma, in mathcomp.algebra.poly]
root [definition, in mathcomp.ssreflect.fingraph]
root [definition, in mathcomp.algebra.poly]
rootC [lemma, in mathcomp.algebra.poly]
rootE [lemma, in mathcomp.algebra.poly]
rootM [lemma, in mathcomp.algebra.poly]
rootN [lemma, in mathcomp.algebra.poly]
rootP [lemma, in mathcomp.ssreflect.fingraph]
rootP [lemma, in mathcomp.algebra.poly]
rootPf [lemma, in mathcomp.algebra.poly]
rootPt [lemma, in mathcomp.algebra.poly]
roots [definition, in mathcomp.ssreflect.fingraph]
roots_root [lemma, in mathcomp.ssreflect.fingraph]
roots_pred [definition, in mathcomp.ssreflect.fingraph]
roots_geq_poly_eq0 [lemma, in mathcomp.algebra.poly]
rootX [lemma, in mathcomp.algebra.poly]
rootZ [lemma, in mathcomp.algebra.poly]
root_cyclotomic [lemma, in mathcomp.field.cyclotomic]
root_minPoly_gal [lemma, in mathcomp.field.galois]
root_minCpoly [lemma, in mathcomp.field.algC]
root_small_adjoin_poly [lemma, in mathcomp.field.fieldext]
root_minPoly [lemma, in mathcomp.field.fieldext]
root_mxminpoly [lemma, in mathcomp.algebra.mxpoly]
root_annihilant [lemma, in mathcomp.algebra.polyXY]
root_monic_Aint [lemma, in mathcomp.field.algnum]
root_connect [lemma, in mathcomp.ssreflect.fingraph]
root_root [lemma, in mathcomp.ssreflect.fingraph]
root_ZXsubC [lemma, in mathcomp.algebra.poly]
root_exp_XsubC [lemma, in mathcomp.algebra.poly]
root_prod_XsubC [lemma, in mathcomp.algebra.poly]
root_exp [lemma, in mathcomp.algebra.poly]
root_comp [lemma, in mathcomp.algebra.poly]
root_polyC [lemma, in mathcomp.algebra.poly]
root_of_unity [definition, in mathcomp.algebra.poly]
root_XaddC [lemma, in mathcomp.algebra.poly]
root_XsubC [lemma, in mathcomp.algebra.poly]
root_size_gt1 [lemma, in mathcomp.algebra.poly]
root0 [lemma, in mathcomp.algebra.poly]
root1 [lemma, in mathcomp.algebra.poly]
rot [definition, in mathcomp.ssreflect.seq]
rot [definition, in mathcomp.solvable.burnside_app]
rotations [definition, in mathcomp.solvable.burnside_app]
rotations_group [definition, in mathcomp.solvable.burnside_app]
rotations_is_rot [lemma, in mathcomp.solvable.burnside_app]
RotCompLemmas [section, in mathcomp.ssreflect.seq]
RotCompLemmas.T [variable, in mathcomp.ssreflect.seq]
rotD [lemma, in mathcomp.ssreflect.seq]
RotIndex [section, in mathcomp.ssreflect.seq]
RotIndex.T [variable, in mathcomp.ssreflect.seq]
rotK [lemma, in mathcomp.ssreflect.seq]
rotr [definition, in mathcomp.ssreflect.seq]
RotRcons [section, in mathcomp.ssreflect.seq]
RotRcons.T [variable, in mathcomp.ssreflect.seq]
rotrK [lemma, in mathcomp.ssreflect.seq]
RotrLemmas [section, in mathcomp.ssreflect.seq]
RotrLemmas.n0 [variable, in mathcomp.ssreflect.seq]
RotrLemmas.T [variable, in mathcomp.ssreflect.seq]
RotrLemmas.T' [variable, in mathcomp.ssreflect.seq]
rotr_bseq [definition, in mathcomp.ssreflect.tuple]
rotr_bseqP [lemma, in mathcomp.ssreflect.tuple]
rotr_tuple [definition, in mathcomp.ssreflect.tuple]
rotr_tupleP [lemma, in mathcomp.ssreflect.tuple]
rotr_rotr [lemma, in mathcomp.ssreflect.seq]
rotr_inj [lemma, in mathcomp.ssreflect.seq]
rotr_uniq [lemma, in mathcomp.ssreflect.seq]
rotr_size_cat [lemma, in mathcomp.ssreflect.seq]
rotr_ucycle [lemma, in mathcomp.ssreflect.path]
rotr_cycle [lemma, in mathcomp.ssreflect.path]
rotr1_rcons [lemma, in mathcomp.ssreflect.seq]
rotS [lemma, in mathcomp.ssreflect.seq]
RotToArcSpec [constructor, in mathcomp.ssreflect.path]
RotToSpec [constructor, in mathcomp.ssreflect.seq]
rot_bseq [definition, in mathcomp.ssreflect.tuple]
rot_bseqP [lemma, in mathcomp.ssreflect.tuple]
rot_tuple [definition, in mathcomp.ssreflect.tuple]
rot_tupleP [lemma, in mathcomp.ssreflect.tuple]
rot_rotr [lemma, in mathcomp.ssreflect.seq]
rot_rot [lemma, in mathcomp.ssreflect.seq]
rot_rot_add [lemma, in mathcomp.ssreflect.seq]
rot_addC [lemma, in mathcomp.ssreflect.seq]
rot_add [definition, in mathcomp.ssreflect.seq]
rot_minn [lemma, in mathcomp.ssreflect.seq]
rot_add_mod [lemma, in mathcomp.ssreflect.seq]
rot_to [lemma, in mathcomp.ssreflect.seq]
rot_to_spec [inductive, in mathcomp.ssreflect.seq]
rot_index [lemma, in mathcomp.ssreflect.seq]
rot_uniq [lemma, in mathcomp.ssreflect.seq]
rot_inj [lemma, in mathcomp.ssreflect.seq]
rot_size_cat [lemma, in mathcomp.ssreflect.seq]
rot_size [lemma, in mathcomp.ssreflect.seq]
rot_oversize [lemma, in mathcomp.ssreflect.seq]
rot_to_arc [lemma, in mathcomp.ssreflect.path]
rot_to_arc_spec [inductive, in mathcomp.ssreflect.path]
rot_ucycle [lemma, in mathcomp.ssreflect.path]
rot_cycle [lemma, in mathcomp.ssreflect.path]
rot_is_rot [lemma, in mathcomp.solvable.burnside_app]
rot_r1 [lemma, in mathcomp.solvable.burnside_app]
rot_eq_c0 [lemma, in mathcomp.solvable.burnside_app]
rot_group [definition, in mathcomp.solvable.burnside_app]
rot_inv [definition, in mathcomp.solvable.burnside_app]
rot0 [lemma, in mathcomp.ssreflect.seq]
rot1_cons [lemma, in mathcomp.ssreflect.seq]
row [definition, in mathcomp.algebra.matrix]
RowColDiagBlockMatrix [section, in mathcomp.algebra.mxalgebra]
rowE [lemma, in mathcomp.algebra.matrix]
rowEsub [lemma, in mathcomp.algebra.matrix]
rowg [definition, in mathcomp.character.mxabelem]
rowgD [lemma, in mathcomp.character.mxabelem]
rowgI [lemma, in mathcomp.character.mxabelem]
rowgK [lemma, in mathcomp.character.mxabelem]
rowgS [lemma, in mathcomp.character.mxabelem]
rowg_mxSK [lemma, in mathcomp.character.mxabelem]
rowg_mxK [lemma, in mathcomp.character.mxabelem]
rowg_mx_eq0 [lemma, in mathcomp.character.mxabelem]
rowg_mx1 [lemma, in mathcomp.character.mxabelem]
rowg_mxS [lemma, in mathcomp.character.mxabelem]
rowg_mx [definition, in mathcomp.character.mxabelem]
rowg_stable [lemma, in mathcomp.character.mxabelem]
rowg_group [definition, in mathcomp.character.mxabelem]
rowg_group_set [lemma, in mathcomp.character.mxabelem]
rowg0 [lemma, in mathcomp.character.mxabelem]
rowg1 [lemma, in mathcomp.character.mxabelem]
rowK [lemma, in mathcomp.algebra.matrix]
rowKd [lemma, in mathcomp.algebra.matrix]
rowKu [lemma, in mathcomp.algebra.matrix]
rowP [lemma, in mathcomp.algebra.matrix]
RowPoly [section, in mathcomp.algebra.mxpoly]
RowPoly.d [variable, in mathcomp.algebra.mxpoly]
RowPoly.R [variable, in mathcomp.algebra.mxpoly]
RowSpaceTheory [section, in mathcomp.algebra.mxalgebra]
RowSpaceTheoryDefs [section, in mathcomp.algebra.mxalgebra]
RowSpaceTheoryDefs.A [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheoryDefs.F [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheoryDefs.LUr [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheoryDefs.m [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheoryDefs.n [variable, in mathcomp.algebra.mxalgebra]
'M_ _ (type_scope) [notation, in mathcomp.algebra.mxalgebra]
'M_ ( _ , _ ) (type_scope) [notation, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.AddsmxSub [section, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.AddsmxSub.A [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.AddsmxSub.B [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.AddsmxSub.m1 [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.AddsmxSub.m2 [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.AddsmxSub.n [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.addsmx_nop_id [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.addsmx_nop0 [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.addsmx_nop_eq0 [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.BinaryDirect [section, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.BinaryDirect.m1 [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.BinaryDirect.m2 [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.BinaryDirect.n [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.capmx_nop_id [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.capmx_eq_norm [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.capmx_nopP [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.capmx_norm_eq [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.capmx_normP [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.capmx_witnessP [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.Eigenspace [section, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.Eigenspace.g [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.Eigenspace.n [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.eqmx_sum_nop [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.F [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.genmx_witnessP [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.hb_instance_9.n [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.hb_instance_9.hb_instance_9 [section, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.hb_instance_1.n [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.hb_instance_1.hb_instance_1 [section, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.I [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.MaxRankSubMatrix [section, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.MaxRankSubMatrix.A [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.MaxRankSubMatrix.m [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.MaxRankSubMatrix.n [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.MaxRankSubMatrix.rkA [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.NaryDirect [section, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.NaryDirect.mxdirect_sums_recP [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.NaryDirect.n [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.NaryDirect.P [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.NaryDirect.TIsum [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.qidmx_cap [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.qidmx_eq1 [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.SubDaddsmx [section, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.SubDaddsmx.A [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.SubDaddsmx.B1 [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.SubDaddsmx.B2 [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.SubDaddsmx.m [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.SubDaddsmx.m1 [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.SubDaddsmx.m2 [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.SubDaddsmx.n [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.SubDsumsmx [section, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.SubDsumsmx.A [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.SubDsumsmx.B [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.SubDsumsmx.m [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.SubDsumsmx.n [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.SubDsumsmx.P [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.sub_qidmx [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.SumExpr [section, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.SumExpr.Binary [section, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.SumExpr.Binary.m1 [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.SumExpr.Binary.m2 [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.SumExpr.Binary.n [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.SumExpr.Binary.S1 [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.SumExpr.Binary.S2 [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.SumExpr.Nary [section, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.unitmx1F [variable, in mathcomp.algebra.mxalgebra]
'M_ _ (type_scope) [notation, in mathcomp.algebra.mxalgebra]
'M_ ( _ , _ ) (type_scope) [notation, in mathcomp.algebra.mxalgebra]
rowsub [abbreviation, in mathcomp.algebra.matrix]
rowsub [abbreviation, in mathcomp.algebra.matrix]
rowsub [abbreviation, in mathcomp.algebra.matrix]
rowsubE [lemma, in mathcomp.algebra.matrix]
rowsub_cast [lemma, in mathcomp.algebra.matrix]
rowsub_comp [lemma, in mathcomp.algebra.matrix]
rowsub_comp_sub [lemma, in mathcomp.algebra.mxalgebra]
rowsub_sub [lemma, in mathcomp.algebra.mxalgebra]
rowV0P [lemma, in mathcomp.algebra.mxalgebra]
rowV0Pn [lemma, in mathcomp.algebra.mxalgebra]
row_mxdiag [lemma, in mathcomp.algebra.matrix]
row_mxblock [lemma, in mathcomp.algebra.matrix]
row_mxcol [lemma, in mathcomp.algebra.matrix]
row_mxrow [lemma, in mathcomp.algebra.matrix]
row_diag_mx [lemma, in mathcomp.algebra.matrix]
row_sum_delta [lemma, in mathcomp.algebra.matrix]
row_permE [lemma, in mathcomp.algebra.matrix]
row_mul [lemma, in mathcomp.algebra.matrix]
row_mx_eq0 [lemma, in mathcomp.algebra.matrix]
row_mx0 [lemma, in mathcomp.algebra.matrix]
row_ind [lemma, in mathcomp.algebra.matrix]
row_row_mx [lemma, in mathcomp.algebra.matrix]
row_mxAx [definition, in mathcomp.algebra.matrix]
row_mxA [lemma, in mathcomp.algebra.matrix]
row_thin_mx [lemma, in mathcomp.algebra.matrix]
row_dsubmx [lemma, in mathcomp.algebra.matrix]
row_usubmx [lemma, in mathcomp.algebra.matrix]
row_mx_const [lemma, in mathcomp.algebra.matrix]
row_mxKr [lemma, in mathcomp.algebra.matrix]
row_mxEr [lemma, in mathcomp.algebra.matrix]
row_mxKl [lemma, in mathcomp.algebra.matrix]
row_mxEl [lemma, in mathcomp.algebra.matrix]
row_mx [definition, in mathcomp.algebra.matrix]
row_mx_key [lemma, in mathcomp.algebra.matrix]
row_rowsub [lemma, in mathcomp.algebra.matrix]
row_mxsub [lemma, in mathcomp.algebra.matrix]
row_eq [lemma, in mathcomp.algebra.matrix]
row_id [lemma, in mathcomp.algebra.matrix]
row_permEsub [lemma, in mathcomp.algebra.matrix]
row_permM [lemma, in mathcomp.algebra.matrix]
row_perm1 [lemma, in mathcomp.algebra.matrix]
row_const [lemma, in mathcomp.algebra.matrix]
row_matrixP [lemma, in mathcomp.algebra.matrix]
row_perm_const [lemma, in mathcomp.algebra.matrix]
row_perm [definition, in mathcomp.algebra.matrix]
row_perm_key [lemma, in mathcomp.algebra.matrix]
row_full_dom_hom [lemma, in mathcomp.character.mxrepresentation]
row_hom_mxP [lemma, in mathcomp.character.mxrepresentation]
row_hom_mx [definition, in mathcomp.character.mxrepresentation]
row_schmidt_sub [lemma, in mathcomp.algebra.spectral]
row_unitarymxP [lemma, in mathcomp.algebra.spectral]
row_full_map [lemma, in mathcomp.algebra.mxalgebra]
row_free_map [lemma, in mathcomp.algebra.mxalgebra]
row_freePn [lemma, in mathcomp.algebra.mxalgebra]
row_free_castmx [lemma, in mathcomp.algebra.mxalgebra]
row_full_castmx [lemma, in mathcomp.algebra.mxalgebra]
row_base_free [lemma, in mathcomp.algebra.mxalgebra]
row_base0 [lemma, in mathcomp.algebra.mxalgebra]
row_full_unit [lemma, in mathcomp.algebra.mxalgebra]
row_free_unit [lemma, in mathcomp.algebra.mxalgebra]
row_free_injr [definition, in mathcomp.algebra.mxalgebra]
row_free_inj [lemma, in mathcomp.algebra.mxalgebra]
row_freeP [lemma, in mathcomp.algebra.mxalgebra]
row_full_inj [lemma, in mathcomp.algebra.mxalgebra]
row_fullP [lemma, in mathcomp.algebra.mxalgebra]
row_subPn [lemma, in mathcomp.algebra.mxalgebra]
row_subP [lemma, in mathcomp.algebra.mxalgebra]
row_sub [lemma, in mathcomp.algebra.mxalgebra]
row_ebase_unit [lemma, in mathcomp.algebra.mxalgebra]
row_leq_rank [lemma, in mathcomp.algebra.mxalgebra]
row_base [definition, in mathcomp.algebra.mxalgebra]
row_full [definition, in mathcomp.algebra.mxalgebra]
row_free [definition, in mathcomp.algebra.mxalgebra]
row_ebase [definition, in mathcomp.algebra.mxalgebra]
row' [definition, in mathcomp.algebra.matrix]
row'Esub [lemma, in mathcomp.algebra.matrix]
row'Kd [lemma, in mathcomp.algebra.matrix]
row'Ku [lemma, in mathcomp.algebra.matrix]
row'_row_mx [lemma, in mathcomp.algebra.matrix]
row'_eq [lemma, in mathcomp.algebra.matrix]
row'_const [lemma, in mathcomp.algebra.matrix]
row'_col'_char_poly_mx [lemma, in mathcomp.algebra.mxpoly]
row0 [lemma, in mathcomp.algebra.matrix]
row1 [lemma, in mathcomp.algebra.matrix]
rpred [section, in mathcomp.algebra.ssrint]
rpredMz [lemma, in mathcomp.algebra.ssrint]
rpredXsign [lemma, in mathcomp.algebra.ssrint]
rpredXz [lemma, in mathcomp.algebra.ssrint]
rpredZint [lemma, in mathcomp.algebra.ssrint]
rpred_Crat [lemma, in mathcomp.field.algC]
rpred_int [lemma, in mathcomp.algebra.ssrint]
rpred_rat [lemma, in mathcomp.algebra.rat]
rpred_horner [lemma, in mathcomp.algebra.poly]
rreg_div0 [lemma, in mathcomp.algebra.poly]
rreg_polyMC_eq0 [lemma, in mathcomp.algebra.poly]
rreg_size [lemma, in mathcomp.algebra.poly]
rreg_lead0 [lemma, in mathcomp.algebra.poly]
rreg_lead [lemma, in mathcomp.algebra.poly]
rshift [definition, in mathcomp.ssreflect.fintype]
rshift_inj [lemma, in mathcomp.ssreflect.fintype]
rshift_subproof [lemma, in mathcomp.ssreflect.fintype]
rshift1 [lemma, in mathcomp.algebra.zmodp]
rsimC [abbreviation, in mathcomp.character.mxrepresentation]
rsimT [abbreviation, in mathcomp.character.mxrepresentation]
rsim_abelem_subg [lemma, in mathcomp.character.mxabelem]
rsim_irr_comp [lemma, in mathcomp.character.mxrepresentation]
rsim_regular_submod [lemma, in mathcomp.character.mxrepresentation]
rsim_regular_series [lemma, in mathcomp.character.mxrepresentation]
rsim_regular_factmod [lemma, in mathcomp.character.mxrepresentation]
rsim_submod1 [lemma, in mathcomp.character.mxrepresentation]
rstab [definition, in mathcomp.character.mxrepresentation]
rstabS [lemma, in mathcomp.character.mxrepresentation]
rstabs [definition, in mathcomp.character.mxrepresentation]
rstabs_abelemG [lemma, in mathcomp.character.mxabelem]
rstabs_abelem [lemma, in mathcomp.character.mxabelem]
rstabs_map [lemma, in mathcomp.character.mxrepresentation]
rstabs_quo [lemma, in mathcomp.character.mxrepresentation]
rstabs_conj [lemma, in mathcomp.character.mxrepresentation]
rstabs_factmod [lemma, in mathcomp.character.mxrepresentation]
rstabs_submod [lemma, in mathcomp.character.mxrepresentation]
rstabs_morphim [lemma, in mathcomp.character.mxrepresentation]
rstabs_morphpre [lemma, in mathcomp.character.mxrepresentation]
rstabs_eqg [lemma, in mathcomp.character.mxrepresentation]
rstabs_subg [lemma, in mathcomp.character.mxrepresentation]
rstabs_act [lemma, in mathcomp.character.mxrepresentation]
rstabs_group [definition, in mathcomp.character.mxrepresentation]
rstabs_group_set [lemma, in mathcomp.character.mxrepresentation]
rstabs_sub [lemma, in mathcomp.character.mxrepresentation]
rstab_abelem [lemma, in mathcomp.character.mxabelem]
rstab_map [lemma, in mathcomp.character.mxrepresentation]
rstab_normal [lemma, in mathcomp.character.mxrepresentation]
rstab_norm [lemma, in mathcomp.character.mxrepresentation]
rstab_factmod [lemma, in mathcomp.character.mxrepresentation]
rstab_submod [lemma, in mathcomp.character.mxrepresentation]
rstab_act [lemma, in mathcomp.character.mxrepresentation]
rstab_quo [lemma, in mathcomp.character.mxrepresentation]
rstab_conj [lemma, in mathcomp.character.mxrepresentation]
rstab_morphim [lemma, in mathcomp.character.mxrepresentation]
rstab_morphpre [lemma, in mathcomp.character.mxrepresentation]
rstab_eqg [lemma, in mathcomp.character.mxrepresentation]
rstab_subg [lemma, in mathcomp.character.mxrepresentation]
rstab_group [definition, in mathcomp.character.mxrepresentation]
rstab_group_set [lemma, in mathcomp.character.mxrepresentation]
rstab_sub [lemma, in mathcomp.character.mxrepresentation]
rsubmx [definition, in mathcomp.algebra.matrix]
rsubmxEsub [lemma, in mathcomp.algebra.matrix]
rsubmx_key [lemma, in mathcomp.algebra.matrix]
rU [abbreviation, in mathcomp.character.mxrepresentation]
rU' [abbreviation, in mathcomp.character.mxrepresentation]
rVabelem [definition, in mathcomp.character.mxabelem]
rVabelemD [lemma, in mathcomp.character.mxabelem]
rVabelemJ [lemma, in mathcomp.character.mxabelem]
rVabelemK [lemma, in mathcomp.character.mxabelem]
rVabelemN [lemma, in mathcomp.character.mxabelem]
rVabelemS [lemma, in mathcomp.character.mxabelem]
rVabelemZ [lemma, in mathcomp.character.mxabelem]
rVabelem_minj [lemma, in mathcomp.character.mxabelem]
rVabelem_mK [lemma, in mathcomp.character.mxabelem]
rVabelem_injm [lemma, in mathcomp.character.mxabelem]
rVabelem_inj [lemma, in mathcomp.character.mxabelem]
rVabelem_morphism [definition, in mathcomp.character.mxabelem]
rVabelem0 [lemma, in mathcomp.character.mxabelem]
rVn [abbreviation, in mathcomp.character.mxabelem]
rVn [abbreviation, in mathcomp.character.mxabelem]
rVn [abbreviation, in mathcomp.character.mxabelem]
rVnpoly [definition, in mathcomp.algebra.qpoly]
rVnpolyK [lemma, in mathcomp.algebra.qpoly]
rVpoly [definition, in mathcomp.algebra.mxpoly]
rVpolyK [lemma, in mathcomp.algebra.mxpoly]
rVpoly_is_linear [lemma, in mathcomp.algebra.mxpoly]
rVpoly_delta [lemma, in mathcomp.algebra.mxpoly]
rV_abelem_sJ [lemma, in mathcomp.character.mxabelem]
rV_E [abbreviation, in mathcomp.character.mxabelem]
rV_form0_eq0 [lemma, in mathcomp.algebra.sesquilinear]
rV_formee [lemma, in mathcomp.algebra.sesquilinear]
rV_eqP [lemma, in mathcomp.algebra.mxalgebra]
rV_subP [lemma, in mathcomp.algebra.mxalgebra]
rV0Pn [lemma, in mathcomp.algebra.matrix]
R_G [abbreviation, in mathcomp.character.integral_char]
R_G [abbreviation, in mathcomp.character.mxrepresentation]
R_G [abbreviation, in mathcomp.character.mxrepresentation]
r012 [definition, in mathcomp.solvable.burnside_app]
R012 [definition, in mathcomp.solvable.burnside_app]
R012f [definition, in mathcomp.solvable.burnside_app]
R012_inj [lemma, in mathcomp.solvable.burnside_app]
r013 [definition, in mathcomp.solvable.burnside_app]
R013 [definition, in mathcomp.solvable.burnside_app]
R013f [definition, in mathcomp.solvable.burnside_app]
R013_inj [lemma, in mathcomp.solvable.burnside_app]
r021 [definition, in mathcomp.solvable.burnside_app]
R021 [definition, in mathcomp.solvable.burnside_app]
R021f [definition, in mathcomp.solvable.burnside_app]
R021_inj [lemma, in mathcomp.solvable.burnside_app]
r024 [definition, in mathcomp.solvable.burnside_app]
R024 [definition, in mathcomp.solvable.burnside_app]
R024f [definition, in mathcomp.solvable.burnside_app]
R024_inj [lemma, in mathcomp.solvable.burnside_app]
r031 [definition, in mathcomp.solvable.burnside_app]
R031 [definition, in mathcomp.solvable.burnside_app]
R031f [definition, in mathcomp.solvable.burnside_app]
R031_inj [lemma, in mathcomp.solvable.burnside_app]
r034 [definition, in mathcomp.solvable.burnside_app]
R034 [definition, in mathcomp.solvable.burnside_app]
R034f [definition, in mathcomp.solvable.burnside_app]
R034_inj [lemma, in mathcomp.solvable.burnside_app]
r042 [definition, in mathcomp.solvable.burnside_app]
R042 [definition, in mathcomp.solvable.burnside_app]
R042f [definition, in mathcomp.solvable.burnside_app]
R042_inj [lemma, in mathcomp.solvable.burnside_app]
r043 [definition, in mathcomp.solvable.burnside_app]
R043 [definition, in mathcomp.solvable.burnside_app]
R043f [definition, in mathcomp.solvable.burnside_app]
R043_inj [lemma, in mathcomp.solvable.burnside_app]
r05 [definition, in mathcomp.solvable.burnside_app]
R05 [definition, in mathcomp.solvable.burnside_app]
R05f [definition, in mathcomp.solvable.burnside_app]
r05_inv [lemma, in mathcomp.solvable.burnside_app]
R05_inj [lemma, in mathcomp.solvable.burnside_app]
r1 [definition, in mathcomp.solvable.burnside_app]
R1 [definition, in mathcomp.solvable.burnside_app]
r1_inv [lemma, in mathcomp.solvable.burnside_app]
R1_inj [lemma, in mathcomp.solvable.burnside_app]
r14 [definition, in mathcomp.solvable.burnside_app]
R14 [definition, in mathcomp.solvable.burnside_app]
R14f [definition, in mathcomp.solvable.burnside_app]
r14_inv [lemma, in mathcomp.solvable.burnside_app]
R14_inj [lemma, in mathcomp.solvable.burnside_app]
r2 [definition, in mathcomp.solvable.burnside_app]
R2 [definition, in mathcomp.solvable.burnside_app]
r2_inv [lemma, in mathcomp.solvable.burnside_app]
R2_inj [lemma, in mathcomp.solvable.burnside_app]
r23 [definition, in mathcomp.solvable.burnside_app]
R23 [definition, in mathcomp.solvable.burnside_app]
R23f [definition, in mathcomp.solvable.burnside_app]
R23_inj [lemma, in mathcomp.solvable.burnside_app]
r3 [definition, in mathcomp.solvable.burnside_app]
R3 [definition, in mathcomp.solvable.burnside_app]
r3_inv [lemma, in mathcomp.solvable.burnside_app]
R3_inj [lemma, in mathcomp.solvable.burnside_app]
r32 [definition, in mathcomp.solvable.burnside_app]
R32 [definition, in mathcomp.solvable.burnside_app]
R32f [definition, in mathcomp.solvable.burnside_app]
R32_inj [lemma, in mathcomp.solvable.burnside_app]
r41 [definition, in mathcomp.solvable.burnside_app]
R41 [definition, in mathcomp.solvable.burnside_app]
R41f [definition, in mathcomp.solvable.burnside_app]
r41_inv [lemma, in mathcomp.solvable.burnside_app]
R41_inj [lemma, in mathcomp.solvable.burnside_app]
r50 [definition, in mathcomp.solvable.burnside_app]
R50 [definition, in mathcomp.solvable.burnside_app]
R50f [definition, in mathcomp.solvable.burnside_app]
r50_inv [lemma, in mathcomp.solvable.burnside_app]
R50_inj [lemma, in mathcomp.solvable.burnside_app]

---

Global Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(54001 entries)

Notation Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(1931 entries)

Module Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(1658 entries)

Variable Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(7199 entries)

Library Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(97 entries)

Lemma Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(15214 entries)

Axiom Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(75 entries)

Constructor Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(224 entries)

Inductive Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(132 entries)

Projection Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(2371 entries)

Section Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(2266 entries)

Abbreviation Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(732 entries)

Definition Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(21455 entries)

Record Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(647 entries)

---

Index

---

This page has been generated by coqdoc