| 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 | (78134 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 | (1810 entries) |
| Binder 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 | (47626 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 | (375 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 | (4027 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 | (91 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 | (14457 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 | (469 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 | (45 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 | (133 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 | (451 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 | (1391 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 | (851 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 | (6161 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 | (247 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]
raddfMz [lemma, in mathcomp.algebra.ssrint]
raddfZ_Cint [lemma, in mathcomp.field.algC]
raddfZ_Cnat [lemma, in mathcomp.field.algC]
raddf_int_scalable [lemma, in mathcomp.algebra.ssrint]
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_DnQ [lemma, in mathcomp.solvable.extraspecial]
rank_Dn [lemma, in mathcomp.solvable.extraspecial]
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 [constructor, in mathcomp.algebra.rat]
rat [library]
ratCK [lemma, in mathcomp.field.algC]
RatFieldIdomainMixin [definition, in mathcomp.algebra.rat]
RatFieldUnitMixin [definition, in mathcomp.algebra.rat]
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_of_choiceType [definition, in mathcomp.algebra.fraction]
ratio_choiceType [definition, in mathcomp.algebra.fraction]
ratio_ChoiceMixin [definition, in mathcomp.algebra.fraction]
ratio_of_eqType [definition, in mathcomp.algebra.fraction]
ratio_eqType [definition, in mathcomp.algebra.fraction]
ratio_EqMixin [definition, in mathcomp.algebra.fraction]
ratio_of_subType [definition, in mathcomp.algebra.fraction]
ratio_subType [definition, in mathcomp.algebra.fraction]
ratio_of [definition, in mathcomp.algebra.fraction]
Ratio0 [lemma, in mathcomp.algebra.fraction]
ratio0 [definition, in mathcomp.algebra.fraction]
RatK [lemma, in mathcomp.algebra.rat]
ratLeMixin [definition, 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_rmorphism [definition, in mathcomp.algebra.rat]
ratr_additive [definition, in mathcomp.algebra.rat]
ratr_is_rmorphism [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_lrmorphism [lemma, in mathcomp.algebra.rat]
rat_linear [lemma, in mathcomp.algebra.rat]
rat_archimedean [lemma, in mathcomp.algebra.rat]
rat_realFieldType [definition, in mathcomp.algebra.rat]
rat_realDomainType [definition, in mathcomp.algebra.rat]
rat_numFieldType [definition, in mathcomp.algebra.rat]
rat_normedZmodType [definition, in mathcomp.algebra.rat]
rat_numDomainType [definition, in mathcomp.algebra.rat]
rat_orderType [definition, in mathcomp.algebra.rat]
rat_distrLatticeType [definition, in mathcomp.algebra.rat]
rat_latticeType [definition, in mathcomp.algebra.rat]
rat_porderType [definition, in mathcomp.algebra.rat]
Rat_spec [constructor, in mathcomp.algebra.rat]
rat_spec [inductive, in mathcomp.algebra.rat]
rat_countFieldType [definition, in mathcomp.algebra.rat]
rat_countIdomainType [definition, in mathcomp.algebra.rat]
rat_countComUnitRingType [definition, in mathcomp.algebra.rat]
rat_countUnitRingType [definition, in mathcomp.algebra.rat]
rat_countComRingType [definition, in mathcomp.algebra.rat]
rat_countRingType [definition, in mathcomp.algebra.rat]
rat_countZmodType [definition, in mathcomp.algebra.rat]
rat_fieldType [definition, in mathcomp.algebra.rat]
rat_idomainType [definition, in mathcomp.algebra.rat]
rat_field_axiom [lemma, in mathcomp.algebra.rat]
rat_comUnitRing [definition, in mathcomp.algebra.rat]
rat_unitRing [definition, in mathcomp.algebra.rat]
rat_comRing [definition, in mathcomp.algebra.rat]
rat_Ring [definition, in mathcomp.algebra.rat]
rat_comRingMixin [definition, in mathcomp.algebra.rat]
rat_ZmodType [definition, in mathcomp.algebra.rat]
rat_ZmodMixin [definition, in mathcomp.algebra.rat]
rat_eq [lemma, in mathcomp.algebra.rat]
rat_eqE [lemma, in mathcomp.algebra.rat]
rat_subCountType [definition, in mathcomp.algebra.rat]
rat_countType [definition, in mathcomp.algebra.rat]
rat_countMixin [definition, in mathcomp.algebra.rat]
rat_choiceType [definition, in mathcomp.algebra.rat]
rat_choiceMixin [definition, in mathcomp.algebra.rat]
rat_eqType [definition, in mathcomp.algebra.rat]
rat_eqMixin [definition, in mathcomp.algebra.rat]
rat_subType [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]
rc:108 [binder, in mathcomp.algebra.ring_quotient]
rc:114 [binder, in mathcomp.algebra.ring_quotient]
rc:145 [binder, in mathcomp.algebra.ring_quotient]
rc:180 [binder, in mathcomp.algebra.ring_quotient]
rc:186 [binder, in mathcomp.algebra.ring_quotient]
rc:77 [binder, in mathcomp.algebra.ring_quotient]
rdegree [projection, in mathcomp.character.character]
realz [lemma, in mathcomp.algebra.ssrint]
recf:549 [binder, in mathcomp.algebra.mxpoly]
redg:2006 [binder, in mathcomp.algebra.ssralg]
reducebig [definition, in mathcomp.ssreflect.bigop]
reducible_Socle1 [lemma, in mathcomp.character.mxrepresentation]
reducible_Socle [lemma, in mathcomp.character.mxrepresentation]
refBaseField [definition, in mathcomp.field.fieldext]
refBaseField_unlockable [definition, in mathcomp.field.fieldext]
refBaseField_key [lemma, in mathcomp.field.fieldext]
ReflectCombinators [section, in mathcomp.ssreflect.ssrbool]
ReflectCombinators.p [variable, in mathcomp.ssreflect.ssrbool]
ReflectCombinators.P [variable, in mathcomp.ssreflect.ssrbool]
ReflectCombinators.q [variable, in mathcomp.ssreflect.ssrbool]
ReflectCombinators.Q [variable, in mathcomp.ssreflect.ssrbool]
ReflectCombinators.rP [variable, in mathcomp.ssreflect.ssrbool]
ReflectCombinators.rQ [variable, in mathcomp.ssreflect.ssrbool]
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_splittingFieldType [definition, in mathcomp.field.galois]
regular_splittingAxiom [lemma, in mathcomp.field.galois]
regular_fieldExtType [definition, in mathcomp.field.fieldext]
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_vectType [definition, in mathcomp.algebra.vector]
regular_vectMixin [definition, in mathcomp.algebra.vector]
regular_vect_iso [lemma, in mathcomp.algebra.vector]
regular_fullv [lemma, in mathcomp.field.falgebra]
regular_FalgType [definition, 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]
reindex_inj_AC [lemma, in mathcomp.ssreflect.bigop]
reindex_AC [lemma, in mathcomp.ssreflect.bigop]
reindex_onto_AC [lemma, in mathcomp.ssreflect.bigop]
reindex_omap_AC [lemma, in mathcomp.ssreflect.bigop]
RelAdjunction [constructor, in mathcomp.ssreflect.fingraph]
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]
relU_sym [lemma, in mathcomp.ssreflect.fingraph]
rel_base [definition, in mathcomp.ssreflect.path]
rel_of_simpl_rel [abbreviation, in mathcomp.ssreflect.ssrbool]
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]
rem_filter [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 [abbreviation, in mathcomp.ssreflect.generic_quotient]
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]
Representation [constructor, 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]
ReprSig [module, in mathcomp.ssreflect.generic_quotient]
ReprSig.E [axiom, in mathcomp.ssreflect.generic_quotient]
ReprSig.f [axiom, 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_ofK [lemma, 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.E [definition, in mathcomp.ssreflect.generic_quotient]
Repr.f [definition, in mathcomp.ssreflect.generic_quotient]
Repr.gT [variable, in mathcomp.fingroup.fingroup]
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]
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]
rF [abbreviation, in mathcomp.character.mxrepresentation]
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]
rfG:656 [binder, in mathcomp.character.character]
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]
rGf:1418 [binder, 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]
rG0:156 [binder, in mathcomp.character.mxrepresentation]
rG1:109 [binder, in mathcomp.character.character]
rG1:112 [binder, in mathcomp.character.character]
rG1:1259 [binder, in mathcomp.character.mxrepresentation]
rG1:1414 [binder, in mathcomp.character.mxrepresentation]
rG1:166 [binder, in mathcomp.character.character]
rG1:181 [binder, in mathcomp.character.character]
rG1:183 [binder, in mathcomp.character.character]
rG1:310 [binder, in mathcomp.character.character]
rG1:316 [binder, in mathcomp.character.character]
rG1:365 [binder, in mathcomp.character.character]
rG1:825 [binder, in mathcomp.character.mxrepresentation]
rG1:834 [binder, in mathcomp.character.mxrepresentation]
rG1:840 [binder, in mathcomp.character.mxrepresentation]
rG1:845 [binder, in mathcomp.character.mxrepresentation]
rG1:850 [binder, in mathcomp.character.mxrepresentation]
rG1:864 [binder, in mathcomp.character.mxrepresentation]
rG1:868 [binder, in mathcomp.character.mxrepresentation]
rG1:873 [binder, in mathcomp.character.mxrepresentation]
rG1:877 [binder, in mathcomp.character.mxrepresentation]
rG1:887 [binder, in mathcomp.character.mxrepresentation]
rG1:892 [binder, in mathcomp.character.mxrepresentation]
rG2:110 [binder, in mathcomp.character.character]
rG2:113 [binder, in mathcomp.character.character]
rG2:1260 [binder, in mathcomp.character.mxrepresentation]
rG2:1415 [binder, in mathcomp.character.mxrepresentation]
rG2:167 [binder, in mathcomp.character.character]
rG2:182 [binder, in mathcomp.character.character]
rG2:184 [binder, in mathcomp.character.character]
rG2:311 [binder, in mathcomp.character.character]
rG2:317 [binder, in mathcomp.character.character]
rG2:366 [binder, in mathcomp.character.character]
rG2:827 [binder, in mathcomp.character.mxrepresentation]
rG2:835 [binder, in mathcomp.character.mxrepresentation]
rG2:841 [binder, in mathcomp.character.mxrepresentation]
rG2:846 [binder, in mathcomp.character.mxrepresentation]
rG2:851 [binder, in mathcomp.character.mxrepresentation]
rG2:865 [binder, in mathcomp.character.mxrepresentation]
rG2:869 [binder, in mathcomp.character.mxrepresentation]
rG2:874 [binder, in mathcomp.character.mxrepresentation]
rG2:878 [binder, in mathcomp.character.mxrepresentation]
rG2:888 [binder, in mathcomp.character.mxrepresentation]
rG2:893 [binder, in mathcomp.character.mxrepresentation]
rG3:847 [binder, in mathcomp.character.mxrepresentation]
rG:1038 [binder, in mathcomp.character.character]
rG:1417 [binder, in mathcomp.character.mxrepresentation]
rG:1436 [binder, in mathcomp.character.mxrepresentation]
rG:173 [binder, in mathcomp.character.character]
rG:176 [binder, in mathcomp.character.character]
rG:178 [binder, in mathcomp.character.character]
rG:188 [binder, in mathcomp.character.character]
rG:195 [binder, in mathcomp.character.character]
rG:215 [binder, in mathcomp.character.mxabelem]
rG:237 [binder, in mathcomp.character.character]
rG:304 [binder, in mathcomp.character.character]
rG:319 [binder, in mathcomp.character.character]
rG:320 [binder, in mathcomp.character.character]
rG:352 [binder, in mathcomp.character.character]
rG:362 [binder, in mathcomp.character.character]
rG:371 [binder, in mathcomp.character.character]
rG:426 [binder, in mathcomp.character.character]
rG:564 [binder, in mathcomp.character.character]
rG:570 [binder, in mathcomp.character.character]
rG:602 [binder, in mathcomp.character.character]
rG:628 [binder, in mathcomp.character.character]
rG:795 [binder, in mathcomp.character.mxrepresentation]
rG:806 [binder, in mathcomp.character.mxrepresentation]
rG:808 [binder, in mathcomp.character.mxrepresentation]
rG:811 [binder, in mathcomp.character.mxrepresentation]
rG:813 [binder, in mathcomp.character.mxrepresentation]
rG:816 [binder, in mathcomp.character.mxrepresentation]
rG:837 [binder, in mathcomp.character.mxrepresentation]
rG:857 [binder, in mathcomp.character.mxrepresentation]
rG:87 [binder, in mathcomp.character.integral_char]
rG:880 [binder, in mathcomp.character.mxrepresentation]
rG:91 [binder, in mathcomp.character.integral_char]
rG:997 [binder, in mathcomp.character.character]
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]
rho:112 [binder, in mathcomp.solvable.pgroup]
rho:116 [binder, in mathcomp.solvable.pgroup]
rho:120 [binder, in mathcomp.solvable.pgroup]
rho:127 [binder, in mathcomp.solvable.pgroup]
rho:31 [binder, in mathcomp.solvable.pgroup]
rho:34 [binder, in mathcomp.solvable.pgroup]
rho:37 [binder, in mathcomp.solvable.pgroup]
rho:462 [binder, in mathcomp.ssreflect.prime]
rho:465 [binder, in mathcomp.ssreflect.prime]
rho:468 [binder, in mathcomp.ssreflect.prime]
rho:473 [binder, in mathcomp.ssreflect.prime]
rho:518 [binder, in mathcomp.ssreflect.prime]
rho:548 [binder, in mathcomp.ssreflect.prime]
rho:551 [binder, in mathcomp.ssreflect.prime]
rho:569 [binder, in mathcomp.solvable.pgroup]
rho:572 [binder, in mathcomp.solvable.pgroup]
rho:575 [binder, in mathcomp.solvable.pgroup]
rho:578 [binder, in mathcomp.solvable.pgroup]
rho:583 [binder, in mathcomp.solvable.pgroup]
rho:592 [binder, in mathcomp.solvable.pgroup]
rhs:117 [binder, in mathcomp.ssreflect.choice]
rhs:124 [binder, in mathcomp.ssreflect.choice]
rid:102 [binder, in mathcomp.ssreflect.ssrAC]
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]
RingQuot [section, in mathcomp.algebra.ring_quotient]
RingQuotClass [constructor, in mathcomp.algebra.ring_quotient]
RingQuotMixin [abbreviation, in mathcomp.algebra.ring_quotient]
RingQuotMixinPack [constructor, in mathcomp.algebra.ring_quotient]
RingQuotMixin_pack [definition, in mathcomp.algebra.ring_quotient]
RingQuotType [abbreviation, in mathcomp.algebra.ring_quotient]
ringQuotType [record, in mathcomp.algebra.ring_quotient]
RingQuotTypePack [constructor, in mathcomp.algebra.ring_quotient]
RingQuotType_clone [definition, in mathcomp.algebra.ring_quotient]
RingQuotType_pack [definition, in mathcomp.algebra.ring_quotient]
ringQuotType_zmodQuotType [definition, in mathcomp.algebra.ring_quotient]
ringQuotType_eqQuotType [definition, in mathcomp.algebra.ring_quotient]
ringQuotType_quotType [definition, in mathcomp.algebra.ring_quotient]
ringQuotType_ringType [definition, in mathcomp.algebra.ring_quotient]
ringQuotType_zmodType [definition, in mathcomp.algebra.ring_quotient]
ringQuotType_choiceType [definition, in mathcomp.algebra.ring_quotient]
ringQuotType_eqType [definition, in mathcomp.algebra.ring_quotient]
RingQuot.addT [variable, in mathcomp.algebra.ring_quotient]
RingQuot.eqT [variable, in mathcomp.algebra.ring_quotient]
RingQuot.mulT [variable, in mathcomp.algebra.ring_quotient]
RingQuot.oneT [variable, in mathcomp.algebra.ring_quotient]
RingQuot.oppT [variable, in mathcomp.algebra.ring_quotient]
RingQuot.T [variable, in mathcomp.algebra.ring_quotient]
RingQuot.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]
ringS:1588 [binder, in mathcomp.algebra.ssralg]
ringS:1594 [binder, in mathcomp.algebra.ssralg]
ringS:1597 [binder, in mathcomp.algebra.ssralg]
ringS:160 [binder, in mathcomp.field.algC]
ringS:1607 [binder, in mathcomp.algebra.ssralg]
ringS:186 [binder, in mathcomp.field.algC]
ringS:256 [binder, in mathcomp.algebra.rat]
ringS:2598 [binder, in mathcomp.algebra.matrix]
ringS:331 [binder, in mathcomp.field.algC]
ringS:594 [binder, in mathcomp.algebra.poly]
ringS:634 [binder, in mathcomp.algebra.poly]
ringS:680 [binder, in mathcomp.algebra.poly]
ringS:828 [binder, in mathcomp.algebra.poly]
ringS:859 [binder, in mathcomp.algebra.ssrint]
ring_quot_mixinP [lemma, in mathcomp.algebra.ring_quotient]
ring_eq_quot_class [definition, in mathcomp.algebra.ring_quotient]
ring_zmod_quot_class [definition, in mathcomp.algebra.ring_quotient]
ring_quot_class [definition, in mathcomp.algebra.ring_quotient]
ring_quot_sort [projection, in mathcomp.algebra.ring_quotient]
ring_quot_mixin [projection, in mathcomp.algebra.ring_quotient]
ring_quot_ring_class [projection, in mathcomp.algebra.ring_quotient]
ring_quot_quot_class [projection, in mathcomp.algebra.ring_quotient]
ring_quot_class_of [record, in mathcomp.algebra.ring_quotient]
ring_zmod_quot_mixin [projection, in mathcomp.algebra.ring_quotient]
ring_quot_mixin_of [record, in mathcomp.algebra.ring_quotient]
ring_display [lemma, in mathcomp.algebra.ssrnum]
ring_quotient [library]
RintMod [section, in mathcomp.algebra.ssrint]
RintMod.R [variable, in mathcomp.algebra.ssrint]
rI:1573 [binder, in mathcomp.ssreflect.bigop]
rI:1596 [binder, in mathcomp.ssreflect.bigop]
rI:2424 [binder, in mathcomp.ssreflect.bigop]
rI:2446 [binder, in mathcomp.ssreflect.bigop]
rI:2754 [binder, in mathcomp.ssreflect.bigop]
rI:344 [binder, in mathcomp.algebra.poly]
rI:353 [binder, in mathcomp.algebra.poly]
rI:360 [binder, in mathcomp.algebra.poly]
rJ:1574 [binder, in mathcomp.ssreflect.bigop]
rJ:1597 [binder, in mathcomp.ssreflect.bigop]
rJ:2425 [binder, in mathcomp.ssreflect.bigop]
rJ:2447 [binder, in mathcomp.ssreflect.bigop]
rJ:2755 [binder, in mathcomp.ssreflect.bigop]
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]
rk:191 [binder, in mathcomp.algebra.vector]
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]
rngS:1819 [binder, in mathcomp.algebra.ssralg]
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]
Rorder:14 [binder, in mathcomp.algebra.ssrnum]
Rorder:3 [binder, in mathcomp.algebra.ssrnum]
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]
RoverFp:169 [binder, in mathcomp.field.finfield]
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]
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.addsmx_nop [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.capmx_nop [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.capmx_norm [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.capmx_witness [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.Defs [section, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.Defs.A [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.Defs.LUr [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.Defs.m [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.Defs.n [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.equivmx [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.equivmx_spec [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.F [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.genmx_witnessP [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.I [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.LtmxIdentities [section, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.LtmxIdentities.A [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.LtmxIdentities.B [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.LtmxIdentities.m1 [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.LtmxIdentities.m2 [variable, in mathcomp.algebra.mxalgebra]
RowSpaceTheory.LtmxIdentities.n [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 [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]
_ :\: _ (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]
\bigcap_ ( _ | _ ) _ (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]
_ :&: _ (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]
\sum_ ( _ <- _ | _ ) _ (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]
\sum_ ( _ | _ ) _ (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]
_ + _ (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]
<< _ >> (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]
_ :=: _ (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]
_ < _ (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]
_ == _ (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]
_ <= _ <= _ (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]
_ <= _ (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]
_ ^C (matrix_set_scope) [notation, in mathcomp.algebra.mxalgebra]
\rank _ (nat_scope) [notation, 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_permE [lemma, in mathcomp.algebra.matrix]
row_mul [lemma, in mathcomp.algebra.matrix]
row_diag_mx [lemma, in mathcomp.algebra.matrix]
row_sum_delta [lemma, in mathcomp.algebra.matrix]
row_perm_linear [definition, in mathcomp.algebra.matrix]
row_linear [definition, in mathcomp.algebra.matrix]
row_mx_eq0 [lemma, in mathcomp.algebra.matrix]
row_mx0 [lemma, in mathcomp.algebra.matrix]
row_perm_additive [definition, in mathcomp.algebra.matrix]
row_additive [definition, 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_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'_linear [definition, in mathcomp.algebra.matrix]
row'_additive [definition, 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]
row1:731 [binder, in mathcomp.algebra.matrix]
row3:733 [binder, 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]
rpredZ_Cint [lemma, in mathcomp.field.algC]
rpredZ_Cnat [lemma, in mathcomp.field.algC]
rpred_Crat [lemma, in mathcomp.field.algC]
rpred_Cnat [lemma, in mathcomp.field.algC]
rpred_Cint [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]
rP:126 [binder, in mathcomp.ssreflect.ssrbool]
rP:208 [binder, in mathcomp.ssreflect.ssrbool]
rqc:162 [binder, in mathcomp.algebra.ring_quotient]
rqc:164 [binder, in mathcomp.algebra.ring_quotient]
rqc:166 [binder, in mathcomp.algebra.ring_quotient]
rqc:94 [binder, in mathcomp.algebra.ring_quotient]
rqc:96 [binder, in mathcomp.algebra.ring_quotient]
rqT:100 [binder, in mathcomp.algebra.ring_quotient]
rqT:101 [binder, in mathcomp.algebra.ring_quotient]
rqT:102 [binder, in mathcomp.algebra.ring_quotient]
rqT:103 [binder, in mathcomp.algebra.ring_quotient]
rqT:121 [binder, in mathcomp.algebra.ring_quotient]
rqT:122 [binder, in mathcomp.algebra.ring_quotient]
rqT:123 [binder, in mathcomp.algebra.ring_quotient]
rqT:128 [binder, in mathcomp.algebra.ring_quotient]
rqT:129 [binder, in mathcomp.algebra.ring_quotient]
rqT:159 [binder, in mathcomp.algebra.ring_quotient]
rqT:161 [binder, in mathcomp.algebra.ring_quotient]
rqT:163 [binder, in mathcomp.algebra.ring_quotient]
rqT:165 [binder, in mathcomp.algebra.ring_quotient]
rqT:167 [binder, in mathcomp.algebra.ring_quotient]
rqT:168 [binder, in mathcomp.algebra.ring_quotient]
rqT:169 [binder, in mathcomp.algebra.ring_quotient]
rqT:170 [binder, in mathcomp.algebra.ring_quotient]
rqT:171 [binder, in mathcomp.algebra.ring_quotient]
rqT:172 [binder, in mathcomp.algebra.ring_quotient]
rqT:173 [binder, in mathcomp.algebra.ring_quotient]
rqT:174 [binder, in mathcomp.algebra.ring_quotient]
rqT:175 [binder, in mathcomp.algebra.ring_quotient]
rqT:193 [binder, in mathcomp.algebra.ring_quotient]
rqT:194 [binder, in mathcomp.algebra.ring_quotient]
rqT:197 [binder, in mathcomp.algebra.ring_quotient]
rqT:200 [binder, in mathcomp.algebra.ring_quotient]
rqT:201 [binder, in mathcomp.algebra.ring_quotient]
rqT:91 [binder, in mathcomp.algebra.ring_quotient]
rqT:93 [binder, in mathcomp.algebra.ring_quotient]
rqT:95 [binder, in mathcomp.algebra.ring_quotient]
rqT:97 [binder, in mathcomp.algebra.ring_quotient]
rqT:98 [binder, in mathcomp.algebra.ring_quotient]
rqT:99 [binder, in mathcomp.algebra.ring_quotient]
rQ:2476 [binder, in mathcomp.algebra.ssralg]
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]
rr:1970 [binder, in mathcomp.ssreflect.bigop]
rr:206 [binder, in mathcomp.field.closed_field]
rr:212 [binder, in mathcomp.field.closed_field]
rR:252 [binder, in mathcomp.algebra.mxpoly]
rR:260 [binder, in mathcomp.algebra.rat]
rR:263 [binder, in mathcomp.algebra.rat]
rr:470 [binder, in mathcomp.algebra.polydiv]
rr:479 [binder, in mathcomp.algebra.polydiv]
rr:68 [binder, in mathcomp.algebra.polydiv]
rR:70 [binder, in mathcomp.field.algnum]
rr:77 [binder, in mathcomp.algebra.polydiv]
rR:868 [binder, 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_linear [definition, in mathcomp.algebra.matrix]
rsubmx_additive [definition, in mathcomp.algebra.matrix]
rsubmx_key [lemma, in mathcomp.algebra.matrix]
rs1:299 [binder, in mathcomp.field.falgebra]
rs2:300 [binder, in mathcomp.field.falgebra]
rs:10 [binder, in mathcomp.field.galois]
rs:1137 [binder, in mathcomp.algebra.poly]
rs:1157 [binder, in mathcomp.algebra.poly]
rs:1159 [binder, in mathcomp.algebra.poly]
rs:1184 [binder, in mathcomp.algebra.poly]
rs:1188 [binder, in mathcomp.algebra.poly]
rs:1194 [binder, in mathcomp.algebra.poly]
rs:1196 [binder, in mathcomp.algebra.poly]
rs:1203 [binder, in mathcomp.algebra.poly]
rs:1208 [binder, in mathcomp.algebra.poly]
rs:1209 [binder, in mathcomp.algebra.poly]
rs:188 [binder, in mathcomp.algebra.polydiv]
rs:215 [binder, in mathcomp.solvable.cyclic]
rs:262 [binder, in mathcomp.field.separable]
rs:283 [binder, in mathcomp.field.falgebra]
rs:285 [binder, in mathcomp.field.falgebra]
rs:297 [binder, in mathcomp.field.falgebra]
rs:388 [binder, in mathcomp.algebra.polydiv]
rs:57 [binder, in mathcomp.field.fieldext]
rs:6 [binder, in mathcomp.field.galois]
rs:778 [binder, in mathcomp.algebra.mxpoly]
rs:839 [binder, in mathcomp.algebra.mxpoly]
rs:840 [binder, in mathcomp.algebra.mxpoly]
rs:844 [binder, in mathcomp.algebra.mxpoly]
rs:856 [binder, in mathcomp.algebra.mxpoly]
rs:857 [binder, in mathcomp.algebra.mxpoly]
rT [abbreviation, in mathcomp.fingroup.fingroup]
RtoK:379 [binder, in mathcomp.algebra.mxpoly]
RtoK:385 [binder, in mathcomp.algebra.mxpoly]
rT':29 [binder, in mathcomp.fingroup.action]
rT:1 [binder, in mathcomp.ssreflect.ssrfun]
rT:10 [binder, in mathcomp.ssreflect.ssrfun]
rT:1013 [binder, in mathcomp.character.character]
rT:1019 [binder, in mathcomp.character.character]
rT:102 [binder, in mathcomp.solvable.gfunctor]
rT:107 [binder, in mathcomp.solvable.gfunctor]
rt:109 [binder, in mathcomp.field.closed_field]
rT:112 [binder, in mathcomp.solvable.gfunctor]
rT:113 [binder, in mathcomp.algebra.ring_quotient]
rT:118 [binder, in mathcomp.solvable.gfunctor]
rT:119 [binder, in mathcomp.solvable.cyclic]
rT:122 [binder, in mathcomp.ssreflect.ssrbool]
rT:123 [binder, in mathcomp.solvable.gfunctor]
rT:123 [binder, in mathcomp.solvable.maximal]
rT:128 [binder, in mathcomp.solvable.maximal]
rT:13 [binder, in mathcomp.ssreflect.ssrfun]
rT:1340 [binder, in mathcomp.ssreflect.seq]
rT:1345 [binder, in mathcomp.ssreflect.seq]
rT:143 [binder, in mathcomp.ssreflect.ssrbool]
rT:148 [binder, in mathcomp.solvable.center]
rT:149 [binder, in mathcomp.ssreflect.ssrbool]
rT:151 [binder, in mathcomp.solvable.commutator]
rT:152 [binder, in mathcomp.solvable.gseries]
rT:16 [binder, in mathcomp.ssreflect.ssrfun]
rT:17 [binder, in mathcomp.fingroup.action]
rT:171 [binder, in mathcomp.solvable.commutator]
rT:178 [binder, in mathcomp.algebra.ring_quotient]
rT:185 [binder, in mathcomp.algebra.ring_quotient]
rT:19 [binder, in mathcomp.ssreflect.ssrfun]
rT:204 [binder, in mathcomp.ssreflect.ssrbool]
rT:215 [binder, in mathcomp.ssreflect.eqtype]
rT:22 [binder, in mathcomp.ssreflect.ssrfun]
rT:253 [binder, in mathcomp.solvable.nilpotent]
rT:256 [binder, in mathcomp.solvable.nilpotent]
rT:260 [binder, in mathcomp.fingroup.quotient]
rT:27 [binder, in mathcomp.ssreflect.ssrfun]
rT:28 [binder, in mathcomp.fingroup.action]
rT:32 [binder, in mathcomp.ssreflect.finfun]
rT:32 [binder, in mathcomp.ssreflect.ssrfun]
rT:35 [binder, in mathcomp.ssreflect.finfun]
rT:38 [binder, in mathcomp.ssreflect.ssrfun]
rT:39 [binder, in mathcomp.solvable.maximal]
rT:40 [binder, in mathcomp.field.fieldext]
rT:412 [binder, in mathcomp.fingroup.morphism]
rT:419 [binder, in mathcomp.fingroup.morphism]
rT:425 [binder, in mathcomp.fingroup.morphism]
rT:427 [binder, in mathcomp.solvable.abelian]
rT:429 [binder, in mathcomp.fingroup.morphism]
rT:43 [binder, in mathcomp.field.fieldext]
rT:437 [binder, in mathcomp.fingroup.morphism]
rT:44 [binder, in mathcomp.ssreflect.ssrfun]
rT:441 [binder, in mathcomp.fingroup.morphism]
rT:442 [binder, in mathcomp.solvable.abelian]
rT:445 [binder, in mathcomp.fingroup.morphism]
rT:446 [binder, in mathcomp.solvable.abelian]
rT:449 [binder, in mathcomp.fingroup.morphism]
rT:45 [binder, in mathcomp.solvable.maximal]
rT:455 [binder, in mathcomp.fingroup.morphism]
rT:46 [binder, in mathcomp.field.fieldext]
rT:460 [binder, in mathcomp.fingroup.morphism]
rT:466 [binder, in mathcomp.solvable.pgroup]
rT:473 [binder, in mathcomp.solvable.pgroup]
rT:49 [binder, in mathcomp.solvable.maximal]
rT:521 [binder, in mathcomp.ssreflect.finset]
rT:529 [binder, in mathcomp.ssreflect.finset]
rT:539 [binder, in mathcomp.ssreflect.finset]
rT:543 [binder, in mathcomp.ssreflect.finset]
rT:548 [binder, in mathcomp.ssreflect.finset]
rT:57 [binder, in mathcomp.fingroup.presentation]
rT:59 [binder, in mathcomp.solvable.center]
rT:595 [binder, in mathcomp.algebra.vector]
rT:599 [binder, in mathcomp.solvable.pgroup]
rT:637 [binder, in mathcomp.ssreflect.fintype]
rT:67 [binder, in mathcomp.solvable.maximal]
rT:671 [binder, in mathcomp.algebra.vector]
rT:674 [binder, in mathcomp.algebra.vector]
rT:679 [binder, in mathcomp.algebra.vector]
rT:684 [binder, in mathcomp.algebra.vector]
rT:687 [binder, in mathcomp.algebra.vector]
rT:69 [binder, in mathcomp.fingroup.presentation]
rT:690 [binder, in mathcomp.algebra.vector]
rT:694 [binder, in mathcomp.algebra.vector]
rT:70 [binder, in mathcomp.solvable.gseries]
rT:71 [binder, in mathcomp.fingroup.presentation]
rT:82 [binder, in mathcomp.ssreflect.finfun]
rT:83 [binder, in mathcomp.ssreflect.finfun]
rT:84 [binder, in mathcomp.ssreflect.finfun]
rT:85 [binder, in mathcomp.ssreflect.finfun]
rT:86 [binder, in mathcomp.ssreflect.finfun]
rT:864 [binder, in mathcomp.character.classfun]
rT:868 [binder, in mathcomp.character.classfun]
rT:87 [binder, in mathcomp.ssreflect.finfun]
rT:87 [binder, in mathcomp.fingroup.presentation]
rT:88 [binder, in mathcomp.ssreflect.finfun]
rT:884 [binder, in mathcomp.algebra.vector]
rT:886 [binder, in mathcomp.algebra.vector]
rT:89 [binder, in mathcomp.ssreflect.finfun]
rT:90 [binder, in mathcomp.ssreflect.finfun]
rT:91 [binder, in mathcomp.ssreflect.finfun]
rT:92 [binder, in mathcomp.ssreflect.finfun]
rT:92 [binder, in mathcomp.fingroup.presentation]
rT:925 [binder, in mathcomp.ssreflect.finset]
rT:93 [binder, in mathcomp.ssreflect.finfun]
rT:99 [binder, in mathcomp.fingroup.presentation]
rU [abbreviation, in mathcomp.character.mxrepresentation]
rU' [abbreviation, in mathcomp.character.mxrepresentation]
rU:119 [binder, in mathcomp.character.character]
rU:127 [binder, in mathcomp.character.character]
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]
rVpoly [definition, in mathcomp.algebra.mxpoly]
rVpolyK [lemma, in mathcomp.algebra.mxpoly]
rVpoly_linear [definition, in mathcomp.algebra.mxpoly]
rVpoly_additive [definition, 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_eqP [lemma, in mathcomp.algebra.mxalgebra]
rV_subP [lemma, in mathcomp.algebra.mxalgebra]
rV0Pn [lemma, in mathcomp.algebra.matrix]
rV:120 [binder, in mathcomp.character.character]
rv:178 [binder, in mathcomp.algebra.vector]
rv:19 [binder, in mathcomp.field.finfield]
rV:288 [binder, in mathcomp.algebra.ssrint]
rw:1039 [binder, in mathcomp.algebra.vector]
rw:1043 [binder, in mathcomp.algebra.vector]
rW:149 [binder, in mathcomp.character.character]
rW:156 [binder, in mathcomp.character.character]
rxx:227 [binder, in mathcomp.ssreflect.generic_quotient]
Rx:159 [binder, in mathcomp.field.algebraics_fundamentals]
rX:175 [binder, in mathcomp.solvable.finmodule]
rX:188 [binder, in mathcomp.solvable.finmodule]
rz:214 [binder, in mathcomp.field.galois]
R_G [abbreviation, in mathcomp.character.integral_char]
r_a:519 [binder, in mathcomp.field.galois]
R_:3422 [binder, in mathcomp.algebra.matrix]
r_:3233 [binder, in mathcomp.algebra.matrix]
R_:3203 [binder, in mathcomp.algebra.matrix]
R_:3196 [binder, in mathcomp.algebra.matrix]
R_:3184 [binder, in mathcomp.algebra.matrix]
R_:2991 [binder, in mathcomp.algebra.matrix]
R_:2972 [binder, in mathcomp.algebra.matrix]
R_:2946 [binder, in mathcomp.algebra.matrix]
R_:2932 [binder, in mathcomp.algebra.matrix]
R_:2927 [binder, in mathcomp.algebra.matrix]
R_:2920 [binder, in mathcomp.algebra.matrix]
R_:2889 [binder, in mathcomp.algebra.matrix]
R_G [abbreviation, in mathcomp.character.mxrepresentation]
R_G [abbreviation, in mathcomp.character.mxrepresentation]
r_:848 [binder, in mathcomp.ssreflect.bigop]
r_:837 [binder, in mathcomp.ssreflect.bigop]
R_:1777 [binder, in mathcomp.algebra.mxalgebra]
R_:1586 [binder, in mathcomp.algebra.mxalgebra]
R'_:2933 [binder, in mathcomp.algebra.matrix]
R'_:2921 [binder, in mathcomp.algebra.matrix]
r':1702 [binder, in mathcomp.ssreflect.order]
r':1714 [binder, in mathcomp.ssreflect.order]
r':1726 [binder, in mathcomp.ssreflect.order]
r':1741 [binder, in mathcomp.ssreflect.order]
R':2022 [binder, in mathcomp.ssreflect.seq]
r':2281 [binder, in mathcomp.ssreflect.seq]
r':2289 [binder, in mathcomp.ssreflect.seq]
r':2299 [binder, in mathcomp.ssreflect.seq]
r':2305 [binder, in mathcomp.ssreflect.seq]
r':2343 [binder, in mathcomp.ssreflect.seq]
r':2383 [binder, in mathcomp.ssreflect.seq]
r':2387 [binder, in mathcomp.ssreflect.seq]
r':2392 [binder, in mathcomp.ssreflect.seq]
r':2396 [binder, in mathcomp.ssreflect.seq]
r':2404 [binder, in mathcomp.ssreflect.seq]
R':557 [binder, in mathcomp.algebra.ssrint]
R':759 [binder, in mathcomp.algebra.ssrint]
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]
r1:1079 [binder, in mathcomp.ssreflect.bigop]
r1:12 [binder, in mathcomp.algebra.polydiv]
r1:1235 [binder, in mathcomp.algebra.mxalgebra]
r1:131 [binder, in mathcomp.field.closed_field]
r1:1362 [binder, in mathcomp.ssreflect.bigop]
r1:1380 [binder, in mathcomp.ssreflect.bigop]
r1:1397 [binder, in mathcomp.ssreflect.bigop]
r1:143 [binder, in mathcomp.field.closed_field]
R1:1566 [binder, in mathcomp.algebra.mxalgebra]
R1:1572 [binder, in mathcomp.algebra.mxalgebra]
R1:1579 [binder, in mathcomp.algebra.mxalgebra]
R1:1608 [binder, in mathcomp.algebra.mxalgebra]
R1:1616 [binder, in mathcomp.algebra.mxalgebra]
R1:1621 [binder, in mathcomp.algebra.mxalgebra]
R1:1629 [binder, in mathcomp.algebra.mxalgebra]
R1:1639 [binder, in mathcomp.algebra.mxalgebra]
R1:1648 [binder, in mathcomp.algebra.mxalgebra]
R1:1656 [binder, in mathcomp.algebra.mxalgebra]
r1:1668 [binder, in mathcomp.ssreflect.seq]
R1:1673 [binder, in mathcomp.algebra.mxalgebra]
R1:1680 [binder, in mathcomp.algebra.mxalgebra]
R1:1687 [binder, in mathcomp.algebra.mxalgebra]
R1:1693 [binder, in mathcomp.algebra.mxalgebra]
R1:1701 [binder, in mathcomp.algebra.mxalgebra]
R1:1706 [binder, in mathcomp.algebra.mxalgebra]
R1:1711 [binder, in mathcomp.algebra.mxalgebra]
R1:1771 [binder, in mathcomp.algebra.mxalgebra]
r1:1772 [binder, in mathcomp.ssreflect.bigop]
r1:1790 [binder, in mathcomp.ssreflect.bigop]
r1:1807 [binder, in mathcomp.ssreflect.bigop]
r1:182 [binder, in mathcomp.field.separable]
r1:2002 [binder, in mathcomp.ssreflect.bigop]
r1:2068 [binder, in mathcomp.ssreflect.bigop]
R1:2714 [binder, in mathcomp.algebra.ssralg]
r1:286 [binder, in mathcomp.fingroup.gproduct]
r1:370 [binder, in mathcomp.algebra.intdiv]
r1:372 [binder, in mathcomp.algebra.intdiv]
r1:374 [binder, in mathcomp.algebra.intdiv]
R1:46 [binder, in mathcomp.field.cyclotomic]
R1:482 [binder, in mathcomp.character.classfun]
R1:486 [binder, in mathcomp.character.classfun]
r1:511 [binder, in mathcomp.ssreflect.div]
r1:513 [binder, in mathcomp.ssreflect.div]
r1:515 [binder, in mathcomp.ssreflect.div]
r1:521 [binder, in mathcomp.ssreflect.bigop]
r1:588 [binder, in mathcomp.ssreflect.bigop]
r1:602 [binder, in mathcomp.ssreflect.bigop]
r1:612 [binder, in mathcomp.ssreflect.bigop]
r2 [definition, in mathcomp.solvable.burnside_app]
R2 [definition, in mathcomp.solvable.burnside_app]
r2v:41 [binder, in mathcomp.algebra.vector]
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]
r2:1080 [binder, in mathcomp.ssreflect.bigop]
r2:1236 [binder, in mathcomp.algebra.mxalgebra]
r2:1363 [binder, in mathcomp.ssreflect.bigop]
r2:1382 [binder, in mathcomp.ssreflect.bigop]
r2:1398 [binder, in mathcomp.ssreflect.bigop]
R2:1567 [binder, in mathcomp.algebra.mxalgebra]
R2:1573 [binder, in mathcomp.algebra.mxalgebra]
R2:1580 [binder, in mathcomp.algebra.mxalgebra]
R2:1609 [binder, in mathcomp.algebra.mxalgebra]
R2:1617 [binder, in mathcomp.algebra.mxalgebra]
R2:1622 [binder, in mathcomp.algebra.mxalgebra]
R2:1630 [binder, in mathcomp.algebra.mxalgebra]
R2:1640 [binder, in mathcomp.algebra.mxalgebra]
R2:1649 [binder, in mathcomp.algebra.mxalgebra]
R2:1657 [binder, in mathcomp.algebra.mxalgebra]
r2:1670 [binder, in mathcomp.ssreflect.seq]
R2:1674 [binder, in mathcomp.algebra.mxalgebra]
R2:1681 [binder, in mathcomp.algebra.mxalgebra]
R2:1688 [binder, in mathcomp.algebra.mxalgebra]
R2:1697 [binder, in mathcomp.algebra.mxalgebra]
R2:1702 [binder, in mathcomp.algebra.mxalgebra]
R2:1707 [binder, in mathcomp.algebra.mxalgebra]
R2:1712 [binder, in mathcomp.algebra.mxalgebra]
R2:1772 [binder, in mathcomp.algebra.mxalgebra]
r2:1773 [binder, in mathcomp.ssreflect.bigop]
r2:1792 [binder, in mathcomp.ssreflect.bigop]
r2:1808 [binder, in mathcomp.ssreflect.bigop]
r2:2003 [binder, in mathcomp.ssreflect.bigop]
r2:2069 [binder, in mathcomp.ssreflect.bigop]
R2:2715 [binder, in mathcomp.algebra.ssralg]
r2:287 [binder, in mathcomp.fingroup.gproduct]
r2:371 [binder, in mathcomp.algebra.intdiv]
r2:373 [binder, in mathcomp.algebra.intdiv]
r2:375 [binder, in mathcomp.algebra.intdiv]
R2:47 [binder, in mathcomp.field.cyclotomic]
R2:483 [binder, in mathcomp.character.classfun]
R2:487 [binder, in mathcomp.character.classfun]
r2:512 [binder, in mathcomp.ssreflect.div]
r2:514 [binder, in mathcomp.ssreflect.div]
r2:516 [binder, in mathcomp.ssreflect.div]
r2:522 [binder, in mathcomp.ssreflect.bigop]
r2:589 [binder, in mathcomp.ssreflect.bigop]
r2:603 [binder, in mathcomp.ssreflect.bigop]
r2:613 [binder, in mathcomp.ssreflect.bigop]
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]
R3:1641 [binder, in mathcomp.algebra.mxalgebra]
R3:1650 [binder, in mathcomp.algebra.mxalgebra]
R3:1675 [binder, in mathcomp.algebra.mxalgebra]
R3:1682 [binder, in mathcomp.algebra.mxalgebra]
R3:1689 [binder, in mathcomp.algebra.mxalgebra]
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]
R4:1642 [binder, in mathcomp.algebra.mxalgebra]
R4:1651 [binder, in mathcomp.algebra.mxalgebra]
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]
R:1 [binder, in mathcomp.algebra.ssrnum]
r:1009 [binder, in mathcomp.algebra.polydiv]
r:1009 [binder, in mathcomp.fingroup.fingroup]
r:1011 [binder, in mathcomp.algebra.matrix]
r:1012 [binder, in mathcomp.algebra.poly]
r:1014 [binder, in mathcomp.algebra.polydiv]
r:1019 [binder, in mathcomp.fingroup.fingroup]
R:102 [binder, in mathcomp.algebra.countalg]
R:1021 [binder, in mathcomp.character.character]
r:1029 [binder, in mathcomp.algebra.polydiv]
r:1029 [binder, in mathcomp.ssreflect.bigop]
r:103 [binder, in mathcomp.algebra.polyXY]
r:103 [binder, in mathcomp.solvable.nilpotent]
r:1035 [binder, in mathcomp.ssreflect.bigop]
r:1039 [binder, in mathcomp.algebra.poly]
r:104 [binder, in mathcomp.algebra.polyXY]
r:104 [binder, in mathcomp.algebra.poly]
r:1042 [binder, in mathcomp.algebra.poly]
r:1043 [binder, in mathcomp.ssreflect.bigop]
r:1045 [binder, in mathcomp.algebra.ssralg]
R:1053 [binder, in mathcomp.algebra.poly]
R:1054 [binder, in mathcomp.algebra.poly]
r:1055 [binder, in mathcomp.ssreflect.bigop]
R:106 [binder, in mathcomp.solvable.pgroup]
r:1065 [binder, in mathcomp.algebra.vector]
r:1067 [binder, in mathcomp.algebra.vector]
r:1069 [binder, in mathcomp.ssreflect.bigop]
r:107 [binder, in mathcomp.character.inertia]
R:107 [binder, in mathcomp.algebra.ssrnum]
R:107 [binder, in mathcomp.fingroup.morphism]
r:108 [binder, in mathcomp.algebra.polydiv]
R:108 [binder, in mathcomp.algebra.finalg]
R:109 [binder, in mathcomp.fingroup.morphism]
r:1097 [binder, in mathcomp.ssreflect.finset]
R:11 [binder, in mathcomp.field.cyclotomic]
r:11 [binder, in mathcomp.field.algnum]
R:110 [binder, in mathcomp.solvable.pgroup]
R:111 [binder, in mathcomp.fingroup.morphism]
R:111 [binder, in mathcomp.ssreflect.eqtype]
r:1113 [binder, in mathcomp.ssreflect.bigop]
R:112 [binder, in mathcomp.algebra.finalg]
R:112 [binder, in mathcomp.algebra.ssrnum]
R:1126 [binder, in mathcomp.algebra.ssralg]
r:1134 [binder, in mathcomp.ssreflect.bigop]
r:1135 [binder, in mathcomp.ssreflect.finset]
R:1135 [binder, in mathcomp.algebra.ssralg]
R:114 [binder, in mathcomp.ssreflect.finfun]
R:114 [binder, in mathcomp.algebra.finalg]
r:1145 [binder, in mathcomp.ssreflect.finset]
r:1145 [binder, in mathcomp.fingroup.fingroup]
R:115 [binder, in mathcomp.solvable.gfunctor]
r:115 [binder, in mathcomp.solvable.nilpotent]
r:1156 [binder, in mathcomp.fingroup.fingroup]
r:1159 [binder, in mathcomp.algebra.ssralg]
R:116 [binder, in mathcomp.algebra.finalg]
R:116 [binder, in mathcomp.ssreflect.eqtype]
R:1160 [binder, in mathcomp.algebra.poly]
R:1161 [binder, in mathcomp.algebra.poly]
R:1162 [binder, in mathcomp.algebra.poly]
R:1163 [binder, in mathcomp.algebra.poly]
R:1164 [binder, in mathcomp.algebra.poly]
R:1165 [binder, in mathcomp.algebra.poly]
r:1169 [binder, in mathcomp.algebra.ssralg]
r:1172 [binder, in mathcomp.ssreflect.finset]
r:118 [binder, in mathcomp.ssreflect.tuple]
R:118 [binder, in mathcomp.algebra.ssrnum]
r:118 [binder, in mathcomp.algebra.ssralg]
r:12 [binder, in mathcomp.ssreflect.div]
r:12 [binder, in mathcomp.field.algnum]
r:120 [binder, in mathcomp.ssreflect.tuple]
R:120 [binder, in mathcomp.solvable.sylow]
r:120 [binder, in mathcomp.field.finfield]
R:120 [binder, in mathcomp.solvable.gseries]
R:120 [binder, in mathcomp.solvable.gfunctor]
r:1202 [binder, in mathcomp.algebra.poly]
r:1206 [binder, in mathcomp.algebra.poly]
R:121 [binder, in mathcomp.algebra.mxpoly]
r:121 [binder, in mathcomp.field.finfield]
R:122 [binder, in mathcomp.algebra.finalg]
R:122 [binder, in mathcomp.solvable.gseries]
r:123 [binder, in mathcomp.field.finfield]
r:124 [binder, in mathcomp.field.closed_field]
R:1245 [binder, in mathcomp.algebra.ssralg]
r:125 [binder, in mathcomp.algebra.interval]
R:126 [binder, in mathcomp.algebra.finalg]
r:1260 [binder, in mathcomp.algebra.mxalgebra]
r:127 [binder, in mathcomp.solvable.burnside_app]
r:1271 [binder, in mathcomp.algebra.ssrnum]
r:1271 [binder, in mathcomp.algebra.poly]
r:1274 [binder, in mathcomp.algebra.ssralg]
R:128 [binder, in mathcomp.algebra.finalg]
r:128 [binder, in mathcomp.algebra.ssralg]
R:13 [binder, in mathcomp.algebra.ssrnum]
r:130 [binder, in mathcomp.algebra.polydiv]
r:1308 [binder, in mathcomp.ssreflect.bigop]
R:1318 [binder, in mathcomp.algebra.ssralg]
r:1318 [binder, in mathcomp.ssreflect.bigop]
r:132 [binder, in mathcomp.ssreflect.prime]
R:132 [binder, in mathcomp.algebra.ssrnum]
R:1324 [binder, in mathcomp.algebra.ssralg]
r:1329 [binder, in mathcomp.ssreflect.seq]
r:1329 [binder, in mathcomp.ssreflect.bigop]
r:133 [binder, in mathcomp.solvable.burnside_app]
r:133 [binder, in mathcomp.algebra.mxalgebra]
R:1331 [binder, in mathcomp.algebra.ssralg]
r:134 [binder, in mathcomp.algebra.polydiv]
R:134 [binder, in mathcomp.algebra.finalg]
r:134 [binder, in mathcomp.algebra.poly]
r:1340 [binder, in mathcomp.ssreflect.bigop]
R:1346 [binder, in mathcomp.algebra.ssralg]
R:1348 [binder, in mathcomp.algebra.ssralg]
r:1349 [binder, in mathcomp.algebra.matrix]
R:1349 [binder, in mathcomp.algebra.ssralg]
R:1350 [binder, in mathcomp.algebra.ssralg]
r:1351 [binder, in mathcomp.ssreflect.bigop]
r:1356 [binder, in mathcomp.algebra.matrix]
r:1358 [binder, in mathcomp.algebra.matrix]
r:136 [binder, in mathcomp.algebra.polydiv]
r:138 [binder, in mathcomp.field.closed_field]
R:138 [binder, in mathcomp.algebra.finalg]
r:139 [binder, in mathcomp.algebra.polydiv]
R:139 [binder, in mathcomp.algebra.ssrint]
r:139 [binder, in mathcomp.algebra.mxalgebra]
r:14 [binder, in mathcomp.solvable.burnside_app]
R:140 [binder, in mathcomp.algebra.finalg]
R:141 [binder, in mathcomp.fingroup.morphism]
r:142 [binder, in mathcomp.algebra.ssralg]
r:1426 [binder, in mathcomp.ssreflect.bigop]
r:143 [binder, in mathcomp.algebra.polydiv]
R:143 [binder, in mathcomp.algebra.ssrint]
r:143 [binder, in mathcomp.solvable.nilpotent]
R:1433 [binder, in mathcomp.algebra.ssralg]
R:1437 [binder, in mathcomp.algebra.ssralg]
r:1440 [binder, in mathcomp.ssreflect.bigop]
r:1450 [binder, in mathcomp.ssreflect.bigop]
R:1453 [binder, in mathcomp.algebra.ssralg]
R:146 [binder, in mathcomp.algebra.ssrint]
R:146 [binder, in mathcomp.fingroup.morphism]
r:147 [binder, in mathcomp.algebra.polydiv]
R:1471 [binder, in mathcomp.algebra.ssralg]
R:1473 [binder, in mathcomp.algebra.ssralg]
r:148 [binder, in mathcomp.field.closed_field]
R:149 [binder, in mathcomp.fingroup.morphism]
r:15 [binder, in mathcomp.solvable.burnside_app]
R:151 [binder, in mathcomp.ssreflect.finfun]
R:151 [binder, in mathcomp.algebra.ssrnum]
R:1515 [binder, in mathcomp.algebra.ssralg]
R:152 [binder, in mathcomp.fingroup.morphism]
R:1523 [binder, in mathcomp.algebra.ssralg]
R:1527 [binder, in mathcomp.algebra.ssralg]
R:153 [binder, in mathcomp.fingroup.morphism]
R:1531 [binder, in mathcomp.algebra.ssralg]
R:1535 [binder, in mathcomp.algebra.ssralg]
R:154 [binder, in mathcomp.field.algebraics_fundamentals]
r:154 [binder, in mathcomp.algebra.ssralg]
R:1540 [binder, in mathcomp.algebra.ssralg]
R:1544 [binder, in mathcomp.algebra.ssralg]
R:1548 [binder, in mathcomp.algebra.ssralg]
r:155 [binder, in mathcomp.field.closed_field]
R:155 [binder, in mathcomp.fingroup.morphism]
R:1553 [binder, in mathcomp.algebra.ssralg]
R:1557 [binder, in mathcomp.algebra.ssralg]
R:1558 [binder, in mathcomp.algebra.mxalgebra]
R:1562 [binder, in mathcomp.algebra.ssralg]
R:1564 [binder, in mathcomp.algebra.ssralg]
R:1566 [binder, in mathcomp.algebra.ssralg]
R:1568 [binder, in mathcomp.algebra.ssralg]
R:157 [binder, in mathcomp.algebra.ssrnum]
R:1571 [binder, in mathcomp.algebra.ssralg]
R:1573 [binder, in mathcomp.algebra.ssralg]
R:1575 [binder, in mathcomp.algebra.ssralg]
R:1578 [binder, in mathcomp.algebra.ssralg]
r:158 [binder, in mathcomp.ssreflect.binomial]
R:1580 [binder, in mathcomp.algebra.ssralg]
R:1583 [binder, in mathcomp.algebra.ssralg]
R:1586 [binder, in mathcomp.algebra.ssralg]
R:1589 [binder, in mathcomp.algebra.ssralg]
R:1592 [binder, in mathcomp.algebra.ssralg]
R:1595 [binder, in mathcomp.algebra.ssralg]
R:1598 [binder, in mathcomp.algebra.ssralg]
r:16 [binder, in mathcomp.solvable.burnside_app]
R:1601 [binder, in mathcomp.algebra.ssralg]
R:1602 [binder, in mathcomp.algebra.mxalgebra]
r:1604 [binder, in mathcomp.ssreflect.seq]
R:1605 [binder, in mathcomp.algebra.ssralg]
R:1608 [binder, in mathcomp.algebra.ssralg]
R:1620 [binder, in mathcomp.algebra.ssralg]
R:1624 [binder, in mathcomp.algebra.ssralg]
R:1629 [binder, in mathcomp.algebra.ssralg]
R:163 [binder, in mathcomp.algebra.finalg]
R:163 [binder, in mathcomp.fingroup.morphism]
R:1631 [binder, in mathcomp.algebra.mxalgebra]
R:1639 [binder, in mathcomp.algebra.ssralg]
r:164 [binder, in mathcomp.field.closed_field]
R:164 [binder, in mathcomp.fingroup.morphism]
r:1646 [binder, in mathcomp.ssreflect.seq]
R:1646 [binder, in mathcomp.algebra.ssralg]
R:1650 [binder, in mathcomp.algebra.ssralg]
R:1654 [binder, in mathcomp.algebra.ssralg]
r:1656 [binder, in mathcomp.ssreflect.seq]
r:1657 [binder, in mathcomp.algebra.matrix]
R:1658 [binder, in mathcomp.algebra.ssralg]
r:1659 [binder, in mathcomp.ssreflect.seq]
r:1659 [binder, in mathcomp.ssreflect.bigop]
r:1663 [binder, in mathcomp.ssreflect.bigop]
r:1664 [binder, in mathcomp.ssreflect.seq]
R:1664 [binder, in mathcomp.algebra.ssralg]
R:1669 [binder, in mathcomp.algebra.ssralg]
r:1669 [binder, in mathcomp.ssreflect.bigop]
r:167 [binder, in mathcomp.solvable.sylow]
r:1671 [binder, in mathcomp.algebra.matrix]
R:1674 [binder, in mathcomp.algebra.ssralg]
r:1675 [binder, in mathcomp.ssreflect.order]
R:168 [binder, in mathcomp.algebra.mxpoly]
R:168 [binder, in mathcomp.character.inertia]
R:1681 [binder, in mathcomp.algebra.ssralg]
R:1687 [binder, in mathcomp.algebra.ssralg]
r:1688 [binder, in mathcomp.ssreflect.order]
r:1690 [binder, in mathcomp.ssreflect.bigop]
r:1696 [binder, in mathcomp.ssreflect.bigop]
r:17 [binder, in mathcomp.fingroup.presentation]
R:170 [binder, in mathcomp.algebra.ssrnum]
r:1701 [binder, in mathcomp.ssreflect.order]
r:1704 [binder, in mathcomp.ssreflect.bigop]
R:1705 [binder, in mathcomp.algebra.ssralg]
r:1713 [binder, in mathcomp.ssreflect.order]
R:1715 [binder, in mathcomp.algebra.ssralg]
R:1715 [binder, in mathcomp.algebra.mxalgebra]
r:1718 [binder, in mathcomp.ssreflect.bigop]
R:1720 [binder, in mathcomp.algebra.ssralg]
R:1721 [binder, in mathcomp.algebra.mxalgebra]
R:1724 [binder, in mathcomp.algebra.mxalgebra]
r:1725 [binder, in mathcomp.ssreflect.order]
R:1725 [binder, in mathcomp.algebra.ssralg]
R:1727 [binder, in mathcomp.algebra.mxalgebra]
r:1728 [binder, in mathcomp.ssreflect.bigop]
R:173 [binder, in mathcomp.fingroup.morphism]
R:1730 [binder, in mathcomp.algebra.ssralg]
R:1736 [binder, in mathcomp.algebra.ssralg]
R:1737 [binder, in mathcomp.algebra.mxalgebra]
r:1739 [binder, in mathcomp.ssreflect.bigop]
r:174 [binder, in mathcomp.field.galois]
r:174 [binder, in mathcomp.fingroup.fingroup]
r:1740 [binder, in mathcomp.ssreflect.order]
R:1741 [binder, in mathcomp.algebra.ssralg]
R:1743 [binder, in mathcomp.algebra.mxalgebra]
R:1746 [binder, in mathcomp.algebra.ssralg]
R:1748 [binder, in mathcomp.algebra.mxalgebra]
r:175 [binder, in mathcomp.ssreflect.generic_quotient]
r:1750 [binder, in mathcomp.ssreflect.bigop]
R:1751 [binder, in mathcomp.algebra.mxalgebra]
R:1752 [binder, in mathcomp.algebra.ssralg]
r:1755 [binder, in mathcomp.ssreflect.order]
R:1755 [binder, in mathcomp.algebra.mxalgebra]
R:1757 [binder, in mathcomp.algebra.ssralg]
R:1759 [binder, in mathcomp.algebra.mxalgebra]
r:176 [binder, in mathcomp.field.closed_field]
r:1761 [binder, in mathcomp.ssreflect.bigop]
R:1764 [binder, in mathcomp.algebra.mxalgebra]
R:1767 [binder, in mathcomp.algebra.mxalgebra]
r:1768 [binder, in mathcomp.ssreflect.order]
r:177 [binder, in mathcomp.algebra.polydiv]
r:1770 [binder, in mathcomp.algebra.ssralg]
R:1776 [binder, in mathcomp.algebra.mxalgebra]
r:18 [binder, in mathcomp.ssreflect.div]
r:18 [binder, in mathcomp.algebra.mxpoly]
r:18 [binder, in mathcomp.solvable.burnside_app]
R:180 [binder, in mathcomp.ssreflect.finfun]
R:181 [binder, in mathcomp.ssreflect.finfun]
R:181 [binder, in mathcomp.algebra.mxpoly]
r:181 [binder, in mathcomp.field.closed_field]
r:1810 [binder, in mathcomp.algebra.ssralg]
R:182 [binder, in mathcomp.ssreflect.binomial]
r:184 [binder, in mathcomp.ssreflect.generic_quotient]
R:185 [binder, in mathcomp.algebra.ssrnum]
r:186 [binder, in mathcomp.character.character]
r:1865 [binder, in mathcomp.algebra.matrix]
R:187 [binder, in mathcomp.algebra.mxpoly]
r:1870 [binder, in mathcomp.algebra.matrix]
r:1872 [binder, in mathcomp.algebra.matrix]
r:1874 [binder, in mathcomp.algebra.matrix]
r:1877 [binder, in mathcomp.algebra.matrix]
r:188 [binder, in mathcomp.ssreflect.prime]
r:1880 [binder, in mathcomp.algebra.matrix]
r:1883 [binder, in mathcomp.algebra.matrix]
r:1886 [binder, in mathcomp.algebra.matrix]
r:1891 [binder, in mathcomp.algebra.matrix]
r:1895 [binder, in mathcomp.algebra.matrix]
r:1897 [binder, in mathcomp.algebra.matrix]
r:19 [binder, in mathcomp.solvable.burnside_app]
r:1900 [binder, in mathcomp.algebra.matrix]
r:1903 [binder, in mathcomp.algebra.matrix]
r:1905 [binder, in mathcomp.algebra.matrix]
R:192 [binder, in mathcomp.algebra.mxpoly]
R:192 [binder, in mathcomp.solvable.cyclic]
r:1926 [binder, in mathcomp.algebra.ssralg]
r:1931 [binder, in mathcomp.algebra.ssralg]
r:1935 [binder, in mathcomp.algebra.ssralg]
R:194 [binder, in mathcomp.fingroup.morphism]
R:195 [binder, in mathcomp.fingroup.morphism]
r:1955 [binder, in mathcomp.algebra.ssralg]
r:1959 [binder, in mathcomp.algebra.ssralg]
R:197 [binder, in mathcomp.fingroup.morphism]
r:1976 [binder, in mathcomp.ssreflect.bigop]
r:1977 [binder, in mathcomp.ssreflect.bigop]
r:1978 [binder, in mathcomp.ssreflect.bigop]
r:198 [binder, in mathcomp.field.separable]
r:198 [binder, in mathcomp.character.classfun]
r:1985 [binder, in mathcomp.ssreflect.bigop]
R:199 [binder, in mathcomp.fingroup.morphism]
r:2 [binder, in mathcomp.ssreflect.prime]
R:202 [binder, in mathcomp.algebra.ring_quotient]
R:202 [binder, in mathcomp.algebra.mxpoly]
r:202 [binder, in mathcomp.algebra.ssrint]
r:202 [binder, in mathcomp.solvable.nilpotent]
R:2021 [binder, in mathcomp.ssreflect.seq]
R:203 [binder, in mathcomp.algebra.ssralg]
r:2036 [binder, in mathcomp.ssreflect.bigop]
R:2046 [binder, in mathcomp.ssreflect.seq]
r:2047 [binder, in mathcomp.ssreflect.bigop]
R:205 [binder, in mathcomp.fingroup.morphism]
R:2053 [binder, in mathcomp.algebra.ssralg]
R:2056 [binder, in mathcomp.algebra.ssralg]
r:2058 [binder, in mathcomp.ssreflect.bigop]
R:206 [binder, in mathcomp.algebra.ring_quotient]
R:206 [binder, in mathcomp.algebra.mxpoly]
R:2069 [binder, in mathcomp.algebra.matrix]
R:207 [binder, in mathcomp.fingroup.morphism]
R:207 [binder, in mathcomp.algebra.ssralg]
R:2078 [binder, in mathcomp.algebra.matrix]
r:2079 [binder, in mathcomp.ssreflect.bigop]
R:2080 [binder, in mathcomp.algebra.matrix]
R:2083 [binder, in mathcomp.algebra.matrix]
r:2083 [binder, in mathcomp.algebra.ssralg]
R:2085 [binder, in mathcomp.algebra.matrix]
r:2089 [binder, in mathcomp.ssreflect.bigop]
R:21 [binder, in mathcomp.algebra.mxpoly]
r:210 [binder, in mathcomp.field.separable]
R:210 [binder, in mathcomp.algebra.ring_quotient]
R:210 [binder, in mathcomp.algebra.mxpoly]
r:2100 [binder, in mathcomp.algebra.ssralg]
r:2103 [binder, in mathcomp.ssreflect.bigop]
r:2104 [binder, in mathcomp.algebra.matrix]
R:211 [binder, in mathcomp.fingroup.morphism]
r:2113 [binder, in mathcomp.algebra.matrix]
R:212 [binder, in mathcomp.fingroup.morphism]
R:2129 [binder, in mathcomp.algebra.matrix]
r:213 [binder, in mathcomp.algebra.ssrint]
R:2133 [binder, in mathcomp.algebra.ssralg]
R:2135 [binder, in mathcomp.algebra.ssralg]
R:2136 [binder, in mathcomp.algebra.ssralg]
r:214 [binder, in mathcomp.solvable.nilpotent]
r:2146 [binder, in mathcomp.ssreflect.bigop]
R:215 [binder, in mathcomp.algebra.ring_quotient]
R:215 [binder, in mathcomp.solvable.maximal]
r:216 [binder, in mathcomp.character.mxrepresentation]
R:216 [binder, in mathcomp.algebra.ssralg]
R:217 [binder, in mathcomp.algebra.ring_quotient]
R:217 [binder, in mathcomp.solvable.maximal]
R:2170 [binder, in mathcomp.ssreflect.seq]
R:2173 [binder, in mathcomp.algebra.matrix]
r:2183 [binder, in mathcomp.algebra.ssralg]
R:219 [binder, in mathcomp.algebra.ring_quotient]
r:2193 [binder, in mathcomp.algebra.ssralg]
r:22 [binder, in mathcomp.fingroup.presentation]
r:2218 [binder, in mathcomp.ssreflect.order]
r:2226 [binder, in mathcomp.ssreflect.order]
R:223 [binder, in mathcomp.algebra.ring_quotient]
r:2235 [binder, in mathcomp.algebra.ssralg]
R:224 [binder, in mathcomp.fingroup.morphism]
r:2250 [binder, in mathcomp.ssreflect.order]
r:2259 [binder, in mathcomp.ssreflect.order]
r:226 [binder, in mathcomp.algebra.polydiv]
R:227 [binder, in mathcomp.algebra.ring_quotient]
r:228 [binder, in mathcomp.algebra.polydiv]
r:228 [binder, in mathcomp.field.fieldext]
r:228 [binder, in mathcomp.character.mxrepresentation]
r:228 [binder, in mathcomp.fingroup.gproduct]
r:2280 [binder, in mathcomp.ssreflect.seq]
r:2288 [binder, in mathcomp.ssreflect.seq]
R:2288 [binder, in mathcomp.algebra.ssralg]
r:229 [binder, in mathcomp.algebra.vector]
R:2292 [binder, in mathcomp.algebra.ssralg]
r:2298 [binder, in mathcomp.ssreflect.seq]
r:230 [binder, in mathcomp.field.fieldext]
r:2304 [binder, in mathcomp.ssreflect.seq]
r:2308 [binder, in mathcomp.ssreflect.seq]
r:2309 [binder, in mathcomp.ssreflect.order]
r:231 [binder, in mathcomp.field.galois]
R:231 [binder, in mathcomp.algebra.ssrnum]
R:231 [binder, in mathcomp.algebra.ssralg]
R:231 [binder, in mathcomp.ssreflect.bigop]
r:2316 [binder, in mathcomp.ssreflect.seq]
R:232 [binder, in mathcomp.character.classfun]
R:232 [binder, in mathcomp.algebra.ssralg]
r:2324 [binder, in mathcomp.ssreflect.seq]
r:233 [binder, in mathcomp.algebra.polydiv]
R:233 [binder, in mathcomp.algebra.ssrnum]
R:233 [binder, in mathcomp.algebra.ssralg]
r:2330 [binder, in mathcomp.ssreflect.order]
r:2331 [binder, in mathcomp.ssreflect.seq]
r:2338 [binder, in mathcomp.ssreflect.order]
r:2342 [binder, in mathcomp.ssreflect.seq]
R:236 [binder, in mathcomp.algebra.ssralg]
R:236 [binder, in mathcomp.solvable.maximal]
r:2362 [binder, in mathcomp.ssreflect.order]
R:2365 [binder, in mathcomp.algebra.ssralg]
r:237 [binder, in mathcomp.algebra.mxpoly]
r:237 [binder, in mathcomp.ssreflect.bigop]
r:2371 [binder, in mathcomp.ssreflect.order]
r:238 [binder, in mathcomp.algebra.mxpoly]
R:238 [binder, in mathcomp.algebra.ssrnum]
r:2382 [binder, in mathcomp.ssreflect.seq]
r:2386 [binder, in mathcomp.ssreflect.seq]
r:239 [binder, in mathcomp.algebra.mxpoly]
r:239 [binder, in mathcomp.fingroup.gproduct]
R:239 [binder, in mathcomp.algebra.ssralg]
r:2391 [binder, in mathcomp.ssreflect.seq]
r:2395 [binder, in mathcomp.ssreflect.seq]
R:2396 [binder, in mathcomp.algebra.matrix]
R:24 [binder, in mathcomp.field.finfield]
R:240 [binder, in mathcomp.algebra.ssrnum]
R:240 [binder, in mathcomp.solvable.maximal]
r:2400 [binder, in mathcomp.ssreflect.seq]
r:2403 [binder, in mathcomp.ssreflect.seq]
R:241 [binder, in mathcomp.algebra.ssralg]
r:2421 [binder, in mathcomp.ssreflect.order]
R:2429 [binder, in mathcomp.algebra.matrix]
R:2434 [binder, in mathcomp.algebra.matrix]
R:2439 [binder, in mathcomp.algebra.matrix]
R:2449 [binder, in mathcomp.algebra.ssralg]
R:2458 [binder, in mathcomp.algebra.ssralg]
R:2465 [binder, in mathcomp.algebra.ssralg]
R:2499 [binder, in mathcomp.algebra.ssralg]
R:25 [binder, in mathcomp.algebra.finalg]
R:2511 [binder, in mathcomp.algebra.ssralg]
R:2513 [binder, in mathcomp.algebra.ssralg]
R:2515 [binder, in mathcomp.algebra.ssralg]
R:2517 [binder, in mathcomp.algebra.ssralg]
R:2566 [binder, in mathcomp.algebra.matrix]
R:257 [binder, in mathcomp.algebra.ssralg]
R:2572 [binder, in mathcomp.algebra.ssrnum]
R:2574 [binder, in mathcomp.algebra.ssrnum]
r:2589 [binder, in mathcomp.algebra.matrix]
R:259 [binder, in mathcomp.algebra.ssralg]
R:2592 [binder, in mathcomp.algebra.matrix]
R:26 [binder, in mathcomp.algebra.countalg]
R:26 [binder, in mathcomp.algebra.zmodp]
r:261 [binder, in mathcomp.ssreflect.bigop]
R:262 [binder, in mathcomp.fingroup.quotient]
R:2621 [binder, in mathcomp.algebra.ssrnum]
r:2622 [binder, in mathcomp.ssreflect.order]
R:2623 [binder, in mathcomp.algebra.ssrnum]
r:263 [binder, in mathcomp.field.closed_field]
r:2632 [binder, in mathcomp.ssreflect.order]
r:2683 [binder, in mathcomp.ssreflect.bigop]
r:2696 [binder, in mathcomp.ssreflect.bigop]
r:27 [binder, in mathcomp.fingroup.presentation]
r:270 [binder, in mathcomp.algebra.ssralg]
R:271 [binder, in mathcomp.algebra.interval]
r:2713 [binder, in mathcomp.ssreflect.bigop]
R:2716 [binder, in mathcomp.algebra.ssralg]
r:272 [binder, in mathcomp.field.fieldext]
r:273 [binder, in mathcomp.solvable.extremal]
r:2731 [binder, in mathcomp.ssreflect.bigop]
r:274 [binder, in mathcomp.fingroup.gproduct]
r:2742 [binder, in mathcomp.ssreflect.bigop]
R:277 [binder, in mathcomp.fingroup.morphism]
r:28 [binder, in mathcomp.field.separable]
R:280 [binder, in mathcomp.fingroup.morphism]
r:281 [binder, in mathcomp.algebra.ssralg]
r:284 [binder, in mathcomp.algebra.ssrnum]
R:284 [binder, in mathcomp.fingroup.morphism]
r:287 [binder, in mathcomp.character.classfun]
r:288 [binder, in mathcomp.ssreflect.bigop]
R:2903 [binder, in mathcomp.ssreflect.bigop]
r:293 [binder, in mathcomp.algebra.mxalgebra]
r:2939 [binder, in mathcomp.ssreflect.bigop]
r:2945 [binder, in mathcomp.ssreflect.bigop]
r:298 [binder, in mathcomp.algebra.ssrint]
R:2981 [binder, in mathcomp.algebra.matrix]
r:2994 [binder, in mathcomp.ssreflect.bigop]
R:30 [binder, in mathcomp.algebra.countalg]
r:3019 [binder, in mathcomp.ssreflect.bigop]
r:3031 [binder, in mathcomp.ssreflect.bigop]
r:304 [binder, in mathcomp.character.classfun]
r:3055 [binder, in mathcomp.ssreflect.bigop]
r:3067 [binder, in mathcomp.ssreflect.bigop]
R:3068 [binder, in mathcomp.algebra.matrix]
r:307 [binder, in mathcomp.algebra.poly]
r:3075 [binder, in mathcomp.ssreflect.bigop]
r:308 [binder, in mathcomp.algebra.ssrint]
r:3083 [binder, in mathcomp.ssreflect.bigop]
r:3112 [binder, in mathcomp.ssreflect.bigop]
r:3129 [binder, in mathcomp.ssreflect.bigop]
r:314 [binder, in mathcomp.ssreflect.bigop]
r:315 [binder, in mathcomp.solvable.abelian]
R:3170 [binder, in mathcomp.algebra.matrix]
r:3172 [binder, in mathcomp.ssreflect.bigop]
R:32 [binder, in mathcomp.field.falgebra]
R:3227 [binder, in mathcomp.algebra.matrix]
r:3230 [binder, in mathcomp.algebra.matrix]
R:33 [binder, in mathcomp.algebra.zmodp]
R:33 [binder, in mathcomp.algebra.vector]
R:333 [binder, in mathcomp.solvable.extremal]
r:334 [binder, in mathcomp.ssreflect.bigop]
R:3383 [binder, in mathcomp.algebra.matrix]
R:34 [binder, in mathcomp.fingroup.morphism]
R:3417 [binder, in mathcomp.algebra.matrix]
R:3428 [binder, in mathcomp.algebra.matrix]
r:343 [binder, in mathcomp.character.character]
R:3443 [binder, in mathcomp.algebra.matrix]
R:3458 [binder, in mathcomp.algebra.matrix]
R:3464 [binder, in mathcomp.algebra.matrix]
r:349 [binder, in mathcomp.field.fieldext]
r:353 [binder, in mathcomp.ssreflect.bigop]
r:354 [binder, in mathcomp.algebra.polydiv]
r:356 [binder, in mathcomp.ssreflect.tuple]
r:357 [binder, in mathcomp.algebra.polydiv]
r:358 [binder, in mathcomp.ssreflect.tuple]
R:36 [binder, in mathcomp.algebra.countalg]
R:36 [binder, in mathcomp.field.separable]
R:360 [binder, in mathcomp.algebra.ssrnum]
r:365 [binder, in mathcomp.fingroup.gproduct]
R:37 [binder, in mathcomp.algebra.matrix]
R:37 [binder, in mathcomp.algebra.polyXY]
r:370 [binder, in mathcomp.ssreflect.bigop]
r:376 [binder, in mathcomp.fingroup.gproduct]
R:377 [binder, in mathcomp.algebra.mxpoly]
r:382 [binder, in mathcomp.algebra.poly]
R:383 [binder, in mathcomp.algebra.mxpoly]
r:383 [binder, in mathcomp.character.classfun]
r:383 [binder, in mathcomp.ssreflect.bigop]
r:387 [binder, in mathcomp.fingroup.gproduct]
R:393 [binder, in mathcomp.fingroup.morphism]
r:393 [binder, in mathcomp.character.character]
r:394 [binder, in mathcomp.algebra.vector]
r:395 [binder, in mathcomp.ssreflect.bigop]
R:396 [binder, in mathcomp.fingroup.morphism]
R:397 [binder, in mathcomp.field.closed_field]
R:40 [binder, in mathcomp.algebra.countalg]
R:40 [binder, in mathcomp.algebra.matrix]
R:40 [binder, in mathcomp.algebra.finalg]
R:401 [binder, in mathcomp.field.closed_field]
r:41 [binder, in mathcomp.fingroup.morphism]
r:412 [binder, in mathcomp.algebra.mxpoly]
r:413 [binder, in mathcomp.ssreflect.bigop]
r:414 [binder, in mathcomp.field.galois]
r:416 [binder, in mathcomp.character.classfun]
r:418 [binder, in mathcomp.algebra.intdiv]
r:426 [binder, in mathcomp.fingroup.gproduct]
R:43 [binder, in mathcomp.algebra.matrix]
r:432 [binder, in mathcomp.ssreflect.bigop]
r:433 [binder, in mathcomp.algebra.polydiv]
r:435 [binder, in mathcomp.algebra.intdiv]
r:436 [binder, in mathcomp.algebra.polydiv]
r:436 [binder, in mathcomp.algebra.poly]
r:437 [binder, in mathcomp.fingroup.gproduct]
r:439 [binder, in mathcomp.algebra.polydiv]
R:44 [binder, in mathcomp.algebra.finalg]
r:44 [binder, in mathcomp.algebra.vector]
R:441 [binder, in mathcomp.algebra.intdiv]
R:442 [binder, in mathcomp.algebra.intdiv]
r:442 [binder, in mathcomp.ssreflect.bigop]
r:443 [binder, in mathcomp.algebra.mxpoly]
r:444 [binder, in mathcomp.algebra.polydiv]
r:444 [binder, in mathcomp.algebra.mxpoly]
r:446 [binder, in mathcomp.field.galois]
r:447 [binder, in mathcomp.field.galois]
r:45 [binder, in mathcomp.algebra.rat]
r:45 [binder, in mathcomp.algebra.vector]
r:450 [binder, in mathcomp.algebra.ssrnum]
R:452 [binder, in mathcomp.algebra.mxpoly]
r:455 [binder, in mathcomp.ssreflect.bigop]
R:457 [binder, in mathcomp.algebra.mxpoly]
r:458 [binder, in mathcomp.algebra.ssralg]
r:459 [binder, in mathcomp.algebra.ssrnum]
r:459 [binder, in mathcomp.ssreflect.bigop]
R:46 [binder, in mathcomp.algebra.countalg]
R:46 [binder, in mathcomp.algebra.matrix]
R:46 [binder, in mathcomp.algebra.finalg]
R:462 [binder, in mathcomp.fingroup.action]
r:463 [binder, in mathcomp.field.galois]
R:464 [binder, in mathcomp.algebra.mxpoly]
R:465 [binder, in mathcomp.fingroup.action]
r:466 [binder, in mathcomp.algebra.mxpoly]
r:468 [binder, in mathcomp.field.galois]
R:468 [binder, in mathcomp.character.classfun]
r:468 [binder, in mathcomp.ssreflect.bigop]
R:47 [binder, in mathcomp.algebra.mxpoly]
r:471 [binder, in mathcomp.fingroup.fingroup]
R:472 [binder, in mathcomp.character.character]
R:473 [binder, in mathcomp.character.classfun]
r:478 [binder, in mathcomp.ssreflect.bigop]
R:48 [binder, in mathcomp.field.finfield]
R:483 [binder, in mathcomp.algebra.ssrint]
r:485 [binder, in mathcomp.fingroup.fingroup]
r:488 [binder, in mathcomp.ssreflect.bigop]
R:489 [binder, in mathcomp.character.classfun]
r:49 [binder, in mathcomp.field.cyclotomic]
R:49 [binder, in mathcomp.algebra.matrix]
r:492 [binder, in mathcomp.field.galois]
r:493 [binder, in mathcomp.field.galois]
r:497 [binder, in mathcomp.character.mxrepresentation]
r:498 [binder, in mathcomp.ssreflect.bigop]
r:5 [binder, in mathcomp.ssreflect.choice]
r:5 [binder, in mathcomp.character.mxrepresentation]
R:50 [binder, in mathcomp.algebra.countalg]
R:50 [binder, in mathcomp.field.finfield]
r:501 [binder, in mathcomp.fingroup.gproduct]
r:506 [binder, in mathcomp.algebra.polydiv]
R:508 [binder, in mathcomp.character.classfun]
r:509 [binder, in mathcomp.algebra.ssralg]
r:509 [binder, in mathcomp.ssreflect.bigop]
r:51 [binder, in mathcomp.field.separable]
R:511 [binder, in mathcomp.character.classfun]
r:512 [binder, in mathcomp.fingroup.gproduct]
R:513 [binder, in mathcomp.character.classfun]
r:517 [binder, in mathcomp.field.galois]
R:517 [binder, in mathcomp.character.classfun]
R:519 [binder, in mathcomp.character.classfun]
r:52 [binder, in mathcomp.field.separable]
R:52 [binder, in mathcomp.algebra.matrix]
R:52 [binder, in mathcomp.field.finfield]
R:530 [binder, in mathcomp.character.classfun]
R:532 [binder, in mathcomp.character.classfun]
r:537 [binder, in mathcomp.algebra.mxpoly]
r:538 [binder, in mathcomp.algebra.polydiv]
r:539 [binder, in mathcomp.algebra.polydiv]
R:54 [binder, in mathcomp.field.finfield]
R:54 [binder, in mathcomp.ssreflect.bigop]
r:540 [binder, in mathcomp.ssreflect.bigop]
r:55 [binder, in mathcomp.field.separable]
R:55 [binder, in mathcomp.algebra.matrix]
R:550 [binder, in mathcomp.ssreflect.finset]
r:550 [binder, in mathcomp.algebra.mxpoly]
r:550 [binder, in mathcomp.character.character]
r:552 [binder, in mathcomp.ssreflect.bigop]
r:555 [binder, in mathcomp.algebra.mxpoly]
r:556 [binder, in mathcomp.character.character]
R:56 [binder, in mathcomp.algebra.countalg]
R:56 [binder, in mathcomp.field.finfield]
r:562 [binder, in mathcomp.ssreflect.bigop]
r:566 [binder, in mathcomp.ssreflect.prime]
r:571 [binder, in mathcomp.ssreflect.bigop]
r:572 [binder, in mathcomp.algebra.mxpoly]
r:573 [binder, in mathcomp.algebra.mxpoly]
r:574 [binder, in mathcomp.algebra.mxpoly]
r:577 [binder, in mathcomp.ssreflect.bigop]
R:58 [binder, in mathcomp.algebra.matrix]
R:58 [binder, in mathcomp.ssreflect.bigop]
r:582 [binder, in mathcomp.ssreflect.bigop]
R:584 [binder, in mathcomp.algebra.ssrint]
r:585 [binder, in mathcomp.algebra.polydiv]
r:588 [binder, in mathcomp.algebra.polydiv]
r:597 [binder, in mathcomp.algebra.polydiv]
R:6 [binder, in mathcomp.algebra.poly]
R:60 [binder, in mathcomp.algebra.countalg]
r:600 [binder, in mathcomp.algebra.polydiv]
R:602 [binder, in mathcomp.solvable.pgroup]
R:61 [binder, in mathcomp.algebra.matrix]
R:615 [binder, in mathcomp.algebra.ssralg]
r:62 [binder, in mathcomp.field.cyclotomic]
R:62 [binder, in mathcomp.algebra.countalg]
R:62 [binder, in mathcomp.algebra.finalg]
r:624 [binder, in mathcomp.ssreflect.bigop]
r:626 [binder, in mathcomp.fingroup.fingroup]
r:63 [binder, in mathcomp.field.cyclotomic]
R:63 [binder, in mathcomp.field.finfield]
R:63 [binder, in mathcomp.ssreflect.bigop]
r:633 [binder, in mathcomp.ssreflect.bigop]
r:64 [binder, in mathcomp.field.cyclotomic]
R:64 [binder, in mathcomp.algebra.matrix]
r:643 [binder, in mathcomp.ssreflect.bigop]
R:645 [binder, in mathcomp.algebra.ssralg]
r:646 [binder, in mathcomp.algebra.polydiv]
r:648 [binder, in mathcomp.algebra.ssrnum]
r:649 [binder, in mathcomp.algebra.polydiv]
R:65 [binder, in mathcomp.field.cyclotomic]
R:65 [binder, in mathcomp.field.finfield]
r:652 [binder, in mathcomp.ssreflect.bigop]
r:656 [binder, in mathcomp.algebra.ssrnum]
R:66 [binder, in mathcomp.algebra.finalg]
R:66 [binder, in mathcomp.fingroup.morphism]
r:66 [binder, in mathcomp.ssreflect.bigop]
r:667 [binder, in mathcomp.algebra.polydiv]
r:669 [binder, in mathcomp.algebra.polydiv]
R:67 [binder, in mathcomp.field.finfield]
r:673 [binder, in mathcomp.algebra.polydiv]
r:676 [binder, in mathcomp.algebra.polydiv]
R:677 [binder, in mathcomp.solvable.abelian]
r:679 [binder, in mathcomp.algebra.ssrnum]
R:68 [binder, in mathcomp.algebra.countalg]
R:68 [binder, in mathcomp.algebra.finalg]
R:68 [binder, in mathcomp.ssreflect.bigop]
R:682 [binder, in mathcomp.solvable.abelian]
r:688 [binder, in mathcomp.algebra.ssralg]
R:69 [binder, in mathcomp.field.finfield]
R:69 [binder, in mathcomp.fingroup.morphism]
r:69 [binder, in mathcomp.solvable.center]
r:696 [binder, in mathcomp.algebra.ssrnum]
r:699 [binder, in mathcomp.algebra.ssralg]
r:7 [binder, in mathcomp.algebra.polydiv]
R:7 [binder, in mathcomp.algebra.poly]
R:70 [binder, in mathcomp.algebra.ssrnum]
R:70 [binder, in mathcomp.fingroup.morphism]
r:71 [binder, in mathcomp.character.mxabelem]
R:71 [binder, in mathcomp.field.finfield]
r:712 [binder, in mathcomp.algebra.polydiv]
R:714 [binder, in mathcomp.ssreflect.finset]
R:714 [binder, in mathcomp.algebra.ssralg]
r:716 [binder, in mathcomp.algebra.vector]
R:719 [binder, in mathcomp.character.classfun]
R:72 [binder, in mathcomp.algebra.countalg]
R:72 [binder, in mathcomp.algebra.ssrnum]
R:726 [binder, in mathcomp.algebra.ssralg]
R:73 [binder, in mathcomp.field.finfield]
r:730 [binder, in mathcomp.algebra.polydiv]
r:733 [binder, in mathcomp.algebra.polydiv]
r:736 [binder, in mathcomp.algebra.polydiv]
R:739 [binder, in mathcomp.algebra.poly]
R:74 [binder, in mathcomp.algebra.finalg]
R:74 [binder, in mathcomp.fingroup.morphism]
R:740 [binder, in mathcomp.algebra.poly]
r:741 [binder, in mathcomp.algebra.polydiv]
R:741 [binder, in mathcomp.algebra.poly]
R:742 [binder, in mathcomp.algebra.poly]
R:744 [binder, in mathcomp.algebra.ssralg]
r:749 [binder, in mathcomp.algebra.matrix]
R:75 [binder, in mathcomp.ssreflect.ssrAC]
R:758 [binder, in mathcomp.algebra.ssrint]
r:76 [binder, in mathcomp.character.classfun]
r:760 [binder, in mathcomp.algebra.polydiv]
R:762 [binder, in mathcomp.algebra.ssrint]
r:763 [binder, in mathcomp.algebra.matrix]
r:774 [binder, in mathcomp.algebra.matrix]
r:779 [binder, in mathcomp.algebra.mxpoly]
R:78 [binder, in mathcomp.algebra.countalg]
R:78 [binder, in mathcomp.algebra.finalg]
r:780 [binder, in mathcomp.algebra.mxpoly]
r:781 [binder, in mathcomp.algebra.mxpoly]
r:784 [binder, in mathcomp.algebra.matrix]
r:79 [binder, in mathcomp.solvable.nilpotent]
r:796 [binder, in mathcomp.algebra.polydiv]
r:799 [binder, in mathcomp.algebra.polydiv]
r:8 [binder, in mathcomp.ssreflect.prime]
r:8 [binder, in mathcomp.solvable.gseries]
R:8 [binder, in mathcomp.algebra.poly]
R:80 [binder, in mathcomp.ssreflect.ssrAC]
R:80 [binder, in mathcomp.algebra.finalg]
R:80 [binder, in mathcomp.fingroup.morphism]
r:802 [binder, in mathcomp.algebra.polydiv]
r:809 [binder, in mathcomp.algebra.vector]
R:82 [binder, in mathcomp.algebra.countalg]
R:82 [binder, in mathcomp.fingroup.morphism]
r:823 [binder, in mathcomp.algebra.vector]
r:826 [binder, in mathcomp.algebra.mxalgebra]
r:827 [binder, in mathcomp.algebra.polydiv]
r:828 [binder, in mathcomp.algebra.mxalgebra]
r:829 [binder, in mathcomp.algebra.polydiv]
r:829 [binder, in mathcomp.algebra.ssralg]
r:831 [binder, in mathcomp.algebra.polydiv]
r:833 [binder, in mathcomp.ssreflect.bigop]
R:84 [binder, in mathcomp.fingroup.morphism]
r:84 [binder, in mathcomp.solvable.center]
r:841 [binder, in mathcomp.algebra.mxpoly]
r:842 [binder, in mathcomp.algebra.mxpoly]
r:843 [binder, in mathcomp.algebra.mxpoly]
r:843 [binder, in mathcomp.algebra.poly]
r:845 [binder, in mathcomp.algebra.mxpoly]
r:845 [binder, in mathcomp.ssreflect.bigop]
r:846 [binder, in mathcomp.algebra.mxpoly]
r:846 [binder, in mathcomp.algebra.poly]
r:847 [binder, in mathcomp.algebra.mxpoly]
r:856 [binder, in mathcomp.ssreflect.bigop]
R:857 [binder, in mathcomp.algebra.ssrint]
r:859 [binder, in mathcomp.algebra.polydiv]
R:862 [binder, in mathcomp.algebra.ssrint]
R:869 [binder, in mathcomp.algebra.ssrint]
R:87 [binder, in mathcomp.solvable.pgroup]
R:87 [binder, in mathcomp.solvable.hall]
R:870 [binder, in mathcomp.character.classfun]
r:874 [binder, in mathcomp.algebra.polydiv]
R:874 [binder, in mathcomp.algebra.matrix]
R:875 [binder, in mathcomp.algebra.ssrint]
r:878 [binder, in mathcomp.algebra.polydiv]
R:88 [binder, in mathcomp.algebra.countalg]
R:88 [binder, in mathcomp.fingroup.morphism]
r:882 [binder, in mathcomp.algebra.polydiv]
r:888 [binder, in mathcomp.ssreflect.ssrnat]
r:89 [binder, in mathcomp.algebra.polydiv]
R:896 [binder, in mathcomp.algebra.matrix]
r:90 [binder, in mathcomp.character.inertia]
r:901 [binder, in mathcomp.ssreflect.ssrnat]
r:91 [binder, in mathcomp.solvable.nilpotent]
r:912 [binder, in mathcomp.ssreflect.ssrnat]
r:914 [binder, in mathcomp.algebra.ssralg]
R:92 [binder, in mathcomp.algebra.countalg]
R:92 [binder, in mathcomp.algebra.ssrnum]
r:926 [binder, in mathcomp.ssreflect.ssrnat]
R:927 [binder, in mathcomp.ssreflect.seq]
R:927 [binder, in mathcomp.ssreflect.finset]
r:929 [binder, in mathcomp.algebra.polydiv]
R:93 [binder, in mathcomp.fingroup.morphism]
r:931 [binder, in mathcomp.algebra.ssralg]
r:932 [binder, in mathcomp.algebra.polydiv]
r:933 [binder, in mathcomp.algebra.poly]
r:936 [binder, in mathcomp.algebra.ssrnum]
r:944 [binder, in mathcomp.algebra.ssrnum]
r:949 [binder, in mathcomp.algebra.polydiv]
R:951 [binder, in mathcomp.ssreflect.bigop]
r:952 [binder, in mathcomp.algebra.polydiv]
r:952 [binder, in mathcomp.algebra.ssrnum]
R:953 [binder, in mathcomp.algebra.matrix]
r:955 [binder, in mathcomp.algebra.polydiv]
R:96 [binder, in mathcomp.algebra.ssrnum]
R:960 [binder, in mathcomp.algebra.ssralg]
r:965 [binder, in mathcomp.algebra.ssrnum]
R:966 [binder, in mathcomp.algebra.ssralg]
R:967 [binder, in mathcomp.algebra.ssralg]
R:97 [binder, in mathcomp.fingroup.morphism]
r:971 [binder, in mathcomp.ssreflect.bigop]
r:976 [binder, in mathcomp.algebra.vector]
r:978 [binder, in mathcomp.algebra.poly]
R:98 [binder, in mathcomp.algebra.countalg]
r:987 [binder, in mathcomp.algebra.polydiv]
| 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 | (78134 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 | (1810 entries) |
| Binder 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 | (47626 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 | (375 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 | (4027 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 | (91 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 | (14457 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 | (469 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 | (45 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 | (133 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 | (451 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 | (1391 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 | (851 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 | (6161 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 | (247 entries) |