| 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) | +
E
+eC [abbreviation, in mathcomp.ssreflect.generic_quotient]+ecubes [definition, in mathcomp.solvable.burnside_app]
+ecubes_def [lemma, in mathcomp.solvable.burnside_app]
+ED [abbreviation, in mathcomp.solvable.extremal]
+edivn [definition, in mathcomp.ssreflect.div]
+edivnP [lemma, in mathcomp.ssreflect.div]
+EdivnSpec [constructor, in mathcomp.ssreflect.div]
+edivn_def [lemma, in mathcomp.ssreflect.div]
+edivn_eq [lemma, in mathcomp.ssreflect.div]
+edivn_spec [inductive, in mathcomp.ssreflect.div]
+edivn_rec [definition, in mathcomp.ssreflect.div]
+edivn2 [definition, in mathcomp.ssreflect.prime]
+edivn2P [lemma, in mathcomp.ssreflect.prime]
+egcdn [definition, in mathcomp.ssreflect.div]
+egcdnP [lemma, in mathcomp.ssreflect.div]
+EgcdnSpec [constructor, in mathcomp.ssreflect.div]
+egcdn_spec [inductive, in mathcomp.ssreflect.div]
+egcdn_rec [definition, in mathcomp.ssreflect.div]
+egcdz [definition, in mathcomp.algebra.intdiv]
+egcdzP [lemma, in mathcomp.algebra.intdiv]
+EgcdzSpec [constructor, in mathcomp.algebra.intdiv]
+egcdz_spec [inductive, in mathcomp.algebra.intdiv]
+egcd0n [lemma, in mathcomp.ssreflect.div]
+eigenspace [definition, in mathcomp.algebra.mxalgebra]
+eigenspaceP [lemma, in mathcomp.algebra.mxalgebra]
+eigenvalue [definition, in mathcomp.algebra.mxalgebra]
+eigenvalueP [lemma, in mathcomp.algebra.mxalgebra]
+eigenvalue_root_min [lemma, in mathcomp.algebra.mxpoly]
+eigenvalue_root_char [lemma, in mathcomp.algebra.mxpoly]
+eigenvalue_map [lemma, in mathcomp.algebra.mxalgebra]
+ElementOps [section, in mathcomp.fingroup.fingroup]
+ElementOps.T [variable, in mathcomp.fingroup.fingroup]
+Elim1 [section, in mathcomp.ssreflect.bigop]
+Elim1.f [variable, in mathcomp.ssreflect.bigop]
+Elim1.fM [variable, in mathcomp.ssreflect.bigop]
+Elim1.f_id [variable, in mathcomp.ssreflect.bigop]
+Elim1.idx [variable, in mathcomp.ssreflect.bigop]
+Elim1.K [variable, in mathcomp.ssreflect.bigop]
+Elim1.Kid [variable, in mathcomp.ssreflect.bigop]
+Elim1.Kop [variable, in mathcomp.ssreflect.bigop]
+Elim1.Kop' [variable, in mathcomp.ssreflect.bigop]
+Elim1.op [variable, in mathcomp.ssreflect.bigop]
+Elim1.op' [variable, in mathcomp.ssreflect.bigop]
+Elim1.R [variable, in mathcomp.ssreflect.bigop]
+Elim2 [section, in mathcomp.ssreflect.bigop]
+Elim2.f [variable, in mathcomp.ssreflect.bigop]
+Elim2.f_id [variable, in mathcomp.ssreflect.bigop]
+Elim2.f_op [variable, in mathcomp.ssreflect.bigop]
+Elim2.id1 [variable, in mathcomp.ssreflect.bigop]
+Elim2.id2 [variable, in mathcomp.ssreflect.bigop]
+Elim2.K [variable, in mathcomp.ssreflect.bigop]
+Elim2.Kid [variable, in mathcomp.ssreflect.bigop]
+Elim2.Kop [variable, in mathcomp.ssreflect.bigop]
+Elim2.op1 [variable, in mathcomp.ssreflect.bigop]
+Elim2.op2 [variable, in mathcomp.ssreflect.bigop]
+Elim2.R1 [variable, in mathcomp.ssreflect.bigop]
+Elim2.R2 [variable, in mathcomp.ssreflect.bigop]
+Elim3 [section, in mathcomp.ssreflect.bigop]
+Elim3.id1 [variable, in mathcomp.ssreflect.bigop]
+Elim3.id2 [variable, in mathcomp.ssreflect.bigop]
+Elim3.id3 [variable, in mathcomp.ssreflect.bigop]
+Elim3.K [variable, in mathcomp.ssreflect.bigop]
+Elim3.Kid [variable, in mathcomp.ssreflect.bigop]
+Elim3.Kop [variable, in mathcomp.ssreflect.bigop]
+Elim3.op1 [variable, in mathcomp.ssreflect.bigop]
+Elim3.op2 [variable, in mathcomp.ssreflect.bigop]
+Elim3.op3 [variable, in mathcomp.ssreflect.bigop]
+Elim3.R1 [variable, in mathcomp.ssreflect.bigop]
+Elim3.R2 [variable, in mathcomp.ssreflect.bigop]
+Elim3.R3 [variable, in mathcomp.ssreflect.bigop]
+elogn2 [definition, in mathcomp.ssreflect.prime]
+elogn2P [lemma, in mathcomp.ssreflect.prime]
+Elogn2Spec [constructor, in mathcomp.ssreflect.prime]
+elogn2_spec [inductive, in mathcomp.ssreflect.prime]
+eltm [definition, in mathcomp.solvable.cyclic]
+Eltm [section, in mathcomp.solvable.cyclic]
+eltmE [lemma, in mathcomp.solvable.cyclic]
+eltmM [lemma, in mathcomp.solvable.cyclic]
+eltm_id [lemma, in mathcomp.solvable.cyclic]
+Eltm.aT [variable, in mathcomp.solvable.cyclic]
+Eltm.dvd_y_x [variable, in mathcomp.solvable.cyclic]
+Eltm.rT [variable, in mathcomp.solvable.cyclic]
+Eltm.x [variable, in mathcomp.solvable.cyclic]
+Eltm.y [variable, in mathcomp.solvable.cyclic]
+encModEquivP [definition, in mathcomp.ssreflect.generic_quotient]
+EncModRel [abbreviation, in mathcomp.ssreflect.generic_quotient]
+encModRel [record, in mathcomp.ssreflect.generic_quotient]
+EncModRelClass [abbreviation, in mathcomp.ssreflect.generic_quotient]
+encModRelClass [definition, in mathcomp.ssreflect.generic_quotient]
+EncModRelClassPack [constructor, in mathcomp.ssreflect.generic_quotient]
+encModRelE [definition, in mathcomp.ssreflect.generic_quotient]
+encModRelP [definition, in mathcomp.ssreflect.generic_quotient]
+EncModRelPack [constructor, in mathcomp.ssreflect.generic_quotient]
+encModRel_class_of [inductive, in mathcomp.ssreflect.generic_quotient]
+encoded_equivP [lemma, in mathcomp.ssreflect.generic_quotient]
+encoded_equiv_is_equiv [lemma, in mathcomp.ssreflect.generic_quotient]
+encoded_equivE [lemma, in mathcomp.ssreflect.generic_quotient]
+encoded_equiv [definition, in mathcomp.ssreflect.generic_quotient]
+EncodingModuloEquiv [section, in mathcomp.ssreflect.generic_quotient]
+EncodingModuloEquiv.D [variable, in mathcomp.ssreflect.generic_quotient]
+EncodingModuloEquiv.DE [variable, in mathcomp.ssreflect.generic_quotient]
+EncodingModuloEquiv.e [variable, in mathcomp.ssreflect.generic_quotient]
+EncodingModuloEquiv.E [variable, in mathcomp.ssreflect.generic_quotient]
+EncodingModuloEquiv.ED [variable, in mathcomp.ssreflect.generic_quotient]
+EncodingModuloEquiv.r [variable, in mathcomp.ssreflect.generic_quotient]
+EncodingModuloRel [section, in mathcomp.ssreflect.generic_quotient]
+EncodingModuloRel.D [variable, in mathcomp.ssreflect.generic_quotient]
+EncodingModuloRel.DE [variable, in mathcomp.ssreflect.generic_quotient]
+EncodingModuloRel.e [variable, in mathcomp.ssreflect.generic_quotient]
+EncodingModuloRel.E [variable, in mathcomp.ssreflect.generic_quotient]
+EncodingModuloRel.ED [variable, in mathcomp.ssreflect.generic_quotient]
+EncodingModuloRel.r [variable, in mathcomp.ssreflect.generic_quotient]
+enc_mod_rel_equiv_rel [definition, in mathcomp.ssreflect.generic_quotient]
+enc_mod_rel_is_equiv [lemma, in mathcomp.ssreflect.generic_quotient]
+enc_mod_rel [projection, in mathcomp.ssreflect.generic_quotient]
+enum [abbreviation, in mathcomp.ssreflect.fintype]
+enumF [abbreviation, in mathcomp.ssreflect.fintype]
+enumP [lemma, in mathcomp.ssreflect.fintype]
+EnumRank [section, in mathcomp.ssreflect.fintype]
+EnumRank.T [variable, in mathcomp.ssreflect.fintype]
+EnumSocle [constructor, in mathcomp.character.mxrepresentation]
+enumT [lemma, in mathcomp.ssreflect.fintype]
+enum_AEnd [lemma, in mathcomp.field.galois]
+enum_tupleP [lemma, in mathcomp.ssreflect.tuple]
+enum_extremal_groups [definition, in mathcomp.solvable.extremal]
+enum_ordS [lemma, in mathcomp.ssreflect.fintype]
+enum_val_ord [lemma, in mathcomp.ssreflect.fintype]
+enum_rank_ord [lemma, in mathcomp.ssreflect.fintype]
+enum_val_bij [lemma, in mathcomp.ssreflect.fintype]
+enum_rank_bij [lemma, in mathcomp.ssreflect.fintype]
+enum_val_bij_in [lemma, in mathcomp.ssreflect.fintype]
+enum_val_inj [lemma, in mathcomp.ssreflect.fintype]
+enum_rank_inj [lemma, in mathcomp.ssreflect.fintype]
+enum_valK [lemma, in mathcomp.ssreflect.fintype]
+enum_valK_in [lemma, in mathcomp.ssreflect.fintype]
+enum_rankK [lemma, in mathcomp.ssreflect.fintype]
+enum_rankK_in [lemma, in mathcomp.ssreflect.fintype]
+enum_val_nth [lemma, in mathcomp.ssreflect.fintype]
+enum_valP [lemma, in mathcomp.ssreflect.fintype]
+enum_val [definition, in mathcomp.ssreflect.fintype]
+enum_default [lemma, in mathcomp.ssreflect.fintype]
+enum_rank [definition, in mathcomp.ssreflect.fintype]
+enum_rank_in [definition, in mathcomp.ssreflect.fintype]
+enum_rank_subproof [lemma, in mathcomp.ssreflect.fintype]
+enum_uniq [lemma, in mathcomp.ssreflect.fintype]
+enum_mem [definition, in mathcomp.ssreflect.fintype]
+enum_set1 [lemma, in mathcomp.ssreflect.finset]
+enum_setT [lemma, in mathcomp.ssreflect.finset]
+enum_set0 [lemma, in mathcomp.ssreflect.finset]
+enum0 [lemma, in mathcomp.ssreflect.fintype]
+enum1 [lemma, in mathcomp.ssreflect.fintype]
+enveloping_algebra_mx [definition, in mathcomp.character.mxrepresentation]
+envelop_mx_ring [lemma, in mathcomp.character.mxrepresentation]
+envelop_mxM [lemma, in mathcomp.character.mxrepresentation]
+envelop_mxP [lemma, in mathcomp.character.mxrepresentation]
+envelop_mx1 [lemma, in mathcomp.character.mxrepresentation]
+envelop_mx_id [lemma, in mathcomp.character.mxrepresentation]
+EqAllPairs [section, in mathcomp.ssreflect.seq]
+EqAllPairs.S [variable, in mathcomp.ssreflect.seq]
+EqAllPairs.T [variable, in mathcomp.ssreflect.seq]
+eqAmod [definition, in mathcomp.field.algnum]
+eqAmodD [lemma, in mathcomp.field.algnum]
+eqAmodDl [lemma, in mathcomp.field.algnum]
+eqAmodDr [lemma, in mathcomp.field.algnum]
+eqAmodM [lemma, in mathcomp.field.algnum]
+eqAmodMl [lemma, in mathcomp.field.algnum]
+eqAmodMl0 [lemma, in mathcomp.field.algnum]
+eqAmodMr [lemma, in mathcomp.field.algnum]
+eqAmodMr0 [lemma, in mathcomp.field.algnum]
+eqAmodm0 [lemma, in mathcomp.field.algnum]
+eqAmodN [lemma, in mathcomp.field.algnum]
+eqAmod_nat [lemma, in mathcomp.field.algnum]
+eqAmod_rat [lemma, in mathcomp.field.algnum]
+eqAmod_addl_mul [lemma, in mathcomp.field.algnum]
+eqAmod_transr [lemma, in mathcomp.field.algnum]
+eqAmod_transl [lemma, in mathcomp.field.algnum]
+eqAmod_trans [lemma, in mathcomp.field.algnum]
+eqAmod_sym [lemma, in mathcomp.field.algnum]
+eqAmod_refl [lemma, in mathcomp.field.algnum]
+eqAmod0 [lemma, in mathcomp.field.algnum]
+eqAmod0_nat [lemma, in mathcomp.field.algnum]
+eqAmod0_rat [lemma, in mathcomp.field.algnum]
+eqb [definition, in mathcomp.ssreflect.eqtype]
+eqbE [lemma, in mathcomp.ssreflect.eqtype]
+eqbF_neg [lemma, in mathcomp.ssreflect.eqtype]
+eqbP [lemma, in mathcomp.ssreflect.eqtype]
+eqb_negLR [lemma, in mathcomp.ssreflect.eqtype]
+eqb_id [lemma, in mathcomp.ssreflect.eqtype]
+eqb0 [lemma, in mathcomp.ssreflect.ssrnat]
+eqb1 [lemma, in mathcomp.ssreflect.ssrnat]
+eqcfP [abbreviation, in mathcomp.character.classfun]
+eqCmodD [lemma, in mathcomp.field.algC]
+eqCmodDl [lemma, in mathcomp.field.algC]
+eqCmodDr [lemma, in mathcomp.field.algC]
+eqCmodM [lemma, in mathcomp.field.algC]
+eqCmodMl [lemma, in mathcomp.field.algC]
+eqCmodMl0 [lemma, in mathcomp.field.algC]
+eqCmodMr [lemma, in mathcomp.field.algC]
+eqCmodMr0 [lemma, in mathcomp.field.algC]
+eqCmodm0 [lemma, in mathcomp.field.algC]
+eqCmodN [lemma, in mathcomp.field.algC]
+eqCmod_addl_mul [lemma, in mathcomp.field.algC]
+eqCmod_nat [lemma, in mathcomp.field.algC]
+eqCmod_transr [lemma, in mathcomp.field.algC]
+eqCmod_transl [lemma, in mathcomp.field.algC]
+eqCmod_trans [lemma, in mathcomp.field.algC]
+eqCmod_sym [lemma, in mathcomp.field.algC]
+eqCmod_refl [lemma, in mathcomp.field.algC]
+eqCmod0 [lemma, in mathcomp.field.algC]
+eqCmod0_nat [lemma, in mathcomp.field.algC]
+EqConnect [section, in mathcomp.ssreflect.fingraph]
+EqConnect.T [variable, in mathcomp.ssreflect.fingraph]
+eqC_nat [definition, in mathcomp.field.algC]
+eqE [lemma, in mathcomp.ssreflect.eqtype]
+eqEcard [lemma, in mathcomp.ssreflect.finset]
+eqEdim [lemma, in mathcomp.algebra.vector]
+eqEproper [lemma, in mathcomp.ssreflect.finset]
+eqEsubset [lemma, in mathcomp.ssreflect.finset]
+eqEsubv [lemma, in mathcomp.algebra.vector]
+EqFlatten [section, in mathcomp.ssreflect.seq]
+EqFlatten.S [variable, in mathcomp.ssreflect.seq]
+EqFlatten.T [variable, in mathcomp.ssreflect.seq]
+EqFun [section, in mathcomp.ssreflect.eqtype]
+eqfunP [lemma, in mathcomp.ssreflect.fintype]
+eqfun_inP [lemma, in mathcomp.ssreflect.fintype]
+EqFun.aT [variable, in mathcomp.ssreflect.eqtype]
+EqFun.Endo [section, in mathcomp.ssreflect.eqtype]
+EqFun.Endo.T [variable, in mathcomp.ssreflect.eqtype]
+EqFun.Exo [section, in mathcomp.ssreflect.eqtype]
+EqFun.Exo.aT [variable, in mathcomp.ssreflect.eqtype]
+EqFun.Exo.D [variable, in mathcomp.ssreflect.eqtype]
+EqFun.Exo.f [variable, in mathcomp.ssreflect.eqtype]
+EqFun.Exo.g [variable, in mathcomp.ssreflect.eqtype]
+EqFun.Exo.rT [variable, in mathcomp.ssreflect.eqtype]
+EqFun.f [variable, in mathcomp.ssreflect.eqtype]
+EqFun.h [variable, in mathcomp.ssreflect.eqtype]
+EqFun.k [variable, in mathcomp.ssreflect.eqtype]
+EqFun.rT1 [variable, in mathcomp.ssreflect.eqtype]
+EqFun.rT2 [variable, in mathcomp.ssreflect.eqtype]
+eqg_mx_abs_irr [lemma, in mathcomp.character.mxrepresentation]
+eqg_mx_irr [lemma, in mathcomp.character.mxrepresentation]
+eqg_mx_faithful [lemma, in mathcomp.character.mxrepresentation]
+eqg_repr [definition, in mathcomp.character.mxrepresentation]
+eqg_repr_proof [lemma, in mathcomp.character.mxrepresentation]
+EqImage [section, in mathcomp.ssreflect.fintype]
+EqImage.T [variable, in mathcomp.ssreflect.fintype]
+EqImage.T' [variable, in mathcomp.ssreflect.fintype]
+EqIso [section, in mathcomp.fingroup.quotient]
+EqIso.eqGH [variable, in mathcomp.fingroup.quotient]
+EqIso.G [variable, in mathcomp.fingroup.quotient]
+EqIso.gT [variable, in mathcomp.fingroup.quotient]
+EqIso.H [variable, in mathcomp.fingroup.quotient]
+eqlfunP [lemma, in mathcomp.algebra.vector]
+eqlfun_inP [lemma, in mathcomp.algebra.vector]
+EqMap [section, in mathcomp.ssreflect.seq]
+EqMap.f [variable, in mathcomp.ssreflect.seq]
+EqMap.Hf [variable, in mathcomp.ssreflect.seq]
+EqMap.n0 [variable, in mathcomp.ssreflect.seq]
+EqMap.T1 [variable, in mathcomp.ssreflect.seq]
+EqMap.T2 [variable, in mathcomp.ssreflect.seq]
+EqMap.x1 [variable, in mathcomp.ssreflect.seq]
+EqMap.x2 [variable, in mathcomp.ssreflect.seq]
+EqMask [section, in mathcomp.ssreflect.seq]
+EqMask.n0 [variable, in mathcomp.ssreflect.seq]
+EqMask.T [variable, in mathcomp.ssreflect.seq]
+eqmodE [lemma, in mathcomp.ssreflect.generic_quotient]
+eqmodP [lemma, in mathcomp.ssreflect.generic_quotient]
+eqmx [definition, in mathcomp.algebra.mxalgebra]
+eqmxMfree [lemma, in mathcomp.algebra.mxalgebra]
+eqmxMfull [lemma, in mathcomp.algebra.mxalgebra]
+eqmxMr [lemma, in mathcomp.algebra.mxalgebra]
+eqmxP [lemma, in mathcomp.algebra.mxalgebra]
+eqmx_semisimple [lemma, in mathcomp.character.mxrepresentation]
+eqmx_iso [lemma, in mathcomp.character.mxrepresentation]
+eqmx_module [lemma, in mathcomp.character.mxrepresentation]
+eqmx_rstabs [lemma, in mathcomp.character.mxrepresentation]
+eqmx_rstab [lemma, in mathcomp.character.mxrepresentation]
+eqmx_sums [lemma, in mathcomp.algebra.mxalgebra]
+eqmx_conform [lemma, in mathcomp.algebra.mxalgebra]
+eqmx_cast [lemma, in mathcomp.algebra.mxalgebra]
+eqmx_opp [lemma, in mathcomp.algebra.mxalgebra]
+eqmx_scale [lemma, in mathcomp.algebra.mxalgebra]
+eqmx_rank [lemma, in mathcomp.algebra.mxalgebra]
+eqmx_trans [lemma, in mathcomp.algebra.mxalgebra]
+eqmx_sym [lemma, in mathcomp.algebra.mxalgebra]
+eqmx_refl [lemma, in mathcomp.algebra.mxalgebra]
+eqmx_eq0 [lemma, in mathcomp.algebra.mxalgebra]
+eqmx0 [lemma, in mathcomp.algebra.mxalgebra]
+eqmx0P [lemma, in mathcomp.algebra.mxalgebra]
+eqn [definition, in mathcomp.ssreflect.ssrnat]
+eqnE [lemma, in mathcomp.ssreflect.ssrnat]
+eqnP [lemma, in mathcomp.ssreflect.ssrnat]
+eqn_mod_dvd [lemma, in mathcomp.ssreflect.div]
+eqn_dvd [lemma, in mathcomp.ssreflect.div]
+eqn_mul [lemma, in mathcomp.ssreflect.div]
+eqn_div [lemma, in mathcomp.ssreflect.div]
+eqn_modDr [lemma, in mathcomp.ssreflect.div]
+eqn_modDl [lemma, in mathcomp.ssreflect.div]
+eqn_sqr [lemma, in mathcomp.ssreflect.ssrnat]
+eqn_exp2r [lemma, in mathcomp.ssreflect.ssrnat]
+eqn_exp2l [lemma, in mathcomp.ssreflect.ssrnat]
+eqn_pmul2r [lemma, in mathcomp.ssreflect.ssrnat]
+eqn_pmul2l [lemma, in mathcomp.ssreflect.ssrnat]
+eqn_mul2r [lemma, in mathcomp.ssreflect.ssrnat]
+eqn_mul2l [lemma, in mathcomp.ssreflect.ssrnat]
+eqn_leq [lemma, in mathcomp.ssreflect.ssrnat]
+eqn_add2r [lemma, in mathcomp.ssreflect.ssrnat]
+eqn_add2l [lemma, in mathcomp.ssreflect.ssrnat]
+eqn0Ngt [lemma, in mathcomp.ssreflect.ssrnat]
+eqn0_xor_gt0 [inductive, in mathcomp.ssreflect.ssrnat]
+eqP [lemma, in mathcomp.ssreflect.eqtype]
+EqPath [section, in mathcomp.ssreflect.path]
+EqPath.e [variable, in mathcomp.ssreflect.path]
+EqPath.n0 [variable, in mathcomp.ssreflect.path]
+EqPath.T [variable, in mathcomp.ssreflect.path]
+EqPath.x0_cycle [variable, in mathcomp.ssreflect.path]
+EqPcore [section, in mathcomp.solvable.pgroup]
+EqPcore.gT [variable, in mathcomp.solvable.pgroup]
+eqperm [lemma, in mathcomp.solvable.burnside_app]
+eqperm_map2 [lemma, in mathcomp.solvable.burnside_app]
+eqperm_map [lemma, in mathcomp.solvable.burnside_app]
+EqPmap [section, in mathcomp.ssreflect.seq]
+EqPmapSub [section, in mathcomp.ssreflect.seq]
+EqPmapSub.insT [variable, in mathcomp.ssreflect.seq]
+EqPmapSub.p [variable, in mathcomp.ssreflect.seq]
+EqPmapSub.sT [variable, in mathcomp.ssreflect.seq]
+EqPmapSub.T [variable, in mathcomp.ssreflect.seq]
+EqPmap.aT [variable, in mathcomp.ssreflect.seq]
+EqPmap.f [variable, in mathcomp.ssreflect.seq]
+EqPmap.fK [variable, in mathcomp.ssreflect.seq]
+EqPmap.g [variable, in mathcomp.ssreflect.seq]
+EqPmap.rT [variable, in mathcomp.ssreflect.seq]
+EqPred [section, in mathcomp.ssreflect.eqtype]
+EqPred.b [variable, in mathcomp.ssreflect.eqtype]
+EqPred.T [variable, in mathcomp.ssreflect.eqtype]
+EqPred.T2 [variable, in mathcomp.ssreflect.eqtype]
+EqPred.u [variable, in mathcomp.ssreflect.eqtype]
+EqPred.x [variable, in mathcomp.ssreflect.eqtype]
+EqPred.y [variable, in mathcomp.ssreflect.eqtype]
+EqPred.z [variable, in mathcomp.ssreflect.eqtype]
+eqp_separable [lemma, in mathcomp.field.separable]
+EqQuotClass [constructor, in mathcomp.ssreflect.generic_quotient]
+eqquotE [lemma, in mathcomp.ssreflect.generic_quotient]
+eqquotP [lemma, in mathcomp.ssreflect.generic_quotient]
+EqQuotTheory [section, in mathcomp.ssreflect.generic_quotient]
+EqQuotTheory.e [variable, in mathcomp.ssreflect.generic_quotient]
+EqQuotTheory.Q [variable, in mathcomp.ssreflect.generic_quotient]
+EqQuotTheory.T [variable, in mathcomp.ssreflect.generic_quotient]
+EqQuotType [abbreviation, in mathcomp.ssreflect.generic_quotient]
+eqQuotType [record, in mathcomp.ssreflect.generic_quotient]
+EqQuotTypePack [constructor, in mathcomp.ssreflect.generic_quotient]
+EqQuotTypeStructure [section, in mathcomp.ssreflect.generic_quotient]
+EqQuotTypeStructure.eq_quot_op [variable, in mathcomp.ssreflect.generic_quotient]
+EqQuotTypeStructure.T [variable, in mathcomp.ssreflect.generic_quotient]
+EqQuotType_clone [definition, in mathcomp.ssreflect.generic_quotient]
+EqQuotType_pack [definition, in mathcomp.ssreflect.generic_quotient]
+eqr_expz2 [lemma, in mathcomp.algebra.ssrint]
+eqr_int [lemma, in mathcomp.algebra.ssrint]
+eqseq [definition, in mathcomp.ssreflect.seq]
+EqSeq [section, in mathcomp.ssreflect.seq]
+eqseqE [lemma, in mathcomp.ssreflect.seq]
+eqseqP [lemma, in mathcomp.ssreflect.seq]
+eqseq_rot [lemma, in mathcomp.ssreflect.seq]
+eqseq_class [definition, in mathcomp.ssreflect.seq]
+eqseq_rcons [lemma, in mathcomp.ssreflect.seq]
+eqseq_cat [lemma, in mathcomp.ssreflect.seq]
+eqseq_cons [lemma, in mathcomp.ssreflect.seq]
+EqSeq.EqIn [section, in mathcomp.ssreflect.seq]
+EqSeq.EqIn.a1 [variable, in mathcomp.ssreflect.seq]
+EqSeq.EqIn.a2 [variable, in mathcomp.ssreflect.seq]
+EqSeq.Filters [section, in mathcomp.ssreflect.seq]
+EqSeq.Filters.a [variable, in mathcomp.ssreflect.seq]
+EqSeq.inE [variable, in mathcomp.ssreflect.seq]
+EqSeq.n0 [variable, in mathcomp.ssreflect.seq]
+EqSeq.T [variable, in mathcomp.ssreflect.seq]
+EqSeq.x0 [variable, in mathcomp.ssreflect.seq]
+eqSS [lemma, in mathcomp.ssreflect.ssrnat]
+eqsVneq [lemma, in mathcomp.ssreflect.finset]
+EqTheory [section, in mathcomp.ssreflect.finfun]
+EqTheory.aT [variable, in mathcomp.ssreflect.finfun]
+EqTheory.rT [variable, in mathcomp.ssreflect.finfun]
+EqTrajectory [section, in mathcomp.ssreflect.path]
+EqTrajectory.f [variable, in mathcomp.ssreflect.path]
+EqTrajectory.T [variable, in mathcomp.ssreflect.path]
+EqTuple [section, in mathcomp.ssreflect.tuple]
+EqTuple.n [variable, in mathcomp.ssreflect.tuple]
+EqTuple.T [variable, in mathcomp.ssreflect.tuple]
+eqtype [library]
+EqTypePred [module, in mathcomp.ssreflect.eqtype]
+EqTypePredSig [module, in mathcomp.ssreflect.eqtype]
+EqTypePredSig.sort [axiom, in mathcomp.ssreflect.eqtype]
+Equality [module, in mathcomp.ssreflect.eqtype]
+Equality.axiom [definition, in mathcomp.ssreflect.eqtype]
+Equality.class [definition, in mathcomp.ssreflect.eqtype]
+Equality.ClassDef [section, in mathcomp.ssreflect.eqtype]
+Equality.ClassDef.cT [variable, in mathcomp.ssreflect.eqtype]
+Equality.ClassDef.T [variable, in mathcomp.ssreflect.eqtype]
+Equality.class_of [abbreviation, in mathcomp.ssreflect.eqtype]
+Equality.clone [definition, in mathcomp.ssreflect.eqtype]
+Equality.Exports [module, in mathcomp.ssreflect.eqtype]
+Equality.Exports.EqMixin [abbreviation, in mathcomp.ssreflect.eqtype]
+Equality.Exports.EqType [abbreviation, in mathcomp.ssreflect.eqtype]
+Equality.Exports.eqType [abbreviation, in mathcomp.ssreflect.eqtype]
+[ eqType of _ ] (form_scope) [notation, in mathcomp.ssreflect.eqtype]
+[ eqType of _ for _ ] (form_scope) [notation, in mathcomp.ssreflect.eqtype]
+[ eqMixin of _ ] (form_scope) [notation, in mathcomp.ssreflect.eqtype]
+Equality.Mixin [constructor, in mathcomp.ssreflect.eqtype]
+Equality.mixin_of [record, in mathcomp.ssreflect.eqtype]
+Equality.op [projection, in mathcomp.ssreflect.eqtype]
+Equality.pack [definition, in mathcomp.ssreflect.eqtype]
+Equality.Pack [constructor, in mathcomp.ssreflect.eqtype]
+Equality.sort [projection, in mathcomp.ssreflect.eqtype]
+Equality.type [record, in mathcomp.ssreflect.eqtype]
+EqualTo [constructor, in mathcomp.ssreflect.generic_quotient]
+equal_toE [lemma, in mathcomp.ssreflect.generic_quotient]
+equal_val [projection, in mathcomp.ssreflect.generic_quotient]
+equal_to [record, in mathcomp.ssreflect.generic_quotient]
+equiv [projection, in mathcomp.ssreflect.generic_quotient]
+equivalence_partition_pblock [lemma, in mathcomp.ssreflect.finset]
+equivalence_partitionP [lemma, in mathcomp.ssreflect.finset]
+equivalence_partition [definition, in mathcomp.ssreflect.finset]
+EquivClass [constructor, in mathcomp.ssreflect.generic_quotient]
+equivf [abbreviation, in mathcomp.algebra.fraction]
+EquivQuot [module, in mathcomp.ssreflect.generic_quotient]
+EquivQuotTheory [section, in mathcomp.ssreflect.generic_quotient]
+EquivQuotTheory.e [variable, in mathcomp.ssreflect.generic_quotient]
+EquivQuotTheory.Q [variable, in mathcomp.ssreflect.generic_quotient]
+EquivQuotTheory.T [variable, in mathcomp.ssreflect.generic_quotient]
+EquivQuot.canon [definition, in mathcomp.ssreflect.generic_quotient]
+EquivQuot.canon_id [lemma, in mathcomp.ssreflect.generic_quotient]
+EquivQuot.choiceMixin [definition, in mathcomp.ssreflect.generic_quotient]
+EquivQuot.eC [abbreviation, in mathcomp.ssreflect.generic_quotient]
+EquivQuot.encDE [abbreviation, in mathcomp.ssreflect.generic_quotient]
+EquivQuot.encDP [abbreviation, in mathcomp.ssreflect.generic_quotient]
+EquivQuot.eqMixin [lemma, in mathcomp.ssreflect.generic_quotient]
+EquivQuot.eqmodE [lemma, in mathcomp.ssreflect.generic_quotient]
+EquivQuot.eqmodP [lemma, in mathcomp.ssreflect.generic_quotient]
+EquivQuot.equivQTP [lemma, in mathcomp.ssreflect.generic_quotient]
+EquivQuot.EquivQuot [section, in mathcomp.ssreflect.generic_quotient]
+EquivQuot.equivQuotient [record, in mathcomp.ssreflect.generic_quotient]
+EquivQuot.EquivQuotient [constructor, in mathcomp.ssreflect.generic_quotient]
+EquivQuot.EquivQuot.C [variable, in mathcomp.ssreflect.generic_quotient]
+EquivQuot.EquivQuot.CD [variable, in mathcomp.ssreflect.generic_quotient]
+EquivQuot.EquivQuot.D [variable, in mathcomp.ssreflect.generic_quotient]
+EquivQuot.EquivQuot.DC [variable, in mathcomp.ssreflect.generic_quotient]
+EquivQuot.EquivQuot.eD [variable, in mathcomp.ssreflect.generic_quotient]
+EquivQuot.EquivQuot.encD [variable, in mathcomp.ssreflect.generic_quotient]
+EquivQuot.erepr [projection, in mathcomp.ssreflect.generic_quotient]
+EquivQuot.ereprK [lemma, in mathcomp.ssreflect.generic_quotient]
+EquivQuot.pi [definition, in mathcomp.ssreflect.generic_quotient]
+EquivQuot.pi_DC [lemma, in mathcomp.ssreflect.generic_quotient]
+EquivQuot.pi_CD [lemma, in mathcomp.ssreflect.generic_quotient]
+EquivQuot.qT [abbreviation, in mathcomp.ssreflect.generic_quotient]
+EquivQuot.quotClass [definition, in mathcomp.ssreflect.generic_quotient]
+EquivQuot.type_of [definition, in mathcomp.ssreflect.generic_quotient]
+EquivRel [abbreviation, in mathcomp.ssreflect.generic_quotient]
+EquivRel [section, in mathcomp.ssreflect.generic_quotient]
+EquivRelPack [constructor, in mathcomp.ssreflect.generic_quotient]
+EquivRel.e [variable, in mathcomp.ssreflect.generic_quotient]
+EquivRel.T [variable, in mathcomp.ssreflect.generic_quotient]
+equiv_subfext_is_equiv [lemma, in mathcomp.field.fieldext]
+equiv_subfext [definition, in mathcomp.field.fieldext]
+equiv_rtrans [lemma, in mathcomp.ssreflect.generic_quotient]
+equiv_ltrans [lemma, in mathcomp.ssreflect.generic_quotient]
+equiv_trans [lemma, in mathcomp.ssreflect.generic_quotient]
+equiv_sym [lemma, in mathcomp.ssreflect.generic_quotient]
+equiv_refl [lemma, in mathcomp.ssreflect.generic_quotient]
+equiv_pack [definition, in mathcomp.ssreflect.generic_quotient]
+equiv_class [definition, in mathcomp.ssreflect.generic_quotient]
+equiv_rel [record, in mathcomp.ssreflect.generic_quotient]
+equiv_class_of [inductive, in mathcomp.ssreflect.generic_quotient]
+eqVneq [lemma, in mathcomp.ssreflect.eqtype]
+eqVproper [lemma, in mathcomp.ssreflect.finset]
+eqxx [abbreviation, in mathcomp.ssreflect.eqtype]
+eqz_mod_dvd [lemma, in mathcomp.algebra.intdiv]
+eqz_mul [lemma, in mathcomp.algebra.intdiv]
+eqz_div [lemma, in mathcomp.algebra.intdiv]
+eqz_modDr [lemma, in mathcomp.algebra.intdiv]
+eqz_modDl [lemma, in mathcomp.algebra.intdiv]
+eqz_nat [lemma, in mathcomp.algebra.ssrint]
+eq_galP [lemma, in mathcomp.field.galois]
+eq_p'core [lemma, in mathcomp.solvable.pgroup]
+eq_pcore [lemma, in mathcomp.solvable.pgroup]
+eq_in_pcore [lemma, in mathcomp.solvable.pgroup]
+eq_Hall_pcore [lemma, in mathcomp.solvable.pgroup]
+eq_constt [lemma, in mathcomp.solvable.pgroup]
+eq_p_elt [lemma, in mathcomp.solvable.pgroup]
+eq_p'Hall [lemma, in mathcomp.solvable.pgroup]
+eq_pHall [lemma, in mathcomp.solvable.pgroup]
+eq_in_pHall [lemma, in mathcomp.solvable.pgroup]
+eq_p'group [lemma, in mathcomp.solvable.pgroup]
+eq_pgroup [lemma, in mathcomp.solvable.pgroup]
+eq_fcycle [lemma, in mathcomp.ssreflect.path]
+eq_fpath [lemma, in mathcomp.ssreflect.path]
+eq_sorted_irr [lemma, in mathcomp.ssreflect.path]
+eq_sorted [lemma, in mathcomp.ssreflect.path]
+eq_cycle [lemma, in mathcomp.ssreflect.path]
+eq_path [lemma, in mathcomp.ssreflect.path]
+eq_pcycle_mem [lemma, in mathcomp.fingroup.perm]
+eq_pnat [lemma, in mathcomp.ssreflect.prime]
+eq_in_pnat [lemma, in mathcomp.ssreflect.prime]
+eq_partn [lemma, in mathcomp.ssreflect.prime]
+eq_in_partn [lemma, in mathcomp.ssreflect.prime]
+eq_piP [lemma, in mathcomp.ssreflect.prime]
+eq_negn [lemma, in mathcomp.ssreflect.prime]
+eq_primes [lemma, in mathcomp.ssreflect.prime]
+eq_adjoin_separable_generator [lemma, in mathcomp.field.separable]
+eq_limg_ker0 [lemma, in mathcomp.algebra.vector]
+eq_in_limg [lemma, in mathcomp.algebra.vector]
+eq_span [lemma, in mathcomp.algebra.vector]
+eq_quot_countMixin [lemma, in mathcomp.ssreflect.generic_quotient]
+eq_op_trans [lemma, in mathcomp.ssreflect.generic_quotient]
+eq_quot_class [definition, in mathcomp.ssreflect.generic_quotient]
+eq_quot_sort [projection, in mathcomp.ssreflect.generic_quotient]
+eq_quot_eq_mixin [projection, in mathcomp.ssreflect.generic_quotient]
+eq_quot_quot_class [projection, in mathcomp.ssreflect.generic_quotient]
+eq_quot_class_of [record, in mathcomp.ssreflect.generic_quotient]
+eq_quot_mixin_of [definition, in mathcomp.ssreflect.generic_quotient]
+eq_lock [lemma, in mathcomp.ssreflect.generic_quotient]
+eq_from_tnth [lemma, in mathcomp.ssreflect.tuple]
+eq_block_mx [lemma, in mathcomp.algebra.matrix]
+eq_col_mx [lemma, in mathcomp.algebra.matrix]
+eq_row_mx [lemma, in mathcomp.algebra.matrix]
+eq_Aut [lemma, in mathcomp.fingroup.automorphism]
+eq_subZnat_irr [lemma, in mathcomp.character.character]
+eq_addZ_irr [lemma, in mathcomp.character.character]
+eq_scale_irr [lemma, in mathcomp.character.character]
+eq_signed_irr [lemma, in mathcomp.character.character]
+eq_scaled_irr [lemma, in mathcomp.character.character]
+eq_irr_mem_classP [lemma, in mathcomp.character.character]
+eq_sum_nth_irr [lemma, in mathcomp.character.character]
+eq_Mod8_D8 [lemma, in mathcomp.solvable.extremal]
+eq_from_flatten_shape [lemma, in mathcomp.ssreflect.seq]
+eq_mkseq [lemma, in mathcomp.ssreflect.seq]
+eq_pmap [lemma, in mathcomp.ssreflect.seq]
+eq_in_map [lemma, in mathcomp.ssreflect.seq]
+eq_map [lemma, in mathcomp.ssreflect.seq]
+eq_all_r [lemma, in mathcomp.ssreflect.seq]
+eq_has_r [lemma, in mathcomp.ssreflect.seq]
+eq_in_has [lemma, in mathcomp.ssreflect.seq]
+eq_in_all [lemma, in mathcomp.ssreflect.seq]
+eq_in_count [lemma, in mathcomp.ssreflect.seq]
+eq_in_find [lemma, in mathcomp.ssreflect.seq]
+eq_in_filter [lemma, in mathcomp.ssreflect.seq]
+eq_all [lemma, in mathcomp.ssreflect.seq]
+eq_has [lemma, in mathcomp.ssreflect.seq]
+eq_count [lemma, in mathcomp.ssreflect.seq]
+eq_filter [lemma, in mathcomp.ssreflect.seq]
+eq_find [lemma, in mathcomp.ssreflect.seq]
+eq_from_nth [lemma, in mathcomp.ssreflect.seq]
+eq_cfclass_IirrE [lemma, in mathcomp.character.inertia]
+eq_choose [lemma, in mathcomp.ssreflect.choice]
+eq_xchoose [lemma, in mathcomp.ssreflect.choice]
+eq_abelian_type_isog [lemma, in mathcomp.solvable.abelian]
+eq_homGrp [lemma, in mathcomp.fingroup.presentation]
+eq_card_prod [lemma, in mathcomp.ssreflect.fintype]
+eq_card_sub [lemma, in mathcomp.ssreflect.fintype]
+eq_invF [lemma, in mathcomp.ssreflect.fintype]
+eq_codom [lemma, in mathcomp.ssreflect.fintype]
+eq_image [lemma, in mathcomp.ssreflect.fintype]
+eq_forallb_in [lemma, in mathcomp.ssreflect.fintype]
+eq_forallb [lemma, in mathcomp.ssreflect.fintype]
+eq_existsb_in [lemma, in mathcomp.ssreflect.fintype]
+eq_existsb [lemma, in mathcomp.ssreflect.fintype]
+eq_disjoint1 [lemma, in mathcomp.ssreflect.fintype]
+eq_disjoint0 [lemma, in mathcomp.ssreflect.fintype]
+eq_disjoint_r [lemma, in mathcomp.ssreflect.fintype]
+eq_disjoint [lemma, in mathcomp.ssreflect.fintype]
+eq_proper_r [lemma, in mathcomp.ssreflect.fintype]
+eq_proper [lemma, in mathcomp.ssreflect.fintype]
+eq_subxx [lemma, in mathcomp.ssreflect.fintype]
+eq_subset_r [lemma, in mathcomp.ssreflect.fintype]
+eq_subset [lemma, in mathcomp.ssreflect.fintype]
+eq_card1 [lemma, in mathcomp.ssreflect.fintype]
+eq_cardT [lemma, in mathcomp.ssreflect.fintype]
+eq_card0 [lemma, in mathcomp.ssreflect.fintype]
+eq_card_trans [lemma, in mathcomp.ssreflect.fintype]
+eq_card [lemma, in mathcomp.ssreflect.fintype]
+eq_pick [lemma, in mathcomp.ssreflect.fintype]
+eq_enum [lemma, in mathcomp.ssreflect.fintype]
+eq_cfker_Res [lemma, in mathcomp.character.classfun]
+eq_orthonormal [lemma, in mathcomp.character.classfun]
+eq_pairwise_orthogonal [lemma, in mathcomp.character.classfun]
+eq_orthogonal [lemma, in mathcomp.character.classfun]
+eq_cfdotr [lemma, in mathcomp.character.classfun]
+eq_cfdotl [lemma, in mathcomp.character.classfun]
+eq_cfuni [lemma, in mathcomp.character.classfun]
+eq_mul_cfuni [lemma, in mathcomp.character.classfun]
+eq_binP [lemma, in mathcomp.ssreflect.ssrnat]
+eq_iterop [lemma, in mathcomp.ssreflect.ssrnat]
+eq_iteri [lemma, in mathcomp.ssreflect.ssrnat]
+eq_iter [lemma, in mathcomp.ssreflect.ssrnat]
+eq_ex_maxn [lemma, in mathcomp.ssreflect.ssrnat]
+eq_ex_minn [lemma, in mathcomp.ssreflect.ssrnat]
+eq_leq [lemma, in mathcomp.ssreflect.ssrnat]
+eq_map_poly [lemma, in mathcomp.algebra.poly]
+eq_prim_root_expr [lemma, in mathcomp.algebra.poly]
+eq_bigmax [lemma, in mathcomp.ssreflect.bigop]
+eq_bigmax_cond [lemma, in mathcomp.ssreflect.bigop]
+eq_big_idem [lemma, in mathcomp.ssreflect.bigop]
+eq_big_perm [lemma, in mathcomp.ssreflect.bigop]
+eq_big_idx [lemma, in mathcomp.ssreflect.bigop]
+eq_big_idx_seq [lemma, in mathcomp.ssreflect.bigop]
+eq_big_nat [lemma, in mathcomp.ssreflect.bigop]
+eq_big_seq [lemma, in mathcomp.ssreflect.bigop]
+eq_big [lemma, in mathcomp.ssreflect.bigop]
+eq_bigr [lemma, in mathcomp.ssreflect.bigop]
+eq_bigl [lemma, in mathcomp.ssreflect.bigop]
+eq_big_op [lemma, in mathcomp.ssreflect.bigop]
+eq_Tagged [lemma, in mathcomp.ssreflect.eqtype]
+eq_tag [lemma, in mathcomp.ssreflect.eqtype]
+eq_comparable [definition, in mathcomp.ssreflect.eqtype]
+eq_frel [lemma, in mathcomp.ssreflect.eqtype]
+eq_axiomK [lemma, in mathcomp.ssreflect.eqtype]
+eq_irrelevance [lemma, in mathcomp.ssreflect.eqtype]
+eq_sym [lemma, in mathcomp.ssreflect.eqtype]
+eq_refl [lemma, in mathcomp.ssreflect.eqtype]
+eq_op [definition, in mathcomp.ssreflect.eqtype]
+eq_abelem_subg_repr [lemma, in mathcomp.character.mxabelem]
+eq_rowg [lemma, in mathcomp.character.mxabelem]
+eq_homgr [lemma, in mathcomp.fingroup.morphism]
+eq_homgl [lemma, in mathcomp.fingroup.morphism]
+eq_in_morphim [lemma, in mathcomp.fingroup.morphism]
+eq_morphim [lemma, in mathcomp.fingroup.morphism]
+eq_mulVg1 [lemma, in mathcomp.fingroup.fingroup]
+eq_mulgV1 [lemma, in mathcomp.fingroup.fingroup]
+eq_invg_mul [lemma, in mathcomp.fingroup.fingroup]
+eq_invg1 [lemma, in mathcomp.fingroup.fingroup]
+eq_invg_sym [lemma, in mathcomp.fingroup.fingroup]
+eq_cpairZ [lemma, in mathcomp.solvable.center]
+eq_froots [lemma, in mathcomp.ssreflect.fingraph]
+eq_froot [lemma, in mathcomp.ssreflect.fingraph]
+eq_finv [lemma, in mathcomp.ssreflect.fingraph]
+eq_fcard [lemma, in mathcomp.ssreflect.fingraph]
+eq_fconnect [lemma, in mathcomp.ssreflect.fingraph]
+eq_roots [lemma, in mathcomp.ssreflect.fingraph]
+eq_root [lemma, in mathcomp.ssreflect.fingraph]
+eq_n_comp_r [lemma, in mathcomp.ssreflect.fingraph]
+eq_n_comp [lemma, in mathcomp.ssreflect.fingraph]
+eq_connect [lemma, in mathcomp.ssreflect.fingraph]
+eq_connect0 [lemma, in mathcomp.ssreflect.fingraph]
+eq_subG_cyclic [lemma, in mathcomp.solvable.cyclic]
+eq_expg_mod_order [lemma, in mathcomp.solvable.cyclic]
+eq_rank_unitmx [lemma, in mathcomp.algebra.mxalgebra]
+eq_genmx [lemma, in mathcomp.algebra.mxalgebra]
+eq_row_base [lemma, in mathcomp.algebra.mxalgebra]
+eq_row_sub [lemma, in mathcomp.algebra.mxalgebra]
+eq_pblock [lemma, in mathcomp.ssreflect.finset]
+eq_in_imset2 [lemma, in mathcomp.ssreflect.finset]
+eq_in_imset [lemma, in mathcomp.ssreflect.finset]
+eq_imset [lemma, in mathcomp.ssreflect.finset]
+eq_preimset [lemma, in mathcomp.ssreflect.finset]
+Eq0NotPos [constructor, in mathcomp.ssreflect.ssrnat]
+ErV [abbreviation, in mathcomp.character.mxabelem]
+Euclid_dvdX [lemma, in mathcomp.ssreflect.prime]
+Euclid_dvd1 [lemma, in mathcomp.ssreflect.prime]
+Euclid_dvdM [lemma, in mathcomp.ssreflect.prime]
+Euler_exp_totient [lemma, in mathcomp.solvable.cyclic]
+eval [abbreviation, in mathcomp.character.mxrepresentation]
+eval [abbreviation, in mathcomp.algebra.polyXY]
+eval_mxmodule [lemma, in mathcomp.character.mxrepresentation]
+eval_bigmul [abbreviation, in mathcomp.field.closed_field]
+eval_poly1 [lemma, in mathcomp.field.closed_field]
+eval_poly_mulM [lemma, in mathcomp.field.closed_field]
+eval_natmulpT [lemma, in mathcomp.field.closed_field]
+eval_opppT [lemma, in mathcomp.field.closed_field]
+eval_mulpT [lemma, in mathcomp.field.closed_field]
+eval_sumpT [lemma, in mathcomp.field.closed_field]
+eval_amulXnT [lemma, in mathcomp.field.closed_field]
+eval_lift [lemma, in mathcomp.field.closed_field]
+eval_poly [definition, in mathcomp.field.closed_field]
+even_prime [lemma, in mathcomp.ssreflect.prime]
+ev_ax [abbreviation, in mathcomp.ssreflect.eqtype]
+exchange_big_nat [lemma, in mathcomp.ssreflect.bigop]
+exchange_big_dep_nat [lemma, in mathcomp.ssreflect.bigop]
+exchange_big [lemma, in mathcomp.ssreflect.bigop]
+exchange_big_dep [lemma, in mathcomp.ssreflect.bigop]
+existsb_tnth [lemma, in mathcomp.ssreflect.tuple]
+existsP [lemma, in mathcomp.ssreflect.fintype]
+existsPP [lemma, in mathcomp.ssreflect.fintype]
+exists_acomps [lemma, in mathcomp.solvable.jordanholder]
+exists_comps [lemma, in mathcomp.solvable.jordanholder]
+exists_eq_inP [lemma, in mathcomp.ssreflect.fintype]
+exists_inP [lemma, in mathcomp.ssreflect.fintype]
+exists_eqP [lemma, in mathcomp.ssreflect.fintype]
+ExMaxn [section, in mathcomp.ssreflect.ssrnat]
+ExMaxnSpec [constructor, in mathcomp.ssreflect.ssrnat]
+ExMaxn.exP [variable, in mathcomp.ssreflect.ssrnat]
+ExMaxn.m [variable, in mathcomp.ssreflect.ssrnat]
+ExMaxn.P [variable, in mathcomp.ssreflect.ssrnat]
+ExMaxn.ubP [variable, in mathcomp.ssreflect.ssrnat]
+ExMinn [section, in mathcomp.ssreflect.ssrnat]
+ExMinnSpec [constructor, in mathcomp.ssreflect.ssrnat]
+ExMinn.exP [variable, in mathcomp.ssreflect.ssrnat]
+ExMinn.P [variable, in mathcomp.ssreflect.ssrnat]
+expand_det_col [lemma, in mathcomp.algebra.matrix]
+expand_det_row [lemma, in mathcomp.algebra.matrix]
+expand_cofactor [lemma, in mathcomp.algebra.matrix]
+expfV [lemma, in mathcomp.algebra.ssrint]
+expfzDr [lemma, in mathcomp.algebra.ssrint]
+expfzMl [lemma, in mathcomp.algebra.ssrint]
+expfz_n0addr [lemma, in mathcomp.algebra.ssrint]
+expfz_neq0 [lemma, in mathcomp.algebra.ssrint]
+expfz_eq0 [lemma, in mathcomp.algebra.ssrint]
+expf_card [lemma, in mathcomp.field.finfield]
+expgAC [lemma, in mathcomp.fingroup.fingroup]
+expgD [lemma, in mathcomp.fingroup.fingroup]
+expgK [lemma, in mathcomp.solvable.cyclic]
+expgM [lemma, in mathcomp.fingroup.fingroup]
+expgMn [lemma, in mathcomp.fingroup.fingroup]
+expgn [definition, in mathcomp.fingroup.fingroup]
+expgnE [lemma, in mathcomp.fingroup.fingroup]
+expgn_rec [definition, in mathcomp.fingroup.fingroup]
+expgS [lemma, in mathcomp.fingroup.fingroup]
+expgSr [lemma, in mathcomp.fingroup.fingroup]
+expgVn [lemma, in mathcomp.fingroup.fingroup]
+expg_exponent [lemma, in mathcomp.solvable.abelian]
+expg_mod_order [lemma, in mathcomp.fingroup.fingroup]
+expg_mod [lemma, in mathcomp.fingroup.fingroup]
+expg_order [lemma, in mathcomp.fingroup.fingroup]
+expg_invn [definition, in mathcomp.solvable.cyclic]
+expg_zneg [lemma, in mathcomp.solvable.cyclic]
+expg_znat [lemma, in mathcomp.solvable.cyclic]
+expg_cardG [lemma, in mathcomp.solvable.cyclic]
+expg0 [lemma, in mathcomp.fingroup.fingroup]
+expg1 [lemma, in mathcomp.fingroup.fingroup]
+expg1n [lemma, in mathcomp.fingroup.fingroup]
+expIn [lemma, in mathcomp.ssreflect.ssrnat]
+expMg_Rmul [lemma, in mathcomp.solvable.commutator]
+expn [definition, in mathcomp.ssreflect.ssrnat]
+expnAC [lemma, in mathcomp.ssreflect.ssrnat]
+expnB [lemma, in mathcomp.ssreflect.div]
+expnD [lemma, in mathcomp.ssreflect.ssrnat]
+expnDn [definition, in mathcomp.ssreflect.binomial]
+expnE [lemma, in mathcomp.ssreflect.ssrnat]
+expnI [lemma, in mathcomp.ssreflect.ssrnat]
+expnM [lemma, in mathcomp.ssreflect.ssrnat]
+expnMn [lemma, in mathcomp.ssreflect.ssrnat]
+expNrz [lemma, in mathcomp.algebra.ssrint]
+expnS [lemma, in mathcomp.ssreflect.ssrnat]
+expnSr [lemma, in mathcomp.ssreflect.ssrnat]
+expn_max [lemma, in mathcomp.ssreflect.div]
+expn_min [lemma, in mathcomp.ssreflect.div]
+expn_eq0 [lemma, in mathcomp.ssreflect.ssrnat]
+expn_gt0 [lemma, in mathcomp.ssreflect.ssrnat]
+expn_rec [definition, in mathcomp.ssreflect.ssrnat]
+expn_sum [lemma, in mathcomp.ssreflect.bigop]
+expn0 [lemma, in mathcomp.ssreflect.ssrnat]
+expn1 [lemma, in mathcomp.ssreflect.ssrnat]
+expN1r [lemma, in mathcomp.algebra.ssrint]
+exponent [definition, in mathcomp.solvable.abelian]
+ExponentAbelem [section, in mathcomp.solvable.abelian]
+ExponentAbelem.gT [variable, in mathcomp.solvable.abelian]
+exponentJ [lemma, in mathcomp.solvable.abelian]
+exponentP [lemma, in mathcomp.solvable.abelian]
+ExponentPextraspecialTheory [section, in mathcomp.solvable.extraspecial]
+ExponentPextraspecialTheory.p [variable, in mathcomp.solvable.extraspecial]
+ExponentPextraspecialTheory.p_gt0 [variable, in mathcomp.solvable.extraspecial]
+ExponentPextraspecialTheory.p_gt1 [variable, in mathcomp.solvable.extraspecial]
+ExponentPextraspecialTheory.p_pr [variable, in mathcomp.solvable.extraspecial]
+exponentS [lemma, in mathcomp.solvable.abelian]
+exponent_pX1p2n [lemma, in mathcomp.solvable.extraspecial]
+exponent_pX1p2 [lemma, in mathcomp.solvable.extraspecial]
+exponent_dprod_homocyclic [lemma, in mathcomp.solvable.abelian]
+exponent_quotient [lemma, in mathcomp.solvable.abelian]
+exponent_isog [lemma, in mathcomp.solvable.abelian]
+exponent_injm [lemma, in mathcomp.solvable.abelian]
+exponent_morphim [lemma, in mathcomp.solvable.abelian]
+exponent_Zgroup [lemma, in mathcomp.solvable.abelian]
+exponent_Hall [lemma, in mathcomp.solvable.abelian]
+exponent_cyclic [lemma, in mathcomp.solvable.abelian]
+exponent_cycle [lemma, in mathcomp.solvable.abelian]
+exponent_witness [lemma, in mathcomp.solvable.abelian]
+exponent_gt0 [lemma, in mathcomp.solvable.abelian]
+exponent_dvdn [lemma, in mathcomp.solvable.abelian]
+exponent_Ohm1_class2 [lemma, in mathcomp.solvable.maximal]
+exponent_2extraspecial [lemma, in mathcomp.solvable.maximal]
+exponent_special [lemma, in mathcomp.solvable.maximal]
+exponent_mx_group [lemma, in mathcomp.character.mxabelem]
+exponent1 [lemma, in mathcomp.solvable.abelian]
+exponent2_abelem [lemma, in mathcomp.solvable.abelian]
+exprMz_comm [lemma, in mathcomp.algebra.ssrint]
+exprnN [lemma, in mathcomp.algebra.ssrint]
+exprnP [lemma, in mathcomp.algebra.ssrint]
+exprN1 [lemma, in mathcomp.algebra.ssrint]
+exprSz [lemma, in mathcomp.algebra.ssrint]
+exprSzr [lemma, in mathcomp.algebra.ssrint]
+exprz [definition, in mathcomp.algebra.ssrint]
+exprzAC [lemma, in mathcomp.algebra.ssrint]
+exprzDr [lemma, in mathcomp.algebra.ssrint]
+exprzD_ss [lemma, in mathcomp.algebra.ssrint]
+exprzD_Nnat [lemma, in mathcomp.algebra.ssrint]
+exprzD_nat [lemma, in mathcomp.algebra.ssrint]
+ExprzField [section, in mathcomp.algebra.ssrint]
+ExprzField.F [variable, in mathcomp.algebra.ssrint]
+ExprzIdomain [section, in mathcomp.algebra.ssrint]
+ExprzIdomain.R [variable, in mathcomp.algebra.ssrint]
+exprzMl [lemma, in mathcomp.algebra.ssrint]
+exprzMzl [lemma, in mathcomp.algebra.ssrint]
+ExprzOrder [section, in mathcomp.algebra.ssrint]
+ExprzOrder.R [variable, in mathcomp.algebra.ssrint]
+ExprzUnitRing [section, in mathcomp.algebra.ssrint]
+ExprzUnitRing.R [variable, in mathcomp.algebra.ssrint]
+exprz_gte0 [definition, in mathcomp.algebra.ssrint]
+exprz_gt0 [lemma, in mathcomp.algebra.ssrint]
+exprz_ge0 [lemma, in mathcomp.algebra.ssrint]
+exprz_pintl [lemma, in mathcomp.algebra.ssrint]
+exprz_pmulzl [lemma, in mathcomp.algebra.ssrint]
+Exprz_Zint_UnitRing.R [variable, in mathcomp.algebra.ssrint]
+Exprz_Zint_UnitRing [section, in mathcomp.algebra.ssrint]
+exprz_out [lemma, in mathcomp.algebra.ssrint]
+exprz_exp [lemma, in mathcomp.algebra.ssrint]
+exprz_inv [lemma, in mathcomp.algebra.ssrint]
+expr0z [lemma, in mathcomp.algebra.ssrint]
+expr1z [lemma, in mathcomp.algebra.ssrint]
+expS_cfunE [lemma, in mathcomp.character.classfun]
+expv [definition, in mathcomp.field.falgebra]
+expvD [lemma, in mathcomp.field.falgebra]
+expvM [lemma, in mathcomp.field.falgebra]
+expvS [lemma, in mathcomp.field.falgebra]
+expvSl [lemma, in mathcomp.field.falgebra]
+expvSr [lemma, in mathcomp.field.falgebra]
+expv_id [lemma, in mathcomp.field.falgebra]
+expv_line [lemma, in mathcomp.field.falgebra]
+expv0 [lemma, in mathcomp.field.falgebra]
+expv0n [lemma, in mathcomp.field.falgebra]
+expv1 [lemma, in mathcomp.field.falgebra]
+expv1n [lemma, in mathcomp.field.falgebra]
+expv2 [lemma, in mathcomp.field.falgebra]
+expzB [lemma, in mathcomp.algebra.intdiv]
+expz_min [lemma, in mathcomp.algebra.intdiv]
+exp_orderC [lemma, in mathcomp.field.algnum]
+exp_cforder [lemma, in mathcomp.character.classfun]
+exp_cfunE [lemma, in mathcomp.character.classfun]
+exp_prim_root [lemma, in mathcomp.algebra.poly]
+exp_finIndexType [definition, in mathcomp.ssreflect.finfun]
+exp0n [lemma, in mathcomp.ssreflect.ssrnat]
+exp0rz [lemma, in mathcomp.algebra.ssrint]
+exp1n [lemma, in mathcomp.ssreflect.ssrnat]
+exp1rz [lemma, in mathcomp.algebra.ssrint]
+ExtCprod [section, in mathcomp.solvable.center]
+ExtCprod.gTH [variable, in mathcomp.solvable.center]
+ExtCprod.gTK [variable, in mathcomp.solvable.center]
+ExtCprod.gt_ [variable, in mathcomp.solvable.center]
+ExtCprod.G_ [variable, in mathcomp.solvable.center]
+ExtCprod.H [variable, in mathcomp.solvable.center]
+ExtCprod.K [variable, in mathcomp.solvable.center]
+extendDerivation [definition, in mathcomp.field.separable]
+extendDerivationP [lemma, in mathcomp.field.separable]
+extendDerivation_horner [lemma, in mathcomp.field.separable]
+extendDerivation_id [lemma, in mathcomp.field.separable]
+extendDerivation_subproof [lemma, in mathcomp.field.separable]
+extendible_irr_invariant [lemma, in mathcomp.character.inertia]
+ExtendInvariantIrr [section, in mathcomp.character.inertia]
+ExtendInvariantIrr.ConsttIndExtendible [section, in mathcomp.character.inertia]
+ExtendInvariantIrr.ConsttIndExtendible.c [variable, in mathcomp.character.inertia]
+ExtendInvariantIrr.ConsttIndExtendible.chi [variable, in mathcomp.character.inertia]
+ExtendInvariantIrr.ConsttIndExtendible.cNt [variable, in mathcomp.character.inertia]
+ExtendInvariantIrr.ConsttIndExtendible.G [variable, in mathcomp.character.inertia]
+ExtendInvariantIrr.ConsttIndExtendible.IGtheta [variable, in mathcomp.character.inertia]
+ExtendInvariantIrr.ConsttIndExtendible.N [variable, in mathcomp.character.inertia]
+ExtendInvariantIrr.ConsttIndExtendible.nNG [variable, in mathcomp.character.inertia]
+ExtendInvariantIrr.ConsttIndExtendible.nsNG [variable, in mathcomp.character.inertia]
+ExtendInvariantIrr.ConsttIndExtendible.sNG [variable, in mathcomp.character.inertia]
+ExtendInvariantIrr.ConsttIndExtendible.t [variable, in mathcomp.character.inertia]
+ExtendInvariantIrr.ConsttIndExtendible.theta [variable, in mathcomp.character.inertia]
+ExtendInvariantIrr.gT [variable, in mathcomp.character.inertia]
+extend_group_splitting_field [lemma, in mathcomp.character.mxrepresentation]
+extend_algC_subfield_aut [lemma, in mathcomp.field.algnum]
+extend_solvable_coprime_irr [lemma, in mathcomp.character.inertia]
+extend_coprime_linear_char [lemma, in mathcomp.character.inertia]
+extend_linear_char_from_Sylow [lemma, in mathcomp.character.inertia]
+extend_to_cfdet [lemma, in mathcomp.character.inertia]
+extend_cyclic_Mho [lemma, in mathcomp.solvable.abelian]
+extend_cfConjC_subset [lemma, in mathcomp.character.classfun]
+extend_number [definition, in mathcomp.ssreflect.ssrnat]
+Extensionality [section, in mathcomp.ssreflect.bigop]
+Extensionality.idx [variable, in mathcomp.ssreflect.bigop]
+Extensionality.op [variable, in mathcomp.ssreflect.bigop]
+Extensionality.R [variable, in mathcomp.ssreflect.bigop]
+Extensionality.SeqExtension [section, in mathcomp.ssreflect.bigop]
+Extensionality.SeqExtension.I [variable, in mathcomp.ssreflect.bigop]
+ExternalAction [section, in mathcomp.solvable.hall]
+ExternalAction.A [variable, in mathcomp.solvable.hall]
+ExternalAction.aT [variable, in mathcomp.solvable.hall]
+ExternalAction.FullExtension [section, in mathcomp.solvable.hall]
+ExternalAction.FullExtension.coGA [variable, in mathcomp.solvable.hall]
+ExternalAction.FullExtension.coGA' [variable, in mathcomp.solvable.hall]
+ExternalAction.FullExtension.injA [variable, in mathcomp.solvable.hall]
+ExternalAction.FullExtension.injG [variable, in mathcomp.solvable.hall]
+ExternalAction.FullExtension.nGA' [variable, in mathcomp.solvable.hall]
+ExternalAction.FullExtension.solG [variable, in mathcomp.solvable.hall]
+ExternalAction.FullExtension.solG' [variable, in mathcomp.solvable.hall]
+ExternalAction.G [variable, in mathcomp.solvable.hall]
+ExternalAction.gT [variable, in mathcomp.solvable.hall]
+ExternalAction.pi [variable, in mathcomp.solvable.hall]
+ExternalAction.to [variable, in mathcomp.solvable.hall]
+ExternalDirProd [section, in mathcomp.fingroup.gproduct]
+ExternalDirProd.gT1 [variable, in mathcomp.fingroup.gproduct]
+ExternalDirProd.gT2 [variable, in mathcomp.fingroup.gproduct]
+ExternalSDirProd [section, in mathcomp.fingroup.gproduct]
+ExternalSDirProd.A [variable, in mathcomp.fingroup.gproduct]
+ExternalSDirProd.aT [variable, in mathcomp.fingroup.gproduct]
+ExternalSDirProd.D [variable, in mathcomp.fingroup.gproduct]
+ExternalSDirProd.G [variable, in mathcomp.fingroup.gproduct]
+ExternalSDirProd.R [variable, in mathcomp.fingroup.gproduct]
+ExternalSDirProd.rT [variable, in mathcomp.fingroup.gproduct]
+ExternalSDirProd.sAD [variable, in mathcomp.fingroup.gproduct]
+ExternalSDirProd.sGR [variable, in mathcomp.fingroup.gproduct]
+ExternalSDirProd.to [variable, in mathcomp.fingroup.gproduct]
+external_action_im_coprime [lemma, in mathcomp.solvable.hall]
+extgK [abbreviation, in mathcomp.solvable.extremal]
+extprod_groupMixin [definition, in mathcomp.fingroup.gproduct]
+extprod_mulgA [lemma, in mathcomp.fingroup.gproduct]
+extprod_mulVg [lemma, in mathcomp.fingroup.gproduct]
+extprod_mul1g [lemma, in mathcomp.fingroup.gproduct]
+extprod_invg [definition, in mathcomp.fingroup.gproduct]
+extprod_mulg [definition, in mathcomp.fingroup.gproduct]
+Extraspecial [section, in mathcomp.solvable.maximal]
+extraspecial [definition, in mathcomp.solvable.maximal]
+Extraspecial [section, in mathcomp.character.mxabelem]
+extraspecial [library]
+extraspecial_structure [lemma, in mathcomp.solvable.maximal]
+extraspecial_nonabelian [lemma, in mathcomp.solvable.maximal]
+extraspecial_prime [lemma, in mathcomp.solvable.maximal]
+extraspecial_repr_structure [lemma, in mathcomp.character.mxabelem]
+Extraspecial.Basic [section, in mathcomp.solvable.maximal]
+Extraspecial.Basic.esS [variable, in mathcomp.solvable.maximal]
+Extraspecial.Basic.pS [variable, in mathcomp.solvable.maximal]
+Extraspecial.Basic.pZ [variable, in mathcomp.solvable.maximal]
+Extraspecial.Basic.S [variable, in mathcomp.solvable.maximal]
+Extraspecial.esS [variable, in mathcomp.character.mxabelem]
+Extraspecial.ExtraspecialFormspace [section, in mathcomp.solvable.maximal]
+Extraspecial.ExtraspecialFormspace.esG [variable, in mathcomp.solvable.maximal]
+Extraspecial.ExtraspecialFormspace.G [variable, in mathcomp.solvable.maximal]
+Extraspecial.ExtraspecialFormspace.oZ [variable, in mathcomp.solvable.maximal]
+Extraspecial.ExtraspecialFormspace.pG [variable, in mathcomp.solvable.maximal]
+Extraspecial.ExtraspecialFormspace.p_gt0 [variable, in mathcomp.solvable.maximal]
+Extraspecial.ExtraspecialFormspace.p_gt1 [variable, in mathcomp.solvable.maximal]
+Extraspecial.ExtraspecialFormspace.p_pr [variable, in mathcomp.solvable.maximal]
+Extraspecial.F [variable, in mathcomp.character.mxabelem]
+Extraspecial.ffulU [variable, in mathcomp.character.mxabelem]
+Extraspecial.F'S [variable, in mathcomp.character.mxabelem]
+Extraspecial.gT [variable, in mathcomp.solvable.maximal]
+Extraspecial.gT [variable, in mathcomp.character.mxabelem]
+Extraspecial.m [variable, in mathcomp.character.mxabelem]
+Extraspecial.modIp' [variable, in mathcomp.character.mxabelem]
+Extraspecial.n [variable, in mathcomp.character.mxabelem]
+Extraspecial.oSpn [variable, in mathcomp.character.mxabelem]
+Extraspecial.oZp [variable, in mathcomp.character.mxabelem]
+Extraspecial.p [variable, in mathcomp.solvable.maximal]
+Extraspecial.p [variable, in mathcomp.character.mxabelem]
+Extraspecial.pS [variable, in mathcomp.character.mxabelem]
+Extraspecial.p_gt1 [variable, in mathcomp.character.mxabelem]
+Extraspecial.p_gt0 [variable, in mathcomp.character.mxabelem]
+Extraspecial.p_pr [variable, in mathcomp.character.mxabelem]
+Extraspecial.rS [variable, in mathcomp.character.mxabelem]
+Extraspecial.rT [variable, in mathcomp.solvable.maximal]
+Extraspecial.rZ [variable, in mathcomp.character.mxabelem]
+Extraspecial.S [variable, in mathcomp.character.mxabelem]
+Extraspecial.simU [variable, in mathcomp.character.mxabelem]
+Extraspecial.splitF [variable, in mathcomp.character.mxabelem]
+Extraspecial.StructureCorollaries [section, in mathcomp.solvable.maximal]
+Extraspecial.StructureCorollaries.esS [variable, in mathcomp.solvable.maximal]
+Extraspecial.StructureCorollaries.oZ [variable, in mathcomp.solvable.maximal]
+Extraspecial.StructureCorollaries.pS [variable, in mathcomp.solvable.maximal]
+Extraspecial.StructureCorollaries.p_pr [variable, in mathcomp.solvable.maximal]
+Extraspecial.StructureCorollaries.S [variable, in mathcomp.solvable.maximal]
+Extraspecial.sZS [variable, in mathcomp.character.mxabelem]
+Extraspecial.U [variable, in mathcomp.character.mxabelem]
+Extrema [section, in mathcomp.ssreflect.fintype]
+Extremal [module, in mathcomp.solvable.extremal]
+extremal [library]
+ExtremalTheory [section, in mathcomp.solvable.extremal]
+ExtremalTheory.DihedralGroup [section, in mathcomp.solvable.extremal]
+ExtremalTheory.DihedralGroup.def_q [variable, in mathcomp.solvable.extremal]
+ExtremalTheory.DihedralGroup.def2 [variable, in mathcomp.solvable.extremal]
+ExtremalTheory.DihedralGroup.Dihedral_extension.even_p [variable, in mathcomp.solvable.extremal]
+ExtremalTheory.DihedralGroup.Dihedral_extension.p_gt1 [variable, in mathcomp.solvable.extremal]
+ExtremalTheory.DihedralGroup.Dihedral_extension.p [variable, in mathcomp.solvable.extremal]
+ExtremalTheory.DihedralGroup.Dihedral_extension [section, in mathcomp.solvable.extremal]
+ExtremalTheory.DihedralGroup.m [variable, in mathcomp.solvable.extremal]
+ExtremalTheory.DihedralGroup.q [variable, in mathcomp.solvable.extremal]
+ExtremalTheory.DihedralGroup.q_gt1 [variable, in mathcomp.solvable.extremal]
+ExtremalTheory.ExtremalClass [section, in mathcomp.solvable.extremal]
+ExtremalTheory.ExtremalClass.G [variable, in mathcomp.solvable.extremal]
+ExtremalTheory.ExtremalClass.gT [variable, in mathcomp.solvable.extremal]
+ExtremalTheory.ExtremalStructure [section, in mathcomp.solvable.extremal]
+ExtremalTheory.ExtremalStructure.def2qr [variable, in mathcomp.solvable.extremal]
+ExtremalTheory.ExtremalStructure.G [variable, in mathcomp.solvable.extremal]
+ExtremalTheory.ExtremalStructure.gT [variable, in mathcomp.solvable.extremal]
+ExtremalTheory.ExtremalStructure.m [variable, in mathcomp.solvable.extremal]
+ExtremalTheory.ExtremalStructure.Mxy [variable, in mathcomp.solvable.extremal]
+ExtremalTheory.ExtremalStructure.My [variable, in mathcomp.solvable.extremal]
+ExtremalTheory.ExtremalStructure.n [variable, in mathcomp.solvable.extremal]
+ExtremalTheory.ExtremalStructure.q [variable, in mathcomp.solvable.extremal]
+ExtremalTheory.ExtremalStructure.q_gt0 [variable, in mathcomp.solvable.extremal]
+ExtremalTheory.ExtremalStructure.r [variable, in mathcomp.solvable.extremal]
+ExtremalTheory.ExtremalStructure.r_gt0 [variable, in mathcomp.solvable.extremal]
+ExtremalTheory.ExtremalStructure.X [variable, in mathcomp.solvable.extremal]
+ExtremalTheory.ExtremalStructure.x [variable, in mathcomp.solvable.extremal]
+ExtremalTheory.ExtremalStructure.xyG [variable, in mathcomp.solvable.extremal]
+ExtremalTheory.ExtremalStructure.Y [variable, in mathcomp.solvable.extremal]
+ExtremalTheory.ExtremalStructure.y [variable, in mathcomp.solvable.extremal]
+ExtremalTheory.ExtremalStructure.yG [variable, in mathcomp.solvable.extremal]
+ExtremalTheory.ModularGroup [section, in mathcomp.solvable.extremal]
+ExtremalTheory.ModularGroup.def_r [variable, in mathcomp.solvable.extremal]
+ExtremalTheory.ModularGroup.def_q [variable, in mathcomp.solvable.extremal]
+ExtremalTheory.ModularGroup.def_p [variable, in mathcomp.solvable.extremal]
+ExtremalTheory.ModularGroup.def_n [variable, in mathcomp.solvable.extremal]
+ExtremalTheory.ModularGroup.ltqm [variable, in mathcomp.solvable.extremal]
+ExtremalTheory.ModularGroup.ltrq [variable, in mathcomp.solvable.extremal]
+ExtremalTheory.ModularGroup.m [variable, in mathcomp.solvable.extremal]
+ExtremalTheory.ModularGroup.n [variable, in mathcomp.solvable.extremal]
+ExtremalTheory.ModularGroup.n_gt2 [variable, in mathcomp.solvable.extremal]
+ExtremalTheory.ModularGroup.p [variable, in mathcomp.solvable.extremal]
+ExtremalTheory.ModularGroup.p_gt0 [variable, in mathcomp.solvable.extremal]
+ExtremalTheory.ModularGroup.p_gt1 [variable, in mathcomp.solvable.extremal]
+ExtremalTheory.ModularGroup.p_pr [variable, in mathcomp.solvable.extremal]
+ExtremalTheory.ModularGroup.q [variable, in mathcomp.solvable.extremal]
+ExtremalTheory.ModularGroup.q_gt1 [variable, in mathcomp.solvable.extremal]
+ExtremalTheory.ModularGroup.r [variable, in mathcomp.solvable.extremal]
+ExtremalTheory.ModularGroup.r_gt0 [variable, in mathcomp.solvable.extremal]
+ExtremalTheory.Quaternion [section, in mathcomp.solvable.extremal]
+ExtremalTheory.Quaternion.defQ [variable, in mathcomp.solvable.extremal]
+ExtremalTheory.Quaternion.GrpQ [variable, in mathcomp.solvable.extremal]
+ExtremalTheory.Quaternion.m [variable, in mathcomp.solvable.extremal]
+ExtremalTheory.Quaternion.n [variable, in mathcomp.solvable.extremal]
+ExtremalTheory.Quaternion.n_gt2 [variable, in mathcomp.solvable.extremal]
+ExtremalTheory.Quaternion.q [variable, in mathcomp.solvable.extremal]
+ExtremalTheory.Quaternion.r [variable, in mathcomp.solvable.extremal]
+extremal_class [definition, in mathcomp.solvable.extremal]
+extremal_group_finMixin [definition, in mathcomp.solvable.extremal]
+extremal_group_countMixin [definition, in mathcomp.solvable.extremal]
+extremal_group_choiceMixin [definition, in mathcomp.solvable.extremal]
+extremal_group_eqMixin [definition, in mathcomp.solvable.extremal]
+extremal_group_type [inductive, in mathcomp.solvable.extremal]
+extremal_generators_facts [lemma, in mathcomp.solvable.extremal]
+extremal_generators [definition, in mathcomp.solvable.extremal]
+Extremal.act_dom [lemma, in mathcomp.solvable.extremal]
+Extremal.act_morphism [definition, in mathcomp.solvable.extremal]
+Extremal.aut_dvdn [lemma, in mathcomp.solvable.extremal]
+Extremal.aut_of [definition, in mathcomp.solvable.extremal]
+Extremal.B [abbreviation, in mathcomp.solvable.extremal]
+Extremal.base_act [definition, in mathcomp.solvable.extremal]
+Extremal.card [lemma, in mathcomp.solvable.extremal]
+Extremal.Construction [section, in mathcomp.solvable.extremal]
+Extremal.Construction.a [variable, in mathcomp.solvable.extremal]
+Extremal.Construction.b [variable, in mathcomp.solvable.extremal]
+Extremal.Construction.e [variable, in mathcomp.solvable.extremal]
+Extremal.Construction.p [variable, in mathcomp.solvable.extremal]
+Extremal.Construction.p_gt1 [variable, in mathcomp.solvable.extremal]
+Extremal.Construction.q [variable, in mathcomp.solvable.extremal]
+Extremal.Construction.q_gt1 [variable, in mathcomp.solvable.extremal]
+Extremal.gact [definition, in mathcomp.solvable.extremal]
+Extremal.Grp [lemma, in mathcomp.solvable.extremal]
+Extremal.gtype [definition, in mathcomp.solvable.extremal]
+Extremal.gtype_key [lemma, in mathcomp.solvable.extremal]
+extremal2 [definition, in mathcomp.solvable.extremal]
+extremal2_structure [lemma, in mathcomp.solvable.extremal]
+Extrema.arg_pred [variable, in mathcomp.ssreflect.fintype]
+Extrema.exFP [variable, in mathcomp.ssreflect.fintype]
+Extrema.F [variable, in mathcomp.ssreflect.fintype]
+Extrema.FP [variable, in mathcomp.ssreflect.fintype]
+Extrema.FP_F [variable, in mathcomp.ssreflect.fintype]
+Extrema.I [variable, in mathcomp.ssreflect.fintype]
+Extrema.i0 [variable, in mathcomp.ssreflect.fintype]
+Extrema.P [variable, in mathcomp.ssreflect.fintype]
+Extrema.Pi0 [variable, in mathcomp.ssreflect.fintype]
+ExtremumSpec [constructor, in mathcomp.ssreflect.fintype]
+extremum_spec [inductive, in mathcomp.ssreflect.fintype]
+ExtSdprodm [section, in mathcomp.fingroup.gproduct]
+ExtSdprodm.actf [variable, in mathcomp.fingroup.gproduct]
+ExtSdprodm.aT [variable, in mathcomp.fingroup.gproduct]
+ExtSdprodm.DgH [variable, in mathcomp.fingroup.gproduct]
+ExtSdprodm.DgK [variable, in mathcomp.fingroup.gproduct]
+ExtSdprodm.fH [variable, in mathcomp.fingroup.gproduct]
+ExtSdprodm.fK [variable, in mathcomp.fingroup.gproduct]
+ExtSdprodm.gT [variable, in mathcomp.fingroup.gproduct]
+ExtSdprodm.H [variable, in mathcomp.fingroup.gproduct]
+ExtSdprodm.K [variable, in mathcomp.fingroup.gproduct]
+ExtSdprodm.rT [variable, in mathcomp.fingroup.gproduct]
+ExtSdprodm.to [variable, in mathcomp.fingroup.gproduct]
+ext_coprime_quotient_cent [lemma, in mathcomp.solvable.hall]
+ext_coprime_Hall_subset [lemma, in mathcomp.solvable.hall]
+ext_norm_conj_cent [lemma, in mathcomp.solvable.hall]
+ext_coprime_Hall_trans [lemma, in mathcomp.solvable.hall]
+ext_coprime_Hall_exists [lemma, in mathcomp.solvable.hall]
+ex_maxnormal_ntrivg [lemma, in mathcomp.solvable.gseries]
+ex_maxnP [lemma, in mathcomp.ssreflect.ssrnat]
+ex_maxn_spec [inductive, in mathcomp.ssreflect.ssrnat]
+ex_maxn [definition, in mathcomp.ssreflect.ssrnat]
+ex_maxn_subproof [lemma, in mathcomp.ssreflect.ssrnat]
+ex_minnP [lemma, in mathcomp.ssreflect.ssrnat]
+ex_minn_spec [inductive, in mathcomp.ssreflect.ssrnat]
+ex_minn [definition, in mathcomp.ssreflect.ssrnat]
+ex_elim_qf [lemma, in mathcomp.field.closed_field]
+ex_elim [definition, in mathcomp.field.closed_field]
+ex_elim_seq_qf [lemma, in mathcomp.field.closed_field]
+ex_elim_seqP [lemma, in mathcomp.field.closed_field]
+ex_elim_seq [definition, in mathcomp.field.closed_field]
+ex_mingroup [lemma, in mathcomp.fingroup.fingroup]
+ex_maxgroup [lemma, in mathcomp.fingroup.fingroup]
+ex_maxset [lemma, in mathcomp.ssreflect.finset]
+ex_minset [lemma, in mathcomp.ssreflect.finset]
+E_G [abbreviation, in mathcomp.character.mxrepresentation]
+E_ [abbreviation, in mathcomp.character.mxrepresentation]
+E_G [abbreviation, in mathcomp.character.mxrepresentation]
+E_G [abbreviation, in mathcomp.character.mxrepresentation]
+e' [abbreviation, in mathcomp.ssreflect.generic_quotient]
+e'E [abbreviation, in mathcomp.ssreflect.generic_quotient]
+e0 [abbreviation, in mathcomp.character.mxrepresentation]
+
| 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) | +