| 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 | -(23836 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 | -(1409 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 | -(221 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 | -(3574 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 | -(90 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 | -(12096 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 | -(368 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 | -(107 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 | -(273 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 | -(1140 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 | -(728 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 | -(3596 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 | -(189 entries) | -
R
-R [abbreviation, in mathcomp.field.finfield]-R [abbreviation, in mathcomp.field.finfield]
-r [abbreviation, in mathcomp.character.mxabelem]
-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]
-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_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]
-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]
-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_lersif_normr [lemma, in mathcomp.algebra.interval]
-real_lersif_norml [lemma, in mathcomp.algebra.interval]
-real_lersifN [lemma, in mathcomp.algebra.interval]
-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_perm [abbreviation, in mathcomp.fingroup.perm]
-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]
-relpre [definition, in mathcomp.ssreflect.ssrbool]
-relU_sym [lemma, in mathcomp.ssreflect.fingraph]
-rel_base [definition, in mathcomp.ssreflect.path]
-rel_adjunction [abbreviation, in mathcomp.ssreflect.fingraph]
-rel_adjunction [abbreviation, in mathcomp.ssreflect.fingraph]
-rel_functor [projection, in mathcomp.ssreflect.fingraph]
-rel_unit [projection, in mathcomp.ssreflect.fingraph]
-rel_adjunction_mem [record, in mathcomp.ssreflect.fingraph]
-rem [definition, in mathcomp.ssreflect.seq]
-Rem [section, in mathcomp.ssreflect.seq]
-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 [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]
-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]
-rgd [definition, in mathcomp.solvable.alt]
-rgdP [lemma, in mathcomp.solvable.alt]
-rgd_fun [definition, in mathcomp.solvable.alt]
-rGf [abbreviation, in mathcomp.character.mxrepresentation]
-rGf [abbreviation, in mathcomp.character.mxrepresentation]
-rGf [abbreviation, in mathcomp.character.mxrepresentation]
-rGf [abbreviation, in mathcomp.character.mxrepresentation]
-rGH [abbreviation, in mathcomp.character.mxrepresentation]
-rGH [abbreviation, in mathcomp.character.mxrepresentation]
-rgraph [definition, in mathcomp.ssreflect.fingraph]
-rgraphK [lemma, in mathcomp.ssreflect.fingraph]
-rH [abbreviation, in mathcomp.character.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]
-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]
-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_geq_poly_eq0 [lemma, in mathcomp.algebra.poly]
-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]
-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_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]
-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]
-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]
-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 | -(23836 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 | -(1409 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 | -(221 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 | -(3574 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 | -(90 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 | -(12096 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 | -(368 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 | -(107 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 | -(273 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 | -(1140 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 | -(728 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 | -(3596 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 | -(189 entries) | -