| 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 | (80254 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 | (1852 entries) |
| Binder Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (48996 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 | (383 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 | (4219 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 | (93 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 | (14738 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 | (223 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 | (132 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 | (452 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 | (1431 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 | (1169 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 | (6273 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 | (248 entries) |
E
e [abbreviation, in mathcomp.algebra.matrix]eC [abbreviation, in mathcomp.ssreflect.generic_quotient]
ecubes [definition, in mathcomp.solvable.burnside_app]
ecubes_def [lemma, in mathcomp.solvable.burnside_app]
ec:111 [binder, in mathcomp.ssreflect.generic_quotient]
ec:131 [binder, in mathcomp.ssreflect.generic_quotient]
ED [abbreviation, in mathcomp.solvable.extremal]
edivn [definition, in mathcomp.ssreflect.div]
edivnB [lemma, in mathcomp.ssreflect.div]
edivnD [lemma, in mathcomp.ssreflect.div]
edivnP [lemma, in mathcomp.ssreflect.div]
edivnS [lemma, in mathcomp.ssreflect.div]
EdivnSpec [constructor, in mathcomp.ssreflect.div]
edivn_pred [lemma, 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]
eigenpoly [definition, in mathcomp.algebra.mxpoly]
eigenpolyP [lemma, in mathcomp.algebra.mxpoly]
eigenpoly_conjmx [lemma, in mathcomp.algebra.mxpoly]
eigenpoly_map [lemma, in mathcomp.algebra.mxpoly]
eigenspace [definition, in mathcomp.algebra.mxalgebra]
eigenspaceP [lemma, in mathcomp.algebra.mxalgebra]
eigenspace_sub_geigen [lemma, in mathcomp.algebra.mxpoly]
eigenspace_poly [lemma, in mathcomp.algebra.mxpoly]
eigenvalue [definition, in mathcomp.algebra.mxalgebra]
eigenvalueP [lemma, in mathcomp.algebra.mxalgebra]
eigenvalue_conjmx [lemma, in mathcomp.algebra.mxpoly]
eigenvalue_poly [lemma, in mathcomp.algebra.mxpoly]
eigenvalue_root_min [lemma, in mathcomp.algebra.mxpoly]
eigenvalue_root_char [lemma, in mathcomp.algebra.mxpoly]
eigenvalue_map [lemma, in mathcomp.algebra.mxalgebra]
eigenvectorP [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_morphism [definition, 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]
encModRel_class_of [inductive, in mathcomp.ssreflect.generic_quotient]
encoded_equivP [lemma, in mathcomp.ssreflect.generic_quotient]
encoded_equiv_equiv_rel [definition, 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]
enumT [lemma, in mathcomp.ssreflect.fintype]
enum_tuple [definition, in mathcomp.ssreflect.tuple]
enum_tupleP [lemma, in mathcomp.ssreflect.tuple]
enum_set1 [lemma, in mathcomp.ssreflect.finset]
enum_setT [lemma, in mathcomp.ssreflect.finset]
enum_set0 [lemma, in mathcomp.ssreflect.finset]
enum_AEnd [lemma, in mathcomp.field.galois]
enum_extremal_groups [definition, in mathcomp.solvable.extremal]
enum_ordSr [lemma, in mathcomp.ssreflect.fintype]
enum_ordSl [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_rank_in_inj [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_ord0 [lemma, in mathcomp.ssreflect.fintype]
enum_uniq [lemma, in mathcomp.ssreflect.fintype]
enum_mem [definition, in mathcomp.ssreflect.fintype]
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]
env:88 [binder, in mathcomp.ssreflect.ssrAC]
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]
eqbLHS [abbreviation, in mathcomp.ssreflect.eqtype]
eqbLR [lemma, in mathcomp.ssreflect.ssrbool]
eqbP [lemma, in mathcomp.ssreflect.eqtype]
eqbRHS [abbreviation, in mathcomp.ssreflect.eqtype]
eqbRL [lemma, in mathcomp.ssreflect.ssrbool]
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]
eqEtuple [lemma, in mathcomp.ssreflect.tuple]
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_col [lemma, in mathcomp.algebra.mxalgebra]
eqmx_stable [lemma, in mathcomp.algebra.mxalgebra]
eqmx_sums [lemma, in mathcomp.algebra.mxalgebra]
eqmx_rowsub [lemma, in mathcomp.algebra.mxalgebra]
eqmx_rowsub_comp [lemma, in mathcomp.algebra.mxalgebra]
eqmx_rowsub_comp_perm [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]
EqNotNeq [constructor, in mathcomp.ssreflect.eqtype]
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_sub2lE [lemma, in mathcomp.ssreflect.ssrnat]
eqn_sub2rE [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]
eqn_from_log [lemma, in mathcomp.ssreflect.prime]
eqn0Ngt [lemma, in mathcomp.ssreflect.ssrnat]
eqn0_xor_gt0 [inductive, in mathcomp.ssreflect.ssrnat]
eqP [lemma, in mathcomp.ssreflect.eqtype]
EqPairwise [section, in mathcomp.ssreflect.seq]
EqPairwise.r [variable, in mathcomp.ssreflect.seq]
EqPairwise.T [variable, in mathcomp.ssreflect.seq]
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]
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]
eqp_take_drop [lemma, in mathcomp.algebra.poly]
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]
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]
eqQuotType_quotType [definition, in mathcomp.ssreflect.generic_quotient]
eqQuotType_eqType [definition, in mathcomp.ssreflect.generic_quotient]
eqrXz2 [lemma, in mathcomp.algebra.ssrint]
eqr_expz2 [abbreviation, 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_all [lemma, in mathcomp.ssreflect.seq]
eqseq_pivotr [lemma, in mathcomp.ssreflect.seq]
eqseq_pivotl [lemma, in mathcomp.ssreflect.seq]
eqseq_pivot2r [lemma, in mathcomp.ssreflect.seq]
eqseq_pivot2l [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]
EqSorted [section, in mathcomp.ssreflect.path]
EqSorted_in.leT [variable, in mathcomp.ssreflect.path]
EqSorted_in.T [variable, in mathcomp.ssreflect.path]
EqSorted_in [section, in mathcomp.ssreflect.path]
EqSorted.leT [variable, in mathcomp.ssreflect.path]
EqSorted.leT_refl [variable, in mathcomp.ssreflect.path]
EqSorted.leT_tr [variable, in mathcomp.ssreflect.path]
EqSorted.T [variable, in mathcomp.ssreflect.path]
EqSortSeq [section, in mathcomp.ssreflect.path]
EqSortSeq.leT [variable, in mathcomp.ssreflect.path]
EqSortSeq.T [variable, in mathcomp.ssreflect.path]
eqSS [lemma, in mathcomp.ssreflect.ssrnat]
EqSupport [section, in mathcomp.ssreflect.bigop]
EqSupport.ComoidSupport [section, in mathcomp.ssreflect.bigop]
EqSupport.ComoidSupport.I [variable, in mathcomp.ssreflect.bigop]
EqSupport.ComoidSupport.op [variable, in mathcomp.ssreflect.bigop]
EqSupport.idx [variable, in mathcomp.ssreflect.bigop]
EqSupport.MonoidSupport [section, in mathcomp.ssreflect.bigop]
EqSupport.MonoidSupport.I [variable, in mathcomp.ssreflect.bigop]
EqSupport.MonoidSupport.op [variable, in mathcomp.ssreflect.bigop]
EqSupport.R [variable, in mathcomp.ssreflect.bigop]
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]
eqTleqif [lemma, in mathcomp.ssreflect.ssrnat]
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]
eqT:123 [binder, in mathcomp.ssreflect.generic_quotient]
eqT:125 [binder, in mathcomp.ssreflect.generic_quotient]
eqT:126 [binder, in mathcomp.ssreflect.generic_quotient]
eqT:134 [binder, in mathcomp.ssreflect.generic_quotient]
eqT:136 [binder, in mathcomp.ssreflect.generic_quotient]
eqT:141 [binder, in mathcomp.ssreflect.generic_quotient]
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_of [record, in mathcomp.ssreflect.eqtype]
Equality.op [projection, in mathcomp.ssreflect.eqtype]
Equality.sort [projection, in mathcomp.ssreflect.eqtype]
Equality.type [record, in mathcomp.ssreflect.eqtype]
equal_to_pi [definition, 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.choiceType [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.encD_equiv_rel [definition, 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.eqQuotType [definition, in mathcomp.ssreflect.generic_quotient]
EquivQuot.eqType [definition, 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.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.quotType [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]
EquivRel.e [variable, in mathcomp.ssreflect.generic_quotient]
EquivRel.T [variable, in mathcomp.ssreflect.generic_quotient]
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]
equiv_subfext_encModRel [definition, in mathcomp.field.fieldext]
equiv_subfext_equiv [definition, in mathcomp.field.fieldext]
equiv_subfext_is_equiv [lemma, in mathcomp.field.fieldext]
equiv_subfext [definition, in mathcomp.field.fieldext]
equiv:168 [binder, in mathcomp.ssreflect.generic_quotient]
eqU:1130 [binder, in mathcomp.character.mxrepresentation]
eqVneq [lemma, in mathcomp.ssreflect.eqtype]
eqVproper [lemma, in mathcomp.ssreflect.finset]
eqV:1131 [binder, in mathcomp.character.mxrepresentation]
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_m_n:326 [binder, in mathcomp.fingroup.perm]
eq_m_n:323 [binder, in mathcomp.fingroup.perm]
eq_m_n:316 [binder, in mathcomp.fingroup.perm]
eq_m_n:313 [binder, in mathcomp.fingroup.perm]
eq_m_n:308 [binder, in mathcomp.fingroup.perm]
eq_m_n:305 [binder, in mathcomp.fingroup.perm]
eq_m_n:302 [binder, in mathcomp.fingroup.perm]
eq_n_p:298 [binder, in mathcomp.fingroup.perm]
eq_m_n:297 [binder, in mathcomp.fingroup.perm]
eq_m_n:291 [binder, in mathcomp.fingroup.perm]
eq_m_n:286 [binder, in mathcomp.fingroup.perm]
eq_n:282 [binder, in mathcomp.fingroup.perm]
eq_mn:277 [binder, in mathcomp.fingroup.perm]
eq_porbit_mem [lemma, in mathcomp.fingroup.perm]
eq_quot_countType [definition, in mathcomp.ssreflect.generic_quotient]
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_mn:286 [binder, in mathcomp.ssreflect.tuple]
eq_mn:279 [binder, in mathcomp.ssreflect.tuple]
eq_np:275 [binder, in mathcomp.ssreflect.tuple]
eq_mn:274 [binder, in mathcomp.ssreflect.tuple]
eq_mn:270 [binder, in mathcomp.ssreflect.tuple]
eq_mn:267 [binder, in mathcomp.ssreflect.tuple]
eq_nn:263 [binder, in mathcomp.ssreflect.tuple]
eq_mn:254 [binder, in mathcomp.ssreflect.tuple]
eq_mktuple [lemma, in mathcomp.ssreflect.tuple]
eq_mn:58 [binder, in mathcomp.ssreflect.tuple]
eq_np:52 [binder, in mathcomp.ssreflect.tuple]
eq_mn:51 [binder, in mathcomp.ssreflect.tuple]
eq_mn:47 [binder, in mathcomp.ssreflect.tuple]
eq_mn:44 [binder, in mathcomp.ssreflect.tuple]
eq_nn:40 [binder, in mathcomp.ssreflect.tuple]
eq_mn:36 [binder, in mathcomp.ssreflect.tuple]
eq_mn:30 [binder, in mathcomp.ssreflect.tuple]
eq_from_tnth [lemma, in mathcomp.ssreflect.tuple]
eq_pairwise [lemma, in mathcomp.ssreflect.seq]
eq_in_pairwise [lemma, in mathcomp.ssreflect.seq]
eq_allrel_mem2 [lemma, in mathcomp.ssreflect.seq]
eq_allrel_memr [lemma, in mathcomp.ssreflect.seq]
eq_allrel_meml [lemma, in mathcomp.ssreflect.seq]
eq_allrel [lemma, in mathcomp.ssreflect.seq]
eq_in_allrel [lemma, in mathcomp.ssreflect.seq]
eq_in_allpairs [lemma, in mathcomp.ssreflect.seq]
eq_in_allpairs_dep [lemma, in mathcomp.ssreflect.seq]
eq_allpairsr [lemma, in mathcomp.ssreflect.seq]
eq_allpairs [lemma, in mathcomp.ssreflect.seq]
eq_from_flatten_shape [lemma, in mathcomp.ssreflect.seq]
eq_map_all [lemma, in mathcomp.ssreflect.seq]
eq_mkseq [lemma, in mathcomp.ssreflect.seq]
eq_pmap [lemma, in mathcomp.ssreflect.seq]
eq_in_pmap [lemma, in mathcomp.ssreflect.seq]
eq_in_map [lemma, in mathcomp.ssreflect.seq]
eq_map [lemma, in mathcomp.ssreflect.seq]
eq_mem_map [lemma, in mathcomp.ssreflect.seq]
eq_count_undup [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_pq:488 [binder, in mathcomp.algebra.polydiv]
eq_choose [lemma, in mathcomp.ssreflect.choice]
eq_xchoose [lemma, in mathcomp.ssreflect.choice]
eq_binP [lemma, in mathcomp.ssreflect.ssrnat]
eq_leqif [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_ffun [lemma, in mathcomp.ssreflect.finfun]
eq_dffun [lemma, in mathcomp.ssreflect.finfun]
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]
eq_galP [lemma, in mathcomp.field.galois]
eq_adjoin_separable_generator [lemma, in mathcomp.field.separable]
eq_mxdiag [lemma, in mathcomp.algebra.matrix]
eq_mxdiagP [lemma, in mathcomp.algebra.matrix]
eq_mxcol [lemma, in mathcomp.algebra.matrix]
eq_mxcolP [lemma, in mathcomp.algebra.matrix]
eq_mxrow [lemma, in mathcomp.algebra.matrix]
eq_mxrowP [lemma, in mathcomp.algebra.matrix]
eq_mxblock [lemma, in mathcomp.algebra.matrix]
eq_mxblockP [lemma, in mathcomp.algebra.matrix]
eq_map2_mx [lemma, in mathcomp.algebra.matrix]
eq_in_map2_mx [lemma, in mathcomp.algebra.matrix]
eq_map_mx [lemma, in mathcomp.algebra.matrix]
eq_in_map_mx [lemma, in mathcomp.algebra.matrix]
eq_block_mx [lemma, in mathcomp.algebra.matrix]
eq_n:579 [binder, in mathcomp.algebra.matrix]
eq_m:572 [binder, in mathcomp.algebra.matrix]
eq_col_mx [lemma, in mathcomp.algebra.matrix]
eq_row_mx [lemma, in mathcomp.algebra.matrix]
eq_mn:424 [binder, in mathcomp.algebra.matrix]
eq_n:418 [binder, in mathcomp.algebra.matrix]
eq_m:417 [binder, in mathcomp.algebra.matrix]
eq_n:411 [binder, in mathcomp.algebra.matrix]
eq_m:406 [binder, in mathcomp.algebra.matrix]
eq_mn:291 [binder, in mathcomp.algebra.matrix]
eq_mn:260 [binder, in mathcomp.algebra.matrix]
eq_mn':255 [binder, in mathcomp.algebra.matrix]
eq_mn:254 [binder, in mathcomp.algebra.matrix]
eq_castmx [lemma, in mathcomp.algebra.matrix]
eq_n:247 [binder, in mathcomp.algebra.matrix]
eq_m:246 [binder, in mathcomp.algebra.matrix]
eq_n:241 [binder, in mathcomp.algebra.matrix]
eq_m:240 [binder, in mathcomp.algebra.matrix]
eq_n:235 [binder, in mathcomp.algebra.matrix]
eq_m:234 [binder, in mathcomp.algebra.matrix]
eq_n2:228 [binder, in mathcomp.algebra.matrix]
eq_m2:227 [binder, in mathcomp.algebra.matrix]
eq_n1:226 [binder, in mathcomp.algebra.matrix]
eq_m1:225 [binder, in mathcomp.algebra.matrix]
eq_colsub [lemma, in mathcomp.algebra.matrix]
eq_rowsub [lemma, in mathcomp.algebra.matrix]
eq_mxsub [lemma, in mathcomp.algebra.matrix]
eq_mn:126 [binder, in mathcomp.algebra.matrix]
eq_mn:80 [binder, in mathcomp.algebra.matrix]
eq_mx [lemma, in mathcomp.algebra.matrix]
eq_Aut [lemma, in mathcomp.fingroup.automorphism]
eq_cfclass_IirrE [lemma, in mathcomp.character.inertia]
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_abelem_subg_repr [lemma, in mathcomp.character.mxabelem]
eq_rowg [lemma, in mathcomp.character.mxabelem]
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_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_count_merge [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_in_sorted [lemma, in mathcomp.ssreflect.path]
eq_in_cycle [lemma, in mathcomp.ssreflect.path]
eq_in_path [lemma, in mathcomp.ssreflect.path]
eq_pnat [lemma, in mathcomp.ssreflect.prime]
eq_in_pnat [lemma, in mathcomp.ssreflect.prime]
eq_partn_from_log [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_Mod8_D8 [lemma, in mathcomp.solvable.extremal]
eq_abelian_type_isog [lemma, in mathcomp.solvable.abelian]
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_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_order_cycle [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_omap [lemma, in mathcomp.ssreflect.ssrfun]
eq_limg_ker0 [lemma, in mathcomp.algebra.vector]
eq_in_limg [lemma, in mathcomp.algebra.vector]
eq_span [lemma, in mathcomp.algebra.vector]
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_homGrp [lemma, in mathcomp.fingroup.presentation]
eq_card_prod [lemma, in mathcomp.ssreflect.fintype]
eq_shift [definition, in mathcomp.ssreflect.fintype]
eq_rlshift [lemma, in mathcomp.ssreflect.fintype]
eq_lrshift [lemma, in mathcomp.ssreflect.fintype]
eq_rshift [lemma, in mathcomp.ssreflect.fintype]
eq_lshift [lemma, in mathcomp.ssreflect.fintype]
eq_liftF [lemma, in mathcomp.ssreflect.fintype]
eq_enum_rank_in [lemma, in mathcomp.ssreflect.fintype]
eq_n:894 [binder, in mathcomp.ssreflect.fintype]
eq_n:891 [binder, in mathcomp.ssreflect.fintype]
eq_n:888 [binder, in mathcomp.ssreflect.fintype]
eq_n3:884 [binder, in mathcomp.ssreflect.fintype]
eq_n2:883 [binder, in mathcomp.ssreflect.fintype]
eq_n:878 [binder, in mathcomp.ssreflect.fintype]
eq_n_m:875 [binder, 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_map_poly [lemma, in mathcomp.algebra.poly]
eq_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_bigl_supp [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_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_xor_neq [inductive, 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_fullrowsub [lemma, in mathcomp.algebra.mxalgebra]
eq_maxrowsub [lemma, in mathcomp.algebra.mxalgebra]
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_row_full [lemma, in mathcomp.algebra.mxalgebra]
Eq0NotPos [constructor, in mathcomp.ssreflect.ssrnat]
erefl_mn:217 [binder, in mathcomp.algebra.matrix]
ErV [abbreviation, in mathcomp.character.mxabelem]
Es:245 [binder, in mathcomp.solvable.maximal]
Es:247 [binder, in mathcomp.solvable.maximal]
EtoK:467 [binder, in mathcomp.field.closed_field]
eT:129 [binder, in mathcomp.ssreflect.generic_quotient]
eT:13 [binder, in mathcomp.ssreflect.fintype]
eT:217 [binder, in mathcomp.fingroup.perm]
eT:752 [binder, in mathcomp.ssreflect.fintype]
Euclid_dvdX [lemma, in mathcomp.ssreflect.prime]
Euclid_dvd_prod [lemma, in mathcomp.ssreflect.prime]
Euclid_dvdM [lemma, in mathcomp.ssreflect.prime]
Euclid_dvd1 [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_uphalfK [lemma, in mathcomp.ssreflect.ssrnat]
even_halfK [lemma, in mathcomp.ssreflect.ssrnat]
even_prime [lemma, in mathcomp.ssreflect.prime]
even_polyMX [lemma, in mathcomp.algebra.poly]
even_polyC [lemma, in mathcomp.algebra.poly]
even_poly_linear [definition, in mathcomp.algebra.poly]
even_poly_additive [definition, in mathcomp.algebra.poly]
even_poly_is_linear [lemma, in mathcomp.algebra.poly]
even_polyZ [lemma, in mathcomp.algebra.poly]
even_polyD [lemma, in mathcomp.algebra.poly]
even_polyE [lemma, in mathcomp.algebra.poly]
even_poly [definition, in mathcomp.algebra.poly]
ev_ax [abbreviation, in mathcomp.ssreflect.eqtype]
ev:2026 [binder, in mathcomp.algebra.ssralg]
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]
exchange_big_nat_idem [lemma, in mathcomp.ssreflect.bigop]
exchange_big_dep_nat_idem [lemma, in mathcomp.ssreflect.bigop]
exchange_big_idem [lemma, in mathcomp.ssreflect.bigop]
exchange_big_dep_idem [lemma, in mathcomp.ssreflect.bigop]
existsb [lemma, in mathcomp.ssreflect.fintype]
existsb_tnth [lemma, in mathcomp.ssreflect.tuple]
existsP [lemma, in mathcomp.ssreflect.fintype]
existsPn [lemma, in mathcomp.ssreflect.fintype]
existsPP [lemma, in mathcomp.ssreflect.fintype]
exists_cons [lemma, in mathcomp.ssreflect.seq]
exists_acomps [lemma, in mathcomp.solvable.jordanholder]
exists_comps [lemma, in mathcomp.solvable.jordanholder]
exists_inPn [lemma, in mathcomp.ssreflect.fintype]
exists_eq_inP [lemma, in mathcomp.ssreflect.fintype]
exists_inPP [lemma, in mathcomp.ssreflect.fintype]
exists_inb [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_mod_order [lemma, in mathcomp.fingroup.fingroup]
expg_mod [lemma, in mathcomp.fingroup.fingroup]
expg_order [lemma, in mathcomp.fingroup.fingroup]
expg_exponent [lemma, in mathcomp.solvable.abelian]
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_mx_group [lemma, in mathcomp.character.mxabelem]
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_pX1p2n [lemma, in mathcomp.solvable.extraspecial]
exponent_pX1p2 [lemma, in mathcomp.solvable.extraspecial]
exponent_Ohm1_class2 [lemma, in mathcomp.solvable.maximal]
exponent_2extraspecial [lemma, in mathcomp.solvable.maximal]
exponent_special [lemma, in mathcomp.solvable.maximal]
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_pmulzl [abbreviation, 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_pMzl [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_finIndexType [definition, in mathcomp.ssreflect.finfun]
exp_block_diag_mx [lemma, in mathcomp.algebra.matrix]
exp_cforder [lemma, in mathcomp.character.classfun]
exp_cfunE [lemma, in mathcomp.character.classfun]
exp_orderC [lemma, in mathcomp.field.algnum]
exp_vectType [definition, in mathcomp.algebra.vector]
exp_prim_root [lemma, in mathcomp.algebra.poly]
exp0n [lemma, in mathcomp.ssreflect.ssrnat]
exp0rz [lemma, in mathcomp.algebra.ssrint]
exp1n [lemma, in mathcomp.ssreflect.ssrnat]
exp1rz [lemma, in mathcomp.algebra.ssrint]
exP:101 [binder, in mathcomp.ssreflect.choice]
exP:104 [binder, in mathcomp.ssreflect.choice]
exP:472 [binder, in mathcomp.ssreflect.ssrnat]
exP:478 [binder, in mathcomp.ssreflect.ssrnat]
exP:95 [binder, in mathcomp.ssreflect.choice]
exP:99 [binder, in mathcomp.ssreflect.choice]
exQ:105 [binder, in mathcomp.ssreflect.choice]
exQ:473 [binder, in mathcomp.ssreflect.ssrnat]
exQ:480 [binder, in mathcomp.ssreflect.ssrnat]
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_number [definition, in mathcomp.ssreflect.ssrnat]
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_cfConjC_subset [lemma, in mathcomp.character.classfun]
extend_group_splitting_field [lemma, in mathcomp.character.mxrepresentation]
extend_algC_subfield_aut [lemma, in mathcomp.field.algnum]
extend_cyclic_Mho [lemma, in mathcomp.solvable.abelian]
extend:204 [binder, in mathcomp.ssreflect.tuple]
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_baseFinGroupType [definition, in mathcomp.fingroup.gproduct]
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.character.mxabelem]
Extraspecial [section, in mathcomp.solvable.maximal]
extraspecial [definition, in mathcomp.solvable.maximal]
extraspecial [library]
extraspecial_repr_structure [lemma, in mathcomp.character.mxabelem]
extraspecial_structure [lemma, in mathcomp.solvable.maximal]
extraspecial_nonabelian [lemma, in mathcomp.solvable.maximal]
extraspecial_prime [lemma, in mathcomp.solvable.maximal]
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.character.mxabelem]
Extraspecial.gT [variable, in mathcomp.solvable.maximal]
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.character.mxabelem]
Extraspecial.p [variable, in mathcomp.solvable.maximal]
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_finType [definition, in mathcomp.solvable.extremal]
extremal_group_finMixin [definition, in mathcomp.solvable.extremal]
extremal_group_countType [definition, in mathcomp.solvable.extremal]
extremal_group_countMixin [definition, in mathcomp.solvable.extremal]
extremal_group_choiceType [definition, in mathcomp.solvable.extremal]
extremal_group_choiceMixin [definition, in mathcomp.solvable.extremal]
extremal_group_eqType [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.ExtremumIn [section, in mathcomp.ssreflect.fintype]
Extrema.ExtremumIn.ord_total [variable, in mathcomp.ssreflect.fintype]
Extrema.ExtremumIn.ord_trans [variable, in mathcomp.ssreflect.fintype]
Extrema.ExtremumIn.ord_refl [variable, in mathcomp.ssreflect.fintype]
Extrema.ExtremumIn.Pi0 [variable, 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[ _ ]_( _ < _ ) _ ] (nat_scope) [notation, in mathcomp.ssreflect.fintype]
[ arg[ _ ]_( _ < _ in _ ) _ ] (nat_scope) [notation, in mathcomp.ssreflect.fintype]
[ arg[ _ ]_( _ < _ | _ ) _ ] (nat_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_inP [lemma, 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_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_maxset [lemma, in mathcomp.ssreflect.finset]
ex_minset [lemma, in mathcomp.ssreflect.finset]
ex_mingroup [lemma, in mathcomp.fingroup.fingroup]
ex_maxgroup [lemma, in mathcomp.fingroup.fingroup]
ex_maxnormal_ntrivg [lemma, in mathcomp.solvable.gseries]
ex_i_bc:2336 [binder, in mathcomp.algebra.ssralg]
E_N:656 [binder, in mathcomp.field.galois]
E_F:243 [binder, in mathcomp.field.fieldext]
e_mn:280 [binder, in mathcomp.algebra.matrix]
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]
E':11 [binder, in mathcomp.ssreflect.ssrnat]
e':1890 [binder, in mathcomp.algebra.ssralg]
e':1892 [binder, in mathcomp.algebra.ssralg]
e':1904 [binder, in mathcomp.algebra.ssralg]
e':1906 [binder, in mathcomp.algebra.ssralg]
e':2048 [binder, in mathcomp.algebra.ssralg]
e':2049 [binder, in mathcomp.algebra.ssralg]
e':2052 [binder, in mathcomp.algebra.ssralg]
e':73 [binder, in mathcomp.ssreflect.ssrAC]
e':76 [binder, in mathcomp.ssreflect.fingraph]
e':78 [binder, in mathcomp.ssreflect.fingraph]
e':80 [binder, in mathcomp.ssreflect.fingraph]
e':82 [binder, in mathcomp.ssreflect.fingraph]
e':89 [binder, in mathcomp.ssreflect.fingraph]
e':91 [binder, in mathcomp.ssreflect.fingraph]
e0 [abbreviation, in mathcomp.character.mxrepresentation]
e0W:638 [binder, in mathcomp.character.mxrepresentation]
E0:317 [binder, in mathcomp.field.fieldext]
E1:1007 [binder, in mathcomp.algebra.ssrnum]
e1:124 [binder, in mathcomp.ssreflect.eqtype]
E1:1450 [binder, in mathcomp.algebra.ssrnum]
E1:1489 [binder, in mathcomp.algebra.ssrnum]
e1:1760 [binder, in mathcomp.algebra.mxalgebra]
E1:1885 [binder, in mathcomp.algebra.mxalgebra]
E1:256 [binder, in mathcomp.field.separable]
E1:3052 [binder, in mathcomp.ssreflect.bigop]
E1:3067 [binder, in mathcomp.ssreflect.bigop]
E1:3079 [binder, in mathcomp.ssreflect.bigop]
E1:3173 [binder, in mathcomp.ssreflect.bigop]
E1:736 [binder, in mathcomp.algebra.poly]
E1:976 [binder, in mathcomp.algebra.ssrnum]
E1:989 [binder, in mathcomp.algebra.ssrnum]
E2:1008 [binder, in mathcomp.algebra.ssrnum]
e2:125 [binder, in mathcomp.ssreflect.eqtype]
E2:1451 [binder, in mathcomp.algebra.ssrnum]
E2:1490 [binder, in mathcomp.algebra.ssrnum]
e2:1761 [binder, in mathcomp.algebra.mxalgebra]
E2:1886 [binder, in mathcomp.algebra.mxalgebra]
E2:255 [binder, in mathcomp.field.separable]
E2:3053 [binder, in mathcomp.ssreflect.bigop]
E2:3068 [binder, in mathcomp.ssreflect.bigop]
E2:3080 [binder, in mathcomp.ssreflect.bigop]
E2:3174 [binder, in mathcomp.ssreflect.bigop]
E2:737 [binder, in mathcomp.algebra.poly]
E2:977 [binder, in mathcomp.algebra.ssrnum]
E2:990 [binder, in mathcomp.algebra.ssrnum]
E:10 [binder, in mathcomp.ssreflect.ssrnat]
e:10 [binder, in mathcomp.ssreflect.fintype]
E:100 [binder, in mathcomp.field.fieldext]
E:1013 [binder, in mathcomp.algebra.matrix]
E:102 [binder, in mathcomp.field.fieldext]
e:102 [binder, in mathcomp.ssreflect.fingraph]
e:104 [binder, in mathcomp.ssreflect.generic_quotient]
E:104 [binder, in mathcomp.field.fieldext]
E:104 [binder, in mathcomp.field.separable]
E:1047 [binder, in mathcomp.algebra.ssralg]
E:106 [binder, in mathcomp.field.galois]
E:106 [binder, in mathcomp.field.fieldext]
e:107 [binder, in mathcomp.field.closed_field]
e:11 [binder, in mathcomp.ssreflect.fintype]
E:112 [binder, in mathcomp.field.separable]
E:113 [binder, in mathcomp.field.galois]
E:116 [binder, in mathcomp.field.galois]
e:116 [binder, in mathcomp.field.closed_field]
E:117 [binder, in mathcomp.field.fieldext]
e:120 [binder, in mathcomp.field.algC]
e:120 [binder, in mathcomp.field.closed_field]
E:121 [binder, in mathcomp.field.galois]
E:121 [binder, in mathcomp.field.fieldext]
e:1215 [binder, in mathcomp.ssreflect.ssrnat]
e:122 [binder, in mathcomp.ssreflect.prime]
E:124 [binder, in mathcomp.character.mxabelem]
E:1246 [binder, in mathcomp.character.mxrepresentation]
E:125 [binder, in mathcomp.field.fieldext]
e:125 [binder, in mathcomp.field.separable]
e:127 [binder, in mathcomp.ssreflect.eqtype]
e:128 [binder, in mathcomp.ssreflect.eqtype]
E:13 [binder, in mathcomp.field.galois]
E:130 [binder, in mathcomp.field.galois]
E:134 [binder, in mathcomp.field.galois]
e:1345 [binder, in mathcomp.algebra.ssrnum]
e:1348 [binder, in mathcomp.algebra.ssrnum]
e:1351 [binder, in mathcomp.algebra.ssrnum]
e:1352 [binder, in mathcomp.character.mxrepresentation]
e:1354 [binder, in mathcomp.algebra.ssrnum]
e:1357 [binder, in mathcomp.algebra.ssrnum]
e:1360 [binder, in mathcomp.algebra.ssrnum]
e:1363 [binder, in mathcomp.algebra.ssrnum]
e:1366 [binder, in mathcomp.algebra.ssrnum]
e:1369 [binder, in mathcomp.algebra.ssrnum]
e:1372 [binder, in mathcomp.algebra.ssrnum]
E:138 [binder, in mathcomp.field.galois]
E:141 [binder, in mathcomp.field.separable]
e:142 [binder, in mathcomp.field.falgebra]
E:1433 [binder, in mathcomp.ssreflect.finset]
E:1445 [binder, in mathcomp.ssreflect.finset]
e:145 [binder, in mathcomp.field.finfield]
E:1458 [binder, in mathcomp.ssreflect.finset]
e:146 [binder, in mathcomp.field.finfield]
e:146 [binder, in mathcomp.field.falgebra]
E:1465 [binder, in mathcomp.ssreflect.finset]
E:1465 [binder, in mathcomp.algebra.ssrnum]
E:147 [binder, in mathcomp.field.finfield]
e:147 [binder, in mathcomp.algebra.finalg]
E:1474 [binder, in mathcomp.ssreflect.finset]
E:1482 [binder, in mathcomp.ssreflect.finset]
E:1489 [binder, in mathcomp.ssreflect.finset]
E:1493 [binder, in mathcomp.algebra.ssrnum]
e:15 [binder, in mathcomp.ssreflect.prime]
E:15 [binder, in mathcomp.solvable.abelian]
e:151 [binder, in mathcomp.field.closed_field]
e:155 [binder, in mathcomp.field.falgebra]
e:156 [binder, in mathcomp.ssreflect.binomial]
e:159 [binder, in mathcomp.field.closed_field]
E:159 [binder, in mathcomp.solvable.abelian]
e:1591 [binder, in mathcomp.algebra.ssrnum]
e:1593 [binder, in mathcomp.character.mxrepresentation]
e:1597 [binder, in mathcomp.character.mxrepresentation]
E:1598 [binder, in mathcomp.algebra.ssrnum]
e:1605 [binder, in mathcomp.character.mxrepresentation]
e:1606 [binder, in mathcomp.character.mxrepresentation]
e:1608 [binder, in mathcomp.character.mxrepresentation]
e:1611 [binder, in mathcomp.character.mxrepresentation]
e:1616 [binder, in mathcomp.character.mxrepresentation]
e:1618 [binder, in mathcomp.character.mxrepresentation]
e:166 [binder, in mathcomp.ssreflect.generic_quotient]
e:167 [binder, in mathcomp.ssreflect.generic_quotient]
e:168 [binder, in mathcomp.field.falgebra]
E:169 [binder, in mathcomp.solvable.abelian]
e:169 [binder, in mathcomp.field.falgebra]
e:17 [binder, in mathcomp.field.closed_field]
E:171 [binder, in mathcomp.field.fieldext]
e:1716 [binder, in mathcomp.algebra.mxalgebra]
e:1728 [binder, in mathcomp.algebra.mxalgebra]
E:173 [binder, in mathcomp.solvable.abelian]
e:1768 [binder, in mathcomp.algebra.matrix]
E:177 [binder, in mathcomp.solvable.abelian]
E:181 [binder, in mathcomp.solvable.abelian]
e:184 [binder, in mathcomp.field.closed_field]
e:187 [binder, in mathcomp.field.closed_field]
E:187 [binder, in mathcomp.solvable.abelian]
E:1881 [binder, in mathcomp.algebra.mxalgebra]
e:1885 [binder, in mathcomp.algebra.ssralg]
e:1886 [binder, in mathcomp.algebra.ssrnum]
e:1889 [binder, in mathcomp.algebra.ssrnum]
e:1889 [binder, in mathcomp.algebra.ssralg]
E:1889 [binder, in mathcomp.algebra.mxalgebra]
e:1891 [binder, in mathcomp.algebra.ssralg]
E:1892 [binder, in mathcomp.algebra.mxalgebra]
e:1894 [binder, in mathcomp.algebra.ssralg]
e:1897 [binder, in mathcomp.algebra.ssralg]
e:19 [binder, in mathcomp.field.closed_field]
E:19 [binder, in mathcomp.solvable.abelian]
E:1902 [binder, in mathcomp.algebra.ssrnum]
e:1903 [binder, in mathcomp.algebra.ssralg]
e:1905 [binder, in mathcomp.algebra.ssralg]
E:191 [binder, in mathcomp.solvable.abelian]
e:1912 [binder, in mathcomp.algebra.ssralg]
E:192 [binder, in mathcomp.solvable.abelian]
E:193 [binder, in mathcomp.solvable.abelian]
e:1946 [binder, in mathcomp.algebra.ssralg]
e:1975 [binder, in mathcomp.algebra.ssralg]
e:1979 [binder, in mathcomp.algebra.ssralg]
e:1997 [binder, in mathcomp.algebra.ssralg]
e:2 [binder, in mathcomp.ssreflect.fintype]
e:2 [binder, in mathcomp.ssreflect.eqtype]
E:20 [binder, in mathcomp.solvable.abelian]
e:2000 [binder, in mathcomp.algebra.ssralg]
e:2007 [binder, in mathcomp.algebra.ssralg]
e:2018 [binder, in mathcomp.algebra.ssrnum]
e:202 [binder, in mathcomp.ssreflect.tuple]
e:2021 [binder, in mathcomp.algebra.ssrnum]
e:2024 [binder, in mathcomp.algebra.ssrnum]
e:2025 [binder, in mathcomp.algebra.ssralg]
e:2027 [binder, in mathcomp.algebra.ssrnum]
e:2030 [binder, in mathcomp.algebra.ssrnum]
e:2033 [binder, in mathcomp.algebra.ssrnum]
e:2036 [binder, in mathcomp.algebra.ssrnum]
e:2039 [binder, in mathcomp.algebra.ssrnum]
e:2039 [binder, in mathcomp.algebra.ssralg]
E:204 [binder, in mathcomp.solvable.maximal]
e:2042 [binder, in mathcomp.algebra.ssrnum]
e:2045 [binder, in mathcomp.algebra.ssrnum]
e:2047 [binder, in mathcomp.algebra.ssralg]
e:2048 [binder, in mathcomp.algebra.ssrnum]
e:2051 [binder, in mathcomp.algebra.ssrnum]
e:2051 [binder, in mathcomp.algebra.ssralg]
E:206 [binder, in mathcomp.field.galois]
E:206 [binder, in mathcomp.solvable.abelian]
E:207 [binder, in mathcomp.field.galois]
e:2077 [binder, in mathcomp.algebra.ssrnum]
E:21 [binder, in mathcomp.solvable.abelian]
E:210 [binder, in mathcomp.solvable.abelian]
E:2185 [binder, in mathcomp.algebra.ssralg]
e:219 [binder, in mathcomp.field.closed_field]
E:2195 [binder, in mathcomp.algebra.ssralg]
E:221 [binder, in mathcomp.field.separable]
e:2213 [binder, in mathcomp.algebra.matrix]
e:2216 [binder, in mathcomp.algebra.matrix]
e:223 [binder, in mathcomp.field.closed_field]
E:224 [binder, in mathcomp.field.separable]
E:226 [binder, in mathcomp.solvable.abelian]
e:227 [binder, in mathcomp.field.algebraics_fundamentals]
e:228 [binder, in mathcomp.field.algebraics_fundamentals]
E:228 [binder, in mathcomp.field.separable]
e:2290 [binder, in mathcomp.algebra.ssralg]
e:2325 [binder, in mathcomp.algebra.ssralg]
e:2328 [binder, in mathcomp.algebra.ssralg]
E:233 [binder, in mathcomp.solvable.abelian]
e:2337 [binder, in mathcomp.algebra.ssralg]
E:235 [binder, in mathcomp.solvable.maximal]
e:2354 [binder, in mathcomp.algebra.ssralg]
e:2356 [binder, in mathcomp.algebra.ssralg]
E:236 [binder, in mathcomp.field.fieldext]
E:236 [binder, in mathcomp.solvable.abelian]
e:2363 [binder, in mathcomp.algebra.ssralg]
E:237 [binder, in mathcomp.field.fieldext]
E:237 [binder, in mathcomp.solvable.maximal]
E:2375 [binder, in mathcomp.algebra.ssrnum]
E:238 [binder, in mathcomp.field.fieldext]
E:238 [binder, in mathcomp.field.separable]
E:238 [binder, in mathcomp.solvable.maximal]
E:239 [binder, in mathcomp.field.separable]
e:239 [binder, in mathcomp.field.closed_field]
E:240 [binder, in mathcomp.field.fieldext]
E:241 [binder, in mathcomp.field.separable]
E:241 [binder, in mathcomp.solvable.abelian]
e:242 [binder, in mathcomp.field.closed_field]
E:243 [binder, in mathcomp.field.separable]
E:244 [binder, in mathcomp.field.fieldext]
E:245 [binder, in mathcomp.field.separable]
E:245 [binder, in mathcomp.solvable.abelian]
e:246 [binder, in mathcomp.field.algebraics_fundamentals]
E:246 [binder, in mathcomp.solvable.maximal]
e:247 [binder, in mathcomp.field.algebraics_fundamentals]
E:247 [binder, in mathcomp.field.separable]
E:248 [binder, in mathcomp.solvable.maximal]
E:249 [binder, in mathcomp.solvable.maximal]
e:25 [binder, in mathcomp.fingroup.presentation]
E:25 [binder, in mathcomp.algebra.qpoly]
E:250 [binder, in mathcomp.solvable.maximal]
e:251 [binder, in mathcomp.field.closed_field]
E:252 [binder, in mathcomp.field.separable]
e:2520 [binder, in mathcomp.algebra.ssralg]
e:253 [binder, in mathcomp.field.closed_field]
E:255 [binder, in mathcomp.field.galois]
E:259 [binder, in mathcomp.field.separable]
E:259 [binder, in mathcomp.solvable.abelian]
E:262 [binder, in mathcomp.field.separable]
e:264 [binder, in mathcomp.algebra.mxpoly]
E:264 [binder, in mathcomp.solvable.abelian]
E:265 [binder, in mathcomp.solvable.abelian]
e:266 [binder, in mathcomp.field.algC]
E:268 [binder, in mathcomp.field.galois]
e:268 [binder, in mathcomp.field.algC]
E:268 [binder, in mathcomp.field.separable]
E:268 [binder, in mathcomp.solvable.abelian]
e:269 [binder, in mathcomp.field.algC]
e:269 [binder, in mathcomp.field.closed_field]
E:270 [binder, in mathcomp.field.galois]
e:271 [binder, in mathcomp.field.algC]
e:272 [binder, in mathcomp.algebra.mxpoly]
E:273 [binder, in mathcomp.field.galois]
e:273 [binder, in mathcomp.algebra.mxpoly]
e:273 [binder, in mathcomp.field.closed_field]
e:274 [binder, in mathcomp.field.algC]
E:274 [binder, in mathcomp.solvable.abelian]
E:275 [binder, in mathcomp.field.galois]
e:277 [binder, in mathcomp.algebra.intdiv]
E:277 [binder, in mathcomp.field.galois]
e:278 [binder, in mathcomp.field.algC]
e:28 [binder, in mathcomp.ssreflect.ssrAC]
e:282 [binder, in mathcomp.field.algC]
e:282 [binder, in mathcomp.field.closed_field]
E:282 [binder, in mathcomp.solvable.abelian]
E:283 [binder, in mathcomp.solvable.abelian]
E:284 [binder, in mathcomp.solvable.abelian]
e:285 [binder, in mathcomp.field.closed_field]
e:286 [binder, in mathcomp.field.algC]
E:288 [binder, in mathcomp.solvable.abelian]
e:289 [binder, in mathcomp.field.algC]
E:29 [binder, in mathcomp.solvable.abelian]
e:291 [binder, in mathcomp.algebra.interval]
e:293 [binder, in mathcomp.field.algC]
E:294 [binder, in mathcomp.solvable.abelian]
e:295 [binder, in mathcomp.algebra.interval]
e:295 [binder, in mathcomp.field.closed_field]
e:296 [binder, in mathcomp.field.algnum]
e:297 [binder, in mathcomp.field.algC]
E:299 [binder, in mathcomp.field.galois]
E:30 [binder, in mathcomp.solvable.abelian]
E:302 [binder, in mathcomp.field.galois]
e:302 [binder, in mathcomp.field.algC]
E:304 [binder, in mathcomp.field.galois]
e:305 [binder, in mathcomp.field.algC]
E:307 [binder, in mathcomp.field.galois]
e:307 [binder, in mathcomp.field.algC]
E:308 [binder, in mathcomp.field.fieldext]
E:309 [binder, in mathcomp.field.galois]
E:309 [binder, in mathcomp.field.fieldext]
e:309 [binder, in mathcomp.field.closed_field]
E:3093 [binder, in mathcomp.ssreflect.bigop]
E:31 [binder, in mathcomp.solvable.abelian]
e:311 [binder, in mathcomp.field.algC]
E:312 [binder, in mathcomp.field.galois]
E:312 [binder, in mathcomp.field.fieldext]
E:314 [binder, in mathcomp.field.galois]
e:315 [binder, in mathcomp.field.algC]
e:317 [binder, in mathcomp.field.algC]
E:317 [binder, in mathcomp.solvable.abelian]
E:318 [binder, in mathcomp.field.galois]
E:318 [binder, in mathcomp.field.fieldext]
E:318 [binder, in mathcomp.solvable.abelian]
e:319 [binder, in mathcomp.field.algC]
E:319 [binder, in mathcomp.field.fieldext]
e:319 [binder, in mathcomp.field.closed_field]
e:319 [binder, in mathcomp.field.algnum]
e:32 [binder, in mathcomp.field.closed_field]
E:32 [binder, in mathcomp.solvable.abelian]
E:320 [binder, in mathcomp.algebra.poly]
e:321 [binder, in mathcomp.field.algnum]
E:322 [binder, in mathcomp.field.galois]
e:322 [binder, in mathcomp.field.algC]
e:322 [binder, in mathcomp.field.algnum]
e:323 [binder, in mathcomp.field.algnum]
e:324 [binder, in mathcomp.field.closed_field]
e:324 [binder, in mathcomp.field.algnum]
E:325 [binder, in mathcomp.field.fieldext]
e:325 [binder, in mathcomp.field.algnum]
e:326 [binder, in mathcomp.field.algnum]
E:327 [binder, in mathcomp.field.galois]
e:327 [binder, in mathcomp.field.algnum]
E:330 [binder, in mathcomp.field.galois]
e:330 [binder, in mathcomp.field.algnum]
e:332 [binder, in mathcomp.field.algnum]
E:333 [binder, in mathcomp.field.galois]
e:334 [binder, in mathcomp.field.closed_field]
e:335 [binder, in mathcomp.field.algnum]
E:336 [binder, in mathcomp.solvable.abelian]
E:338 [binder, in mathcomp.field.galois]
e:339 [binder, in mathcomp.field.closed_field]
e:339 [binder, in mathcomp.field.algnum]
e:34 [binder, in mathcomp.ssreflect.ssrAC]
e:34 [binder, in mathcomp.field.closed_field]
E:342 [binder, in mathcomp.field.galois]
e:343 [binder, in mathcomp.field.algnum]
E:344 [binder, in mathcomp.solvable.abelian]
E:346 [binder, in mathcomp.field.galois]
e:347 [binder, in mathcomp.field.algnum]
e:349 [binder, in mathcomp.field.algnum]
E:35 [binder, in mathcomp.solvable.abelian]
e:352 [binder, in mathcomp.field.algnum]
E:355 [binder, in mathcomp.field.galois]
e:356 [binder, in mathcomp.field.algnum]
E:357 [binder, in mathcomp.field.galois]
E:357 [binder, in mathcomp.solvable.abelian]
E:36 [binder, in mathcomp.solvable.abelian]
e:360 [binder, in mathcomp.field.algnum]
e:361 [binder, in mathcomp.ssreflect.div]
E:361 [binder, in mathcomp.solvable.abelian]
e:365 [binder, in mathcomp.field.algnum]
E:366 [binder, in mathcomp.field.galois]
e:366 [binder, in mathcomp.field.algnum]
E:37 [binder, in mathcomp.solvable.abelian]
E:370 [binder, in mathcomp.field.galois]
e:370 [binder, in mathcomp.field.algnum]
E:371 [binder, in mathcomp.field.closed_field]
E:374 [binder, in mathcomp.field.galois]
e:374 [binder, in mathcomp.field.algnum]
E:376 [binder, in mathcomp.field.galois]
e:376 [binder, in mathcomp.field.algnum]
E:376 [binder, in mathcomp.solvable.abelian]
E:378 [binder, in mathcomp.field.galois]
e:378 [binder, in mathcomp.field.algnum]
E:379 [binder, in mathcomp.solvable.abelian]
E:38 [binder, in mathcomp.solvable.abelian]
E:38 [binder, in mathcomp.algebra.poly]
E:380 [binder, in mathcomp.field.galois]
e:381 [binder, in mathcomp.field.algnum]
E:381 [binder, in mathcomp.solvable.abelian]
E:383 [binder, in mathcomp.solvable.abelian]
E:384 [binder, in mathcomp.field.galois]
E:385 [binder, in mathcomp.field.galois]
e:386 [binder, in mathcomp.field.algnum]
E:388 [binder, in mathcomp.field.galois]
e:389 [binder, in mathcomp.field.algnum]
E:39 [binder, in mathcomp.field.galois]
E:39 [binder, in mathcomp.solvable.abelian]
e:391 [binder, in mathcomp.field.algnum]
e:394 [binder, in mathcomp.field.algnum]
e:4 [binder, in mathcomp.fingroup.presentation]
e:4 [binder, in mathcomp.ssreflect.fintype]
e:40 [binder, in mathcomp.ssreflect.ssrAC]
E:405 [binder, in mathcomp.solvable.abelian]
E:406 [binder, in mathcomp.field.closed_field]
E:408 [binder, in mathcomp.field.closed_field]
E:41 [binder, in mathcomp.algebra.poly]
E:410 [binder, in mathcomp.algebra.mxpoly]
E:410 [binder, in mathcomp.field.closed_field]
E:411 [binder, in mathcomp.solvable.abelian]
E:412 [binder, in mathcomp.field.closed_field]
E:414 [binder, in mathcomp.algebra.mxpoly]
E:414 [binder, in mathcomp.field.closed_field]
E:417 [binder, in mathcomp.algebra.mxpoly]
E:422 [binder, in mathcomp.algebra.mxpoly]
E:422 [binder, in mathcomp.field.closed_field]
E:423 [binder, in mathcomp.field.closed_field]
E:423 [binder, in mathcomp.algebra.poly]
E:424 [binder, in mathcomp.field.closed_field]
E:426 [binder, in mathcomp.field.closed_field]
E:428 [binder, in mathcomp.fingroup.gproduct]
e:429 [binder, in mathcomp.character.character]
E:431 [binder, in mathcomp.solvable.extremal]
E:432 [binder, in mathcomp.solvable.extremal]
e:433 [binder, in mathcomp.ssreflect.div]
e:44 [binder, in mathcomp.algebra.ring_quotient]
e:44 [binder, in mathcomp.ssreflect.ssrAC]
e:44 [binder, in mathcomp.ssreflect.prime]
E:44 [binder, in mathcomp.algebra.poly]
E:440 [binder, in mathcomp.ssreflect.ssrnat]
E:444 [binder, in mathcomp.algebra.mxpoly]
e:444 [binder, in mathcomp.character.inertia]
E:445 [binder, in mathcomp.field.galois]
e:446 [binder, in mathcomp.character.inertia]
E:448 [binder, in mathcomp.field.galois]
E:448 [binder, in mathcomp.algebra.mxpoly]
E:45 [binder, in mathcomp.field.fieldext]
e:452 [binder, in mathcomp.character.inertia]
E:458 [binder, in mathcomp.field.galois]
E:462 [binder, in mathcomp.field.galois]
E:47 [binder, in mathcomp.algebra.poly]
E:48 [binder, in mathcomp.field.fieldext]
e:48 [binder, in mathcomp.ssreflect.prime]
e:483 [binder, in mathcomp.character.inertia]
E:485 [binder, in mathcomp.field.galois]
e:486 [binder, in mathcomp.fingroup.gproduct]
e:49 [binder, in mathcomp.ssreflect.ssrAC]
E:490 [binder, in mathcomp.field.galois]
E:496 [binder, in mathcomp.field.galois]
E:50 [binder, in mathcomp.algebra.poly]
e:513 [binder, in mathcomp.algebra.mxpoly]
e:514 [binder, in mathcomp.algebra.mxpoly]
E:515 [binder, in mathcomp.field.galois]
E:517 [binder, in mathcomp.field.galois]
E:518 [binder, in mathcomp.solvable.abelian]
e:52 [binder, in mathcomp.field.cyclotomic]
E:523 [binder, in mathcomp.field.galois]
e:528 [binder, in mathcomp.algebra.mxpoly]
E:533 [binder, in mathcomp.field.galois]
E:536 [binder, in mathcomp.field.galois]
e:54 [binder, in mathcomp.field.closed_field]
e:54 [binder, in mathcomp.ssreflect.prime]
E:54 [binder, in mathcomp.algebra.poly]
E:542 [binder, in mathcomp.field.galois]
E:545 [binder, in mathcomp.field.galois]
E:547 [binder, in mathcomp.field.galois]
E:55 [binder, in mathcomp.field.fieldext]
E:55 [binder, in mathcomp.solvable.extraspecial]
e:556 [binder, in mathcomp.algebra.mxalgebra]
e:557 [binder, in mathcomp.algebra.mxpoly]
E:56 [binder, in mathcomp.field.galois]
e:56 [binder, in mathcomp.ssreflect.ssrAC]
e:56 [binder, in mathcomp.field.closed_field]
E:561 [binder, in mathcomp.algebra.poly]
e:561 [binder, in mathcomp.algebra.mxalgebra]
e:562 [binder, in mathcomp.algebra.mxpoly]
E:565 [binder, in mathcomp.field.galois]
e:566 [binder, in mathcomp.algebra.mxpoly]
e:566 [binder, in mathcomp.algebra.mxalgebra]
e:571 [binder, in mathcomp.fingroup.action]
e:573 [binder, in mathcomp.fingroup.action]
E:574 [binder, in mathcomp.field.galois]
e:578 [binder, in mathcomp.algebra.mxpoly]
e:579 [binder, in mathcomp.algebra.mxpoly]
E:58 [binder, in mathcomp.field.fieldext]
e:58 [binder, in mathcomp.ssreflect.ssrAC]
e:587 [binder, in mathcomp.ssreflect.prime]
e:589 [binder, in mathcomp.algebra.mxpoly]
E:59 [binder, in mathcomp.field.fieldext]
e:590 [binder, in mathcomp.algebra.mxpoly]
e:593 [binder, in mathcomp.algebra.mxpoly]
e:598 [binder, in mathcomp.algebra.mxpoly]
e:6 [binder, in mathcomp.ssreflect.prime]
E:60 [binder, in mathcomp.field.galois]
e:61 [binder, in mathcomp.field.closed_field]
E:62 [binder, in mathcomp.field.fieldext]
E:63 [binder, in mathcomp.field.algebraics_fundamentals]
e:633 [binder, in mathcomp.algebra.polydiv]
e:638 [binder, in mathcomp.algebra.polydiv]
e:641 [binder, in mathcomp.algebra.polydiv]
e:644 [binder, in mathcomp.algebra.polydiv]
e:648 [binder, in mathcomp.solvable.abelian]
e:649 [binder, in mathcomp.solvable.abelian]
E:65 [binder, in mathcomp.field.galois]
e:650 [binder, in mathcomp.ssreflect.ssrnat]
e:650 [binder, in mathcomp.solvable.abelian]
E:658 [binder, in mathcomp.field.galois]
E:661 [binder, in mathcomp.field.galois]
E:663 [binder, in mathcomp.field.galois]
E:665 [binder, in mathcomp.field.galois]
E:667 [binder, in mathcomp.field.galois]
e:671 [binder, in mathcomp.ssreflect.ssrnat]
e:674 [binder, in mathcomp.ssreflect.ssrnat]
e:677 [binder, in mathcomp.ssreflect.ssrnat]
e:678 [binder, in mathcomp.ssreflect.ssrnat]
E:68 [binder, in mathcomp.field.galois]
e:68 [binder, in mathcomp.field.closed_field]
E:71 [binder, in mathcomp.field.galois]
e:71 [binder, in mathcomp.ssreflect.ssrAC]
E:74 [binder, in mathcomp.field.separable]
E:75 [binder, in mathcomp.field.galois]
e:75 [binder, in mathcomp.ssreflect.fingraph]
e:76 [binder, in mathcomp.field.closed_field]
E:77 [binder, in mathcomp.field.algebraics_fundamentals]
e:77 [binder, in mathcomp.ssreflect.fingraph]
e:78 [binder, in mathcomp.field.closed_field]
e:79 [binder, in mathcomp.ssreflect.fingraph]
E:80 [binder, in mathcomp.field.galois]
e:81 [binder, in mathcomp.ssreflect.ssrAC]
e:81 [binder, in mathcomp.ssreflect.fingraph]
e:82 [binder, in mathcomp.ssreflect.ssrAC]
e:83 [binder, in mathcomp.ssreflect.fingraph]
E:831 [binder, in mathcomp.algebra.ssralg]
e:85 [binder, in mathcomp.ssreflect.div]
E:85 [binder, in mathcomp.field.galois]
e:86 [binder, in mathcomp.field.closed_field]
e:87 [binder, in mathcomp.ssreflect.fingraph]
E:870 [binder, in mathcomp.ssreflect.bigop]
e:88 [binder, in mathcomp.ssreflect.fingraph]
e:90 [binder, in mathcomp.ssreflect.fingraph]
E:90 [binder, in mathcomp.solvable.extraspecial]
E:91 [binder, in mathcomp.solvable.extraspecial]
E:916 [binder, in mathcomp.algebra.ssralg]
e:92 [binder, in mathcomp.ssreflect.fingraph]
E:933 [binder, in mathcomp.algebra.ssralg]
e:96 [binder, in mathcomp.field.closed_field]
E:96 [binder, in mathcomp.field.finfield]
E:960 [binder, in mathcomp.algebra.ssrnum]
e:963 [binder, in mathcomp.ssreflect.bigop]
E:968 [binder, in mathcomp.algebra.ssrnum]
E:98 [binder, in mathcomp.field.separable]
E:98 [binder, in mathcomp.field.finfield]
E:99 [binder, in mathcomp.field.separable]
| 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 | (80254 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 | (1852 entries) |
| Binder Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (48996 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 | (383 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 | (4219 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 | (93 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 | (14738 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 | (223 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 | (132 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 | (452 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 | (1431 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 | (1169 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 | (6273 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 | (248 entries) |