| 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 | +(23233 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 | +(1373 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 | +(213 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 | +(3475 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 | +(89 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 | +(11853 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 | +(359 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 | +(47 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 | +(103 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 | +(266 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 | +(1118 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 | +(691 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 | +(3461 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 | +(185 entries) | +
R
+R [abbreviation, in mathcomp.field.finfield]+R [abbreviation, in mathcomp.field.finfield]
+r [abbreviation, in mathcomp.character.mxabelem]
+rabstrX [lemma, in mathcomp.field.closed_field]
+ract [definition, in mathcomp.fingroup.action]
+ractE [lemma, in mathcomp.fingroup.action]
+ractpermE [lemma, 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]
+ramulXnT [lemma, in mathcomp.field.closed_field]
+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_Wedderburn_subring [lemma, in mathcomp.character.mxrepresentation]
+rank_irr_comp [lemma, in mathcomp.character.mxrepresentation]
+rank_irr1 [lemma, in mathcomp.character.mxrepresentation]
+rank_DnQ [lemma, in mathcomp.solvable.extraspecial]
+rank_Dn [lemma, in mathcomp.solvable.extraspecial]
+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_mx_group [lemma, in mathcomp.character.mxabelem]
+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_ChoiceMixin [definition, in mathcomp.algebra.fraction]
+ratio_EqMixin [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_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_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_spec [constructor, in mathcomp.algebra.rat]
+rat_spec [inductive, in mathcomp.algebra.rat]
+rat_field_axiom [lemma, in mathcomp.algebra.rat]
+rat_comRingMixin [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_countMixin [definition, in mathcomp.algebra.rat]
+rat_choiceMixin [definition, in mathcomp.algebra.rat]
+rat_eqMixin [definition, 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]
+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_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_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_mx_repr [lemma, in mathcomp.character.mxrepresentation]
+rconj_mx [definition, in mathcomp.character.mxrepresentation]
+rcons [definition, in mathcomp.ssreflect.seq]
+rcons_path [lemma, in mathcomp.ssreflect.path]
+rcons_tupleP [lemma, in mathcomp.ssreflect.tuple]
+rcons_uniq [lemma, in mathcomp.ssreflect.seq]
+rcons_cat [lemma, in mathcomp.ssreflect.seq]
+rcons_cons [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_is_action [lemma, in mathcomp.fingroup.action]
+rcoset_kerP [lemma, in mathcomp.fingroup.morphism]
+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]
+rcoset1 [lemma, in mathcomp.fingroup.fingroup]
+rdegree [projection, in mathcomp.character.character]
+rdivpT [definition, in mathcomp.field.closed_field]
+rdvdpT [definition, in mathcomp.field.closed_field]
+RealLeAxiom [abbreviation, in mathcomp.algebra.ssrnum]
+RealLeMixin [abbreviation, in mathcomp.algebra.ssrnum]
+RealLtMixin [abbreviation, in mathcomp.algebra.ssrnum]
+realz [lemma, in mathcomp.algebra.ssrint]
+real_lersifN [lemma, in mathcomp.algebra.interval]
+redivpT [definition, in mathcomp.field.closed_field]
+redivpTP [lemma, in mathcomp.field.closed_field]
+redivpT_qf [lemma, in mathcomp.field.closed_field]
+redivp_rec_loopP [lemma, in mathcomp.field.closed_field]
+redivp_rec_loopT_qf [lemma, in mathcomp.field.closed_field]
+redivp_rec_loopTP [lemma, in mathcomp.field.closed_field]
+redivp_rec_loop [definition, in mathcomp.field.closed_field]
+redivp_rec_loopT [definition, in mathcomp.field.closed_field]
+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_key [lemma, in mathcomp.field.fieldext]
+ReflectProp [section, in mathcomp.fingroup.morphism]
+ReflectProp.aT [variable, in mathcomp.fingroup.morphism]
+ReflectProp.Defs [section, in mathcomp.fingroup.morphism]
+ReflectProp.Defs.A [variable, in mathcomp.fingroup.morphism]
+ReflectProp.Defs.B [variable, in mathcomp.fingroup.morphism]
+ReflectProp.Defs.MorphicProps [section, in mathcomp.fingroup.morphism]
+ReflectProp.Defs.MorphicProps.f [variable, in mathcomp.fingroup.morphism]
+ReflectProp.f [variable, in mathcomp.fingroup.morphism]
+ReflectProp.G [variable, in mathcomp.fingroup.morphism]
+ReflectProp.Main [section, in mathcomp.fingroup.morphism]
+ReflectProp.Main.f [variable, in mathcomp.fingroup.morphism]
+ReflectProp.Main.G [variable, in mathcomp.fingroup.morphism]
+ReflectProp.Main.H [variable, in mathcomp.fingroup.morphism]
+ReflectProp.Main.isoGH [variable, in mathcomp.fingroup.morphism]
+ReflectProp.rT [variable, in mathcomp.fingroup.morphism]
+_ \isog _ [notation, in mathcomp.fingroup.morphism]
+RegularVectType [section, in mathcomp.algebra.vector]
+RegularVectType.R [variable, in mathcomp.algebra.vector]
+regular_splittingAxiom [lemma, in mathcomp.field.galois]
+regular_norm_coprime [lemma, in mathcomp.solvable.frobenius]
+regular_norm_dvd_pred [lemma, in mathcomp.solvable.frobenius]
+regular_op_inj [lemma, in mathcomp.character.mxrepresentation]
+regular_module_ideal [lemma, in mathcomp.character.mxrepresentation]
+regular_mx_faithful [lemma, in mathcomp.character.mxrepresentation]
+regular_mx_repr [lemma, in mathcomp.character.mxrepresentation]
+regular_mx [definition, in mathcomp.character.mxrepresentation]
+regular_vectMixin [definition, in mathcomp.algebra.vector]
+regular_vect_iso [lemma, in mathcomp.algebra.vector]
+regular_fullv [lemma, in mathcomp.field.falgebra]
+reindex [lemma, in mathcomp.ssreflect.bigop]
+reindex_bigcprod [lemma, in mathcomp.fingroup.gproduct]
+reindex_irr_class [lemma, in mathcomp.character.character]
+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_inj [lemma, in mathcomp.ssreflect.bigop]
+reindex_onto [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_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]
+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.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]
+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_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_ofK [lemma, in mathcomp.ssreflect.generic_quotient]
+repr_of [definition, in mathcomp.ssreflect.generic_quotient]
+repr_irr_classK [lemma, in mathcomp.character.character]
+repr_rsim_diag [lemma, in mathcomp.character.character]
+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_mem_transversal [lemma, in mathcomp.ssreflect.finset]
+repr_mem_pblock [lemma, in mathcomp.ssreflect.finset]
+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.character.character]
+Restrict [section, in mathcomp.fingroup.action]
+Restrict [section, in mathcomp.character.classfun]
+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]
+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.character]
+Restrict.gT [variable, in mathcomp.character.classfun]
+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]
+restr_perm_isom [lemma, in mathcomp.fingroup.action]
+restr_perm_Aut [lemma, in mathcomp.fingroup.action]
+restr_permE [lemma, in mathcomp.fingroup.action]
+restr_perm_on [lemma, 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 [section, in mathcomp.ssreflect.seq]
+rev [definition, in mathcomp.ssreflect.seq]
+revK [lemma, in mathcomp.ssreflect.seq]
+rev_sorted [lemma, in mathcomp.ssreflect.path]
+rev_path [lemma, in mathcomp.ssreflect.path]
+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_rot [lemma, in mathcomp.ssreflect.seq]
+rev_rotr [lemma, in mathcomp.ssreflect.seq]
+rev_uniq [lemma, in mathcomp.ssreflect.seq]
+rev_rcons [lemma, in mathcomp.ssreflect.seq]
+rev_cat [lemma, in mathcomp.ssreflect.seq]
+rev_cons [lemma, in mathcomp.ssreflect.seq]
+rev_ord_inj [lemma, in mathcomp.ssreflect.fintype]
+rev_ordK [lemma, in mathcomp.ssreflect.fintype]
+rev_ord [definition, in mathcomp.ssreflect.fintype]
+rev_ord_proof [lemma, in mathcomp.ssreflect.fintype]
+Rev.T [variable, in mathcomp.ssreflect.seq]
+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_morph [lemma, in mathcomp.solvable.alt]
+rfd_fun [definition, in mathcomp.solvable.alt]
+rfd_funP [lemma, in mathcomp.solvable.alt]
+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]
+rfix_pgroup_char [lemma, in mathcomp.character.mxabelem]
+rfix_abelem [lemma, in mathcomp.character.mxabelem]
+rG [abbreviation, in mathcomp.character.mxrepresentation]
+rG [abbreviation, in mathcomp.character.mxrepresentation]
+rG [abbreviation, in mathcomp.character.mxabelem]
+rGB [abbreviation, in mathcomp.character.mxrepresentation]
+rGB [abbreviation, in mathcomp.character.mxrepresentation]
+rgcdpT [definition, in mathcomp.field.closed_field]
+rgcdpTP [lemma, in mathcomp.field.closed_field]
+rgcdpTs [definition, in mathcomp.field.closed_field]
+rgcdpTsP [lemma, in mathcomp.field.closed_field]
+rgcdpTs_qf [lemma, in mathcomp.field.closed_field]
+rgcdpT_qf [lemma, in mathcomp.field.closed_field]
+rgcdp_loopT_qf [lemma, in mathcomp.field.closed_field]
+rgcdp_loopP [lemma, in mathcomp.field.closed_field]
+rgcdp_loopT [definition, in mathcomp.field.closed_field]
+rgcdp_loop [definition, in mathcomp.field.closed_field]
+rgd [definition, in mathcomp.solvable.alt]
+rgdcopT [definition, in mathcomp.field.closed_field]
+rgdcopTP [lemma, in mathcomp.field.closed_field]
+rgdcopT_qf [lemma, in mathcomp.field.closed_field]
+rgdcop_recT_qf [lemma, in mathcomp.field.closed_field]
+rgdcop_recTP [lemma, in mathcomp.field.closed_field]
+rgdcop_recT [definition, in mathcomp.field.closed_field]
+rgdP [lemma, in mathcomp.solvable.alt]
+rgd_fun [definition, in mathcomp.solvable.alt]
+rGf [abbreviation, in mathcomp.character.mxrepresentation]
+rGf [abbreviation, in mathcomp.character.mxrepresentation]
+rGf [abbreviation, in mathcomp.character.mxrepresentation]
+rGf [abbreviation, in mathcomp.character.mxrepresentation]
+rGH [abbreviation, in mathcomp.character.mxrepresentation]
+rGH [abbreviation, in mathcomp.character.mxrepresentation]
+rgraph [definition, in mathcomp.ssreflect.fingraph]
+rgraphK [lemma, in mathcomp.ssreflect.fingraph]
+rH [abbreviation, in mathcomp.character.mxrepresentation]
+rH [abbreviation, in mathcomp.character.mxrepresentation]
+rH [abbreviation, in mathcomp.character.mxrepresentation]
+rH [abbreviation, in mathcomp.character.mxrepresentation]
+rH [abbreviation, in mathcomp.character.mxabelem]
+rHG [abbreviation, in mathcomp.character.mxabelem]
+right_arc [lemma, in mathcomp.ssreflect.path]
+right_trans [lemma, in mathcomp.ssreflect.generic_quotient]
+right_mx_ideal [definition, in mathcomp.algebra.mxalgebra]
+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]
+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]
+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_quotient [library]
+RintMod [section, in mathcomp.algebra.ssrint]
+RintMod.R [variable, in mathcomp.algebra.ssrint]
+rker [definition, in mathcomp.character.mxrepresentation]
+rkerP [lemma, in mathcomp.character.mxrepresentation]
+rker_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_abelem [lemma, in mathcomp.character.mxabelem]
+rmodpT [definition, in mathcomp.field.closed_field]
+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_unity_root [lemma, in mathcomp.algebra.poly]
+rmorph_root [lemma, in mathcomp.algebra.poly]
+rmorph_int [lemma, in mathcomp.algebra.ssrint]
+rmulpT [lemma, in mathcomp.field.closed_field]
+root [definition, in mathcomp.algebra.poly]
+root [definition, in mathcomp.ssreflect.fingraph]
+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.algebra.poly]
+rootP [lemma, in mathcomp.ssreflect.fingraph]
+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]
+rootX [lemma, in mathcomp.algebra.poly]
+rootZ [lemma, in mathcomp.algebra.poly]
+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_annihilant [lemma, in mathcomp.algebra.polyXY]
+root_cyclotomic [lemma, in mathcomp.field.cyclotomic]
+root_monic_Aint [lemma, in mathcomp.field.algnum]
+root_exp_XsubC [lemma, in mathcomp.algebra.poly]
+root_prod_XsubC [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]
+root_connect [lemma, in mathcomp.ssreflect.fingraph]
+root_root [lemma, in mathcomp.ssreflect.fingraph]
+root0 [lemma, in mathcomp.algebra.poly]
+root1 [lemma, in mathcomp.algebra.poly]
+rot [definition, in mathcomp.ssreflect.seq]
+rot [definition, in mathcomp.solvable.burnside_app]
+rotations [definition, in mathcomp.solvable.burnside_app]
+rotations_is_rot [lemma, in mathcomp.solvable.burnside_app]
+RotCompLemmas [section, in mathcomp.ssreflect.seq]
+RotCompLemmas.T [variable, in mathcomp.ssreflect.seq]
+rotK [lemma, in mathcomp.ssreflect.seq]
+rotr [definition, 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_ucycle [lemma, in mathcomp.ssreflect.path]
+rotr_cycle [lemma, in mathcomp.ssreflect.path]
+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]
+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_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_tupleP [lemma, in mathcomp.ssreflect.tuple]
+rot_rotr [lemma, in mathcomp.ssreflect.seq]
+rot_rot [lemma, in mathcomp.ssreflect.seq]
+rot_add_mod [lemma, in mathcomp.ssreflect.seq]
+rot_addn [lemma, in mathcomp.ssreflect.seq]
+rot_to [lemma, in mathcomp.ssreflect.seq]
+rot_to_spec [inductive, 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_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_inv [definition, in mathcomp.solvable.burnside_app]
+rot0 [lemma, in mathcomp.ssreflect.seq]
+rot1_cons [lemma, in mathcomp.ssreflect.seq]
+row [definition, in mathcomp.algebra.matrix]
+rowE [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_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.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]
+rowV0P [lemma, in mathcomp.algebra.mxalgebra]
+rowV0Pn [lemma, in mathcomp.algebra.mxalgebra]
+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_permE [lemma, in mathcomp.algebra.matrix]
+row_mul [lemma, in mathcomp.algebra.matrix]
+row_sum_delta [lemma, in mathcomp.algebra.matrix]
+row_mx_eq0 [lemma, in mathcomp.algebra.matrix]
+row_mx0 [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_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_eq [lemma, in mathcomp.algebra.matrix]
+row_id [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_map [lemma, in mathcomp.algebra.mxalgebra]
+row_free_map [lemma, in mathcomp.algebra.mxalgebra]
+row_base_free [lemma, in mathcomp.algebra.mxalgebra]
+row_full_unit [lemma, in mathcomp.algebra.mxalgebra]
+row_free_unit [lemma, 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'Kd [lemma, in mathcomp.algebra.matrix]
+row'Ku [lemma, in mathcomp.algebra.matrix]
+row'_row_mx [lemma, in mathcomp.algebra.matrix]
+row'_eq [lemma, in mathcomp.algebra.matrix]
+row'_const [lemma, in mathcomp.algebra.matrix]
+row0 [lemma, in mathcomp.algebra.matrix]
+row1 [lemma, in mathcomp.algebra.matrix]
+rpoly [definition, in mathcomp.field.closed_field]
+rpoly_map_mul [lemma, in mathcomp.field.closed_field]
+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_rat [lemma, in mathcomp.algebra.rat]
+rpred_Crat [lemma, in mathcomp.field.algC]
+rpred_Cnat [lemma, in mathcomp.field.algC]
+rpred_Cint [lemma, in mathcomp.field.algC]
+rpred_horner [lemma, in mathcomp.algebra.poly]
+rpred_int [lemma, in mathcomp.algebra.ssrint]
+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]
+rscalpT [definition, in mathcomp.field.closed_field]
+rseq_poly_map [lemma, in mathcomp.field.closed_field]
+rseq_poly [definition, in mathcomp.field.closed_field]
+rshift [definition, 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_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]
+rsim_abelem_subg [lemma, in mathcomp.character.mxabelem]
+rstab [definition, in mathcomp.character.mxrepresentation]
+rstabS [lemma, in mathcomp.character.mxrepresentation]
+rstabs [definition, in mathcomp.character.mxrepresentation]
+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_set [lemma, in mathcomp.character.mxrepresentation]
+rstabs_sub [lemma, in mathcomp.character.mxrepresentation]
+rstabs_abelemG [lemma, in mathcomp.character.mxabelem]
+rstabs_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_set [lemma, in mathcomp.character.mxrepresentation]
+rstab_sub [lemma, in mathcomp.character.mxrepresentation]
+rstab_abelem [lemma, in mathcomp.character.mxabelem]
+rsubmx [definition, in mathcomp.algebra.matrix]
+rsubmx_key [lemma, in mathcomp.algebra.matrix]
+rsumpT [lemma, in mathcomp.field.closed_field]
+rT [abbreviation, in mathcomp.fingroup.fingroup]
+rU [abbreviation, in mathcomp.character.mxrepresentation]
+rU' [abbreviation, in mathcomp.character.mxrepresentation]
+rVabelem [definition, in mathcomp.character.mxabelem]
+rVabelemD [lemma, in mathcomp.character.mxabelem]
+rVabelemJ [lemma, in mathcomp.character.mxabelem]
+rVabelemK [lemma, in mathcomp.character.mxabelem]
+rVabelemN [lemma, in mathcomp.character.mxabelem]
+rVabelemS [lemma, in mathcomp.character.mxabelem]
+rVabelemZ [lemma, in mathcomp.character.mxabelem]
+rVabelem_minj [lemma, in mathcomp.character.mxabelem]
+rVabelem_mK [lemma, in mathcomp.character.mxabelem]
+rVabelem_injm [lemma, in mathcomp.character.mxabelem]
+rVabelem_inj [lemma, in mathcomp.character.mxabelem]
+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_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]
+R_G [abbreviation, in mathcomp.character.integral_char]
+R_G [abbreviation, in mathcomp.character.mxrepresentation]
+R_G [abbreviation, in mathcomp.character.mxrepresentation]
+r012 [definition, in mathcomp.solvable.burnside_app]
+R012 [definition, in mathcomp.solvable.burnside_app]
+R012f [definition, in mathcomp.solvable.burnside_app]
+R012_inj [lemma, in mathcomp.solvable.burnside_app]
+r013 [definition, in mathcomp.solvable.burnside_app]
+R013 [definition, in mathcomp.solvable.burnside_app]
+R013f [definition, in mathcomp.solvable.burnside_app]
+R013_inj [lemma, in mathcomp.solvable.burnside_app]
+r021 [definition, in mathcomp.solvable.burnside_app]
+R021 [definition, in mathcomp.solvable.burnside_app]
+R021f [definition, in mathcomp.solvable.burnside_app]
+R021_inj [lemma, in mathcomp.solvable.burnside_app]
+r024 [definition, in mathcomp.solvable.burnside_app]
+R024 [definition, in mathcomp.solvable.burnside_app]
+R024f [definition, in mathcomp.solvable.burnside_app]
+R024_inj [lemma, in mathcomp.solvable.burnside_app]
+r031 [definition, in mathcomp.solvable.burnside_app]
+R031 [definition, in mathcomp.solvable.burnside_app]
+R031f [definition, in mathcomp.solvable.burnside_app]
+R031_inj [lemma, in mathcomp.solvable.burnside_app]
+r034 [definition, in mathcomp.solvable.burnside_app]
+R034 [definition, in mathcomp.solvable.burnside_app]
+R034f [definition, in mathcomp.solvable.burnside_app]
+R034_inj [lemma, in mathcomp.solvable.burnside_app]
+r042 [definition, in mathcomp.solvable.burnside_app]
+R042 [definition, in mathcomp.solvable.burnside_app]
+R042f [definition, in mathcomp.solvable.burnside_app]
+R042_inj [lemma, in mathcomp.solvable.burnside_app]
+r043 [definition, in mathcomp.solvable.burnside_app]
+R043 [definition, in mathcomp.solvable.burnside_app]
+R043f [definition, in mathcomp.solvable.burnside_app]
+R043_inj [lemma, in mathcomp.solvable.burnside_app]
+r05 [definition, in mathcomp.solvable.burnside_app]
+R05 [definition, in mathcomp.solvable.burnside_app]
+R05f [definition, in mathcomp.solvable.burnside_app]
+r05_inv [lemma, in mathcomp.solvable.burnside_app]
+R05_inj [lemma, in mathcomp.solvable.burnside_app]
+r1 [definition, in mathcomp.solvable.burnside_app]
+R1 [definition, in mathcomp.solvable.burnside_app]
+r1_inv [lemma, in mathcomp.solvable.burnside_app]
+R1_inj [lemma, in mathcomp.solvable.burnside_app]
+r14 [definition, in mathcomp.solvable.burnside_app]
+R14 [definition, in mathcomp.solvable.burnside_app]
+R14f [definition, in mathcomp.solvable.burnside_app]
+r14_inv [lemma, in mathcomp.solvable.burnside_app]
+R14_inj [lemma, in mathcomp.solvable.burnside_app]
+r2 [definition, in mathcomp.solvable.burnside_app]
+R2 [definition, in mathcomp.solvable.burnside_app]
+r2_inv [lemma, in mathcomp.solvable.burnside_app]
+R2_inj [lemma, in mathcomp.solvable.burnside_app]
+r23 [definition, in mathcomp.solvable.burnside_app]
+R23 [definition, in mathcomp.solvable.burnside_app]
+R23f [definition, in mathcomp.solvable.burnside_app]
+R23_inj [lemma, in mathcomp.solvable.burnside_app]
+r3 [definition, in mathcomp.solvable.burnside_app]
+R3 [definition, in mathcomp.solvable.burnside_app]
+r3_inv [lemma, in mathcomp.solvable.burnside_app]
+R3_inj [lemma, in mathcomp.solvable.burnside_app]
+r32 [definition, in mathcomp.solvable.burnside_app]
+R32 [definition, in mathcomp.solvable.burnside_app]
+R32f [definition, in mathcomp.solvable.burnside_app]
+R32_inj [lemma, in mathcomp.solvable.burnside_app]
+r41 [definition, in mathcomp.solvable.burnside_app]
+R41 [definition, in mathcomp.solvable.burnside_app]
+R41f [definition, in mathcomp.solvable.burnside_app]
+r41_inv [lemma, in mathcomp.solvable.burnside_app]
+R41_inj [lemma, in mathcomp.solvable.burnside_app]
+r50 [definition, in mathcomp.solvable.burnside_app]
+R50 [definition, in mathcomp.solvable.burnside_app]
+R50f [definition, in mathcomp.solvable.burnside_app]
+r50_inv [lemma, in mathcomp.solvable.burnside_app]
+R50_inj [lemma, in mathcomp.solvable.burnside_app]
+
| Global Index | +A | +B | +C | +D | +E | +F | +G | +H | +I | +J | +K | +L | +M | +N | +O | +P | +Q | +R | +S | +T | +U | +V | +W | +X | +Y | +Z | +_ | +other | +(23233 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 | +(1373 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 | +(213 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 | +(3475 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 | +(89 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 | +(11853 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 | +(359 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 | +(47 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 | +(103 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 | +(266 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 | +(1118 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 | +(691 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 | +(3461 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 | +(185 entries) | +