| 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) | -
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]
-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]
-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]
-EqAllPairsDep [section, in mathcomp.ssreflect.seq]
-EqAllPairsDep.R [variable, in mathcomp.ssreflect.seq]
-EqAllPairsDep.S [variable, in mathcomp.ssreflect.seq]
-EqAllPairsDep.T [variable, in mathcomp.ssreflect.seq]
-EqAllPairs.R [variable, 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]
-eqitv [definition, in mathcomp.algebra.interval]
-eqitvP [lemma, in mathcomp.algebra.interval]
-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]
-eqMixin [lemma, in mathcomp.ssreflect.finfun]
-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]
-eqmxMunitP [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_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.Filters.a [variable, in mathcomp.ssreflect.seq]
-EqSeq.Filters.aP [variable, in mathcomp.ssreflect.seq]
-EqSeq.Filters.s [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]
-'all_ _ [notation, in mathcomp.ssreflect.seq]
-'has_ _ [notation, 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 [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_itv_boundP [lemma, in mathcomp.algebra.interval]
-eq_itv_bound [definition, in mathcomp.algebra.interval]
-eq_mktuple [lemma, in mathcomp.ssreflect.tuple]
-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_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_in_allpairs [lemma, in mathcomp.ssreflect.seq]
-eq_in_allpairs_dep [lemma, in mathcomp.ssreflect.seq]
-eq_allpairs [lemma, in mathcomp.ssreflect.seq]
-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_uniq [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_poly [lemma, in mathcomp.algebra.poly]
-eq_prim_root_expr [lemma, in mathcomp.algebra.poly]
-eq_big_perm [abbreviation, in mathcomp.ssreflect.bigop]
-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_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_ffun [lemma, in mathcomp.ssreflect.finfun]
-eq_dffun [lemma, in mathcomp.ssreflect.finfun]
-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]
-eq_finset [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]
-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_inPP [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.ArgMinMax [section, in mathcomp.ssreflect.fintype]
-Extrema.ArgMinMax.F [variable, in mathcomp.ssreflect.fintype]
-Extrema.ArgMinMax.I [variable, in mathcomp.ssreflect.fintype]
-Extrema.ArgMinMax.i0 [variable, in mathcomp.ssreflect.fintype]
-Extrema.ArgMinMax.P [variable, in mathcomp.ssreflect.fintype]
-Extrema.ArgMinMax.Pi0 [variable, in mathcomp.ssreflect.fintype]
-Extrema.arg_pred [variable, in mathcomp.ssreflect.fintype]
-Extrema.Extremum [section, in mathcomp.ssreflect.fintype]
-Extrema.Extremum.ord_total [variable, in mathcomp.ssreflect.fintype]
-Extrema.Extremum.ord_trans [variable, in mathcomp.ssreflect.fintype]
-Extrema.Extremum.ord_refl [variable, in mathcomp.ssreflect.fintype]
-Extrema.Extremum.Pi0 [variable, in mathcomp.ssreflect.fintype]
-[ arg[ _ ]_( _ < _ ) _ ] (form_scope) [notation, in mathcomp.ssreflect.fintype]
-[ arg[ _ ]_( _ < _ in _ ) _ ] (form_scope) [notation, in mathcomp.ssreflect.fintype]
-[ arg[ _ ]_( _ < _ | _ ) _ ] (form_scope) [notation, in mathcomp.ssreflect.fintype]
-extremum [definition, in mathcomp.ssreflect.fintype]
-extremumP [lemma, 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_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 | -(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) | -