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

(54001 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

(1931 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

(1658 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

(7199 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

(97 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

(15214 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

(75 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

(224 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

(2371 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

(2266 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

(732 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

(21455 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

(647 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]
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]
eigenpoly_conjmx [lemma, in mathcomp.algebra.mxred]
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_conjmx [lemma, in mathcomp.algebra.mxred]
eigenvalue_closed [lemma, in mathcomp.algebra.spectral]
eigenvalue_map [lemma, in mathcomp.algebra.mxalgebra]
eigenvectorP [lemma, in mathcomp.algebra.mxalgebra]
eisenstein_crit [lemma, in mathcomp.algebra.intdiv]
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]
enumP_subdef [definition, 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_setI [lemma, in mathcomp.ssreflect.finset]
enum_setU [lemma, in mathcomp.ssreflect.finset]
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_unlock_subterm [definition, in mathcomp.ssreflect.fintype]
enum_rank_in.unlock [definition, in mathcomp.ssreflect.fintype]
enum_rank_in.body [definition, in mathcomp.ssreflect.fintype]
enum_rank_in [module, in mathcomp.ssreflect.fintype]
enum_rank_in_Locked.unlock [axiom, in mathcomp.ssreflect.fintype]
enum_rank_in_Locked.body [axiom, in mathcomp.ssreflect.fintype]
enum_rank_in_Locked [module, 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]
enum_subdef [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]
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]
eqbP [lemma, in mathcomp.ssreflect.eqtype]
eqbRHS [abbreviation, in mathcomp.ssreflect.eqtype]
eqb_negLR [lemma, in mathcomp.ssreflect.eqtype]
eqb_id [lemma, in mathcomp.ssreflect.eqtype]
eqb0 [lemma, in mathcomp.ssreflect.ssrnat]
eqb1 [lemma, in mathcomp.ssreflect.ssrnat]
eqcfP [abbreviation, in mathcomp.character.classfun]
eqCmodD [lemma, in mathcomp.field.algC]
eqCmodDl [lemma, in mathcomp.field.algC]
eqCmodDr [lemma, in mathcomp.field.algC]
eqCmodM [lemma, in mathcomp.field.algC]
eqCmodMl [lemma, in mathcomp.field.algC]
eqCmodMl0 [lemma, in mathcomp.field.algC]
eqCmodMr [lemma, in mathcomp.field.algC]
eqCmodMr0 [lemma, in mathcomp.field.algC]
eqCmodm0 [lemma, in mathcomp.field.algC]
eqCmodN [lemma, in mathcomp.field.algC]
eqCmod_addl_mul [lemma, in mathcomp.field.algC]
eqCmod_nat [lemma, in mathcomp.field.algC]
eqCmod_transr [lemma, in mathcomp.field.algC]
eqCmod_transl [lemma, in mathcomp.field.algC]
eqCmod_trans [lemma, in mathcomp.field.algC]
eqCmod_sym [lemma, in mathcomp.field.algC]
eqCmod_refl [lemma, in mathcomp.field.algC]
eqCmod0 [lemma, in mathcomp.field.algC]
eqCmod0_nat [lemma, in mathcomp.field.algC]
EqConnect [section, in mathcomp.ssreflect.fingraph]
EqConnect.T [variable, in mathcomp.ssreflect.fingraph]
eqC_nat [definition, in mathcomp.field.algC]
eqE [lemma, in mathcomp.ssreflect.eqtype]
eqEcard [lemma, in mathcomp.ssreflect.finset]
eqEdim [lemma, in mathcomp.algebra.vector]
eqEproper [lemma, in mathcomp.ssreflect.finset]
eqEsubset [lemma, in mathcomp.ssreflect.finset]
eqEsubv [lemma, in mathcomp.algebra.vector]
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]
eqlfunP [lemma, in mathcomp.algebra.vector]
eqlfun_inP [lemma, in mathcomp.algebra.vector]
EqMap [section, in mathcomp.ssreflect.seq]
EqMap.f [variable, in mathcomp.ssreflect.seq]
EqMap.Hf [variable, in mathcomp.ssreflect.seq]
EqMap.n0 [variable, in mathcomp.ssreflect.seq]
EqMap.T1 [variable, in mathcomp.ssreflect.seq]
EqMap.T2 [variable, in mathcomp.ssreflect.seq]
EqMap.x1 [variable, in mathcomp.ssreflect.seq]
EqMap.x2 [variable, in mathcomp.ssreflect.seq]
EqMask [section, in mathcomp.ssreflect.seq]
EqMask.n0 [variable, in mathcomp.ssreflect.seq]
EqMask.T [variable, in mathcomp.ssreflect.seq]
eqmodE [lemma, in mathcomp.ssreflect.generic_quotient]
eqmodP [lemma, in mathcomp.ssreflect.generic_quotient]
eqmx [definition, in mathcomp.algebra.mxalgebra]
eqmxMfree [lemma, in mathcomp.algebra.mxalgebra]
eqmxMfull [lemma, in mathcomp.algebra.mxalgebra]
eqmxMr [lemma, in mathcomp.algebra.mxalgebra]
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_schmidt_free [lemma, in mathcomp.algebra.spectral]
eqmx_schmidt_full [lemma, in mathcomp.algebra.spectral]
eqmx_ReiIm [lemma, in mathcomp.algebra.spectral]
eqmx_ortho [lemma, in mathcomp.algebra.sesquilinear]
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 [definition, 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]
EqQuotient [module, in mathcomp.ssreflect.generic_quotient]
EqQuotientElpiOperations [module, in mathcomp.ssreflect.generic_quotient]
EqQuotient.axioms_ [record, in mathcomp.ssreflect.generic_quotient]
EqQuotient.class [projection, in mathcomp.ssreflect.generic_quotient]
EqQuotient.eqtype_hasDecEq_mixin [projection, in mathcomp.ssreflect.generic_quotient]
EqQuotient.Exports [module, in mathcomp.ssreflect.generic_quotient]
EqQuotient.Exports.generic_quotient_EqQuotient__to__eqtype_Equality [definition, in mathcomp.ssreflect.generic_quotient]
EqQuotient.Exports.generic_quotient_EqQuotient_class__to__eqtype_Equality_class [definition, in mathcomp.ssreflect.generic_quotient]
EqQuotient.Exports.generic_quotient_EqQuotient__to__generic_quotient_Quotient [definition, in mathcomp.ssreflect.generic_quotient]
EqQuotient.Exports.generic_quotient_EqQuotient_class__to__generic_quotient_Quotient_class [definition, in mathcomp.ssreflect.generic_quotient]
EqQuotient.Exports.join_generic_quotient_EqQuotient_between_eqtype_Equality_and_generic_quotient_Quotient [definition, in mathcomp.ssreflect.generic_quotient]
EqQuotient.generic_quotient_isEqQuotient_mixin [projection, in mathcomp.ssreflect.generic_quotient]
EqQuotient.generic_quotient_isQuotient_mixin [projection, in mathcomp.ssreflect.generic_quotient]
EqQuotient.pack_ [definition, in mathcomp.ssreflect.generic_quotient]
EqQuotient.phant_on_ [definition, in mathcomp.ssreflect.generic_quotient]
EqQuotient.phant_clone [definition, in mathcomp.ssreflect.generic_quotient]
EqQuotient.sort [projection, in mathcomp.ssreflect.generic_quotient]
EqQuotient.type [record, 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]
eqrXz2 [lemma, in mathcomp.algebra.ssrint]
eqr_int [lemma, in mathcomp.algebra.ssrint]
eqseq [definition, in mathcomp.ssreflect.seq]
EqSeq [section, in mathcomp.ssreflect.seq]
eqseqE [lemma, in mathcomp.ssreflect.seq]
eqseqP [lemma, in mathcomp.ssreflect.seq]
eqseq_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]
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]
eqtype_Equality__to__eqtype_hasDecEq [definition, in mathcomp.ssreflect.tuple]
eqtype_Equality__to__eqtype_hasDecEq [definition, in mathcomp.ssreflect.seq]
eqtype_sub_type__canonical__choice_Countable [definition, in mathcomp.ssreflect.choice]
eqtype_sub_type__canonical__choice_SubChoice [definition, in mathcomp.ssreflect.choice]
eqtype_can_type__canonical__choice_Countable [definition, in mathcomp.ssreflect.choice]
eqtype_pcan_type__canonical__choice_Countable [definition, in mathcomp.ssreflect.choice]
eqtype_sub_type__canonical__choice_Choice [definition, in mathcomp.ssreflect.choice]
eqtype_can_type__canonical__choice_Choice [definition, in mathcomp.ssreflect.choice]
eqtype_pcan_type__canonical__choice_Choice [definition, in mathcomp.ssreflect.choice]
eqtype_Equality__to__eqtype_hasDecEq [definition, in mathcomp.ssreflect.choice]
eqtype_Equality__to__eqtype_hasDecEq [definition, in mathcomp.ssreflect.ssrnat]
eqtype_Equality__to__eqtype_hasDecEq__8 [definition, in mathcomp.ssreflect.finfun]
eqtype_Equality__to__eqtype_hasDecEq [definition, in mathcomp.ssreflect.finfun]
eqtype_Equality__to__eqtype_hasDecEq [definition, in mathcomp.algebra.matrix]
eqtype_SubType__to__eqtype_isSub__28 [definition, in mathcomp.solvable.burnside_app]
eqtype_SubType__to__eqtype_isSub [definition, in mathcomp.solvable.burnside_app]
eqtype_Equality__to__eqtype_hasDecEq [definition, in mathcomp.algebra.rat]
eqtype_Equality__to__eqtype_hasDecEq__43 [definition, in mathcomp.ssreflect.fintype]
eqtype_sub_type__canonical__fintype_SubFinite [definition, in mathcomp.ssreflect.fintype]
eqtype_sub_type__canonical__fintype_Finite [definition, in mathcomp.ssreflect.fintype]
eqtype_can_type__canonical__fintype_Finite [definition, in mathcomp.ssreflect.fintype]
eqtype_pcan_type__canonical__fintype_Finite [definition, in mathcomp.ssreflect.fintype]
eqtype_Equality__to__eqtype_hasDecEq [definition, in mathcomp.ssreflect.fintype]
eqtype_Equality__to__eqtype_hasDecEq__36 [definition, in mathcomp.ssreflect.eqtype]
eqtype_Equality__to__eqtype_hasDecEq__31 [definition, in mathcomp.ssreflect.eqtype]
eqtype_sub_type__canonical__eqtype_SubEquality [definition, in mathcomp.ssreflect.eqtype]
eqtype_sub_type__canonical__eqtype_Equality [definition, in mathcomp.ssreflect.eqtype]
eqtype_Equality__to__eqtype_hasDecEq__26 [definition, in mathcomp.ssreflect.eqtype]
eqtype_sub_type__canonical__eqtype_SubType [definition, in mathcomp.ssreflect.eqtype]
eqtype_SubType__to__eqtype_isSub [definition, in mathcomp.ssreflect.eqtype]
eqtype_can_type__canonical__eqtype_Equality [definition, in mathcomp.ssreflect.eqtype]
eqtype_Equality__to__eqtype_hasDecEq__18 [definition, in mathcomp.ssreflect.eqtype]
eqtype_pcan_type__canonical__eqtype_Equality [definition, in mathcomp.ssreflect.eqtype]
eqtype_Equality__to__eqtype_hasDecEq [definition, in mathcomp.ssreflect.eqtype]
eqtype_inj_type__canonical__eqtype_Equality [definition, in mathcomp.ssreflect.eqtype]
eqtype_Equality__to__eqtype_hasDecEq [definition, in mathcomp.field.falgebra]
Equality [module, in mathcomp.ssreflect.eqtype]
EqualityElpiOperations [module, in mathcomp.ssreflect.eqtype]
Equality.axioms_ [record, in mathcomp.ssreflect.eqtype]
Equality.class [projection, in mathcomp.ssreflect.eqtype]
Equality.eqtype_hasDecEq_mixin [projection, in mathcomp.ssreflect.eqtype]
Equality.Exports [module, in mathcomp.ssreflect.eqtype]
Equality.pack_ [definition, in mathcomp.ssreflect.eqtype]
Equality.phant_on_ [definition, in mathcomp.ssreflect.eqtype]
Equality.phant_clone [definition, 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]
equivmx [definition, in mathcomp.algebra.mxalgebra]
equivmx_spec [definition, in mathcomp.algebra.mxalgebra]
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_type_of__canonical__choice_Countable [definition, in mathcomp.ssreflect.generic_quotient]
EquivQuot.canon [definition, in mathcomp.ssreflect.generic_quotient]
EquivQuot.canon_id [lemma, in mathcomp.ssreflect.generic_quotient]
EquivQuot.choice_Choice__to__eqtype_hasDecEq [definition, in mathcomp.ssreflect.generic_quotient]
EquivQuot.choice_Choice__to__choice_hasChoice [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.eqmodE [lemma, in mathcomp.ssreflect.generic_quotient]
EquivQuot.eqmodP [lemma, in mathcomp.ssreflect.generic_quotient]
EquivQuot.equivQTP [lemma, in mathcomp.ssreflect.generic_quotient]
EquivQuot.EquivQuot [section, in mathcomp.ssreflect.generic_quotient]
EquivQuot.equivQuotient [record, in mathcomp.ssreflect.generic_quotient]
EquivQuot.EquivQuot_type_of__canonical__generic_quotient_EqQuotient [definition, in mathcomp.ssreflect.generic_quotient]
EquivQuot.EquivQuot_type_of__canonical__choice_Choice [definition, in mathcomp.ssreflect.generic_quotient]
EquivQuot.EquivQuot_type_of__canonical__eqtype_Equality [definition, in mathcomp.ssreflect.generic_quotient]
EquivQuot.EquivQuot_type_of__canonical__generic_quotient_Quotient [definition, 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.Exports [module, in mathcomp.ssreflect.generic_quotient]
EquivQuot.HB_unnamed_factory_35 [definition, in mathcomp.ssreflect.generic_quotient]
EquivQuot.HB_unnamed_mixin_34 [definition, in mathcomp.ssreflect.generic_quotient]
EquivQuot.HB_unnamed_mixin_33 [definition, in mathcomp.ssreflect.generic_quotient]
EquivQuot.HB_unnamed_factory_30 [definition, in mathcomp.ssreflect.generic_quotient]
EquivQuot.HB_unnamed_factory_28 [definition, 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.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]
eqVneq [lemma, in mathcomp.ssreflect.eqtype]
eqVproper [lemma, in mathcomp.ssreflect.finset]
eqxx [abbreviation, in mathcomp.ssreflect.eqtype]
eqz_mod_dvd [lemma, in mathcomp.algebra.intdiv]
eqz_mul [lemma, in mathcomp.algebra.intdiv]
eqz_div [lemma, in mathcomp.algebra.intdiv]
eqz_modDr [lemma, in mathcomp.algebra.intdiv]
eqz_modDl [lemma, in mathcomp.algebra.intdiv]
eqz_nat [lemma, in mathcomp.algebra.ssrint]
eq_porbit_mem [lemma, in mathcomp.fingroup.perm]
eq_op_trans [lemma, in mathcomp.ssreflect.generic_quotient]
eq_lock [lemma, in mathcomp.ssreflect.generic_quotient]
eq_mktuple [lemma, 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_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_setXn [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_col_mx [lemma, in mathcomp.algebra.matrix]
eq_row_mx [lemma, in mathcomp.algebra.matrix]
eq_castmx [lemma, 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_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_orthonormal [lemma, in mathcomp.algebra.sesquilinear]
eq_pairwise_orthogonal [lemma, in mathcomp.algebra.sesquilinear]
eq_dim_orthov1 [lemma, in mathcomp.algebra.sesquilinear]
eq_map_mx_id [lemma, in mathcomp.algebra.sesquilinear]
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_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_in_map_poly [lemma, in mathcomp.algebra.poly]
eq_in_map_poly_id0 [lemma, in mathcomp.algebra.poly]
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_axiom [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]
ErV [abbreviation, in mathcomp.character.mxabelem]
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_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]
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]
expgnE [lemma, 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 [lemma, 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]
Exports_Crat__canonical__GRing_DivringClosed [definition, in mathcomp.field.algC]
Exports_Crat__canonical__GRing_SubringClosed [definition, in mathcomp.field.algC]
Exports_Crat__canonical__GRing_ZmodClosed [definition, in mathcomp.field.algC]
Exports_Crat__canonical__GRing_SdivClosed [definition, in mathcomp.field.algC]
Exports_Crat__canonical__GRing_SmulClosed [definition, in mathcomp.field.algC]
Exports_Crat__canonical__GRing_OppClosed [definition, in mathcomp.field.algC]
Exports_Crat__canonical__GRing_SemiringClosed [definition, in mathcomp.field.algC]
Exports_Crat__canonical__GRing_DivClosed [definition, in mathcomp.field.algC]
Exports_Crat__canonical__GRing_MulClosed [definition, in mathcomp.field.algC]
Exports_Crat__canonical__GRing_Semiring2Closed [definition, in mathcomp.field.algC]
Exports_Crat__canonical__GRing_Mul2Closed [definition, in mathcomp.field.algC]
Exports_Crat__canonical__GRing_AddClosed [definition, in mathcomp.field.algC]
Exports_dvdC__canonical__GRing_ZmodClosed [definition, in mathcomp.field.algC]
Exports_dvdC__canonical__GRing_OppClosed [definition, in mathcomp.field.algC]
Exports_dvdC__canonical__GRing_AddClosed [definition, in mathcomp.field.algC]
exprMz_comm [lemma, in mathcomp.algebra.ssrint]
exprnN [lemma, in mathcomp.algebra.ssrint]
exprnP [lemma, in mathcomp.algebra.ssrint]
exprN1 [lemma, in mathcomp.algebra.ssrint]
exprSz [lemma, in mathcomp.algebra.ssrint]
exprSzr [lemma, in mathcomp.algebra.ssrint]
exprz [definition, in mathcomp.algebra.ssrint]
exprzAC [lemma, in mathcomp.algebra.ssrint]
exprzDr [lemma, in mathcomp.algebra.ssrint]
exprzD_ss [lemma, in mathcomp.algebra.ssrint]
exprzD_Nnat [lemma, in mathcomp.algebra.ssrint]
exprzD_nat [lemma, in mathcomp.algebra.ssrint]
ExprzField [section, in mathcomp.algebra.ssrint]
ExprzField.F [variable, in mathcomp.algebra.ssrint]
ExprzIdomain [section, in mathcomp.algebra.ssrint]
ExprzIdomain.R [variable, in mathcomp.algebra.ssrint]
exprzMl [lemma, in mathcomp.algebra.ssrint]
exprzMzl [lemma, in mathcomp.algebra.ssrint]
ExprzOrder [section, in mathcomp.algebra.ssrint]
ExprzOrder.R [variable, in mathcomp.algebra.ssrint]
ExprzUnitRing [section, in mathcomp.algebra.ssrint]
ExprzUnitRing.R [variable, in mathcomp.algebra.ssrint]
exprz_gte0 [definition, in mathcomp.algebra.ssrint]
exprz_gt0 [lemma, in mathcomp.algebra.ssrint]
exprz_ge0 [lemma, in mathcomp.algebra.ssrint]
exprz_pintl [lemma, in mathcomp.algebra.ssrint]
exprz_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_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]
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_scalable_subproof [lemma, in mathcomp.field.separable]
extendDerivation_additive_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]
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]
ExternalDirDepProd [section, in mathcomp.fingroup.gproduct]
ExternalDirDepProd.gT [variable, in mathcomp.fingroup.gproduct]
ExternalDirDepProd.I [variable, in mathcomp.fingroup.gproduct]
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]
extnprod_mulgA [lemma, in mathcomp.fingroup.gproduct]
extnprod_mulVg [lemma, in mathcomp.fingroup.gproduct]
extnprod_mul1g [lemma, in mathcomp.fingroup.gproduct]
extnprod_invg [definition, in mathcomp.fingroup.gproduct]
extnprod_mulg [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_extremal_group_type__canonical__choice_Countable [definition, in mathcomp.solvable.extremal]
extremal_extremal_group_type__canonical__choice_Choice [definition, in mathcomp.solvable.extremal]
extremal_extremal_group_type__canonical__eqtype_Equality [definition, in mathcomp.solvable.extremal]
extremal_group_type_sind [definition, in mathcomp.solvable.extremal]
extremal_group_type_rec [definition, in mathcomp.solvable.extremal]
extremal_group_type_ind [definition, in mathcomp.solvable.extremal]
extremal_group_type_rect [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_of [abbreviation, 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.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.ConstructionCont [section, in mathcomp.solvable.extremal]
Extremal.ConstructionCont.a [variable, in mathcomp.solvable.extremal]
Extremal.ConstructionCont.b [variable, in mathcomp.solvable.extremal]
Extremal.ConstructionCont.e [variable, in mathcomp.solvable.extremal]
Extremal.ConstructionCont.p [variable, in mathcomp.solvable.extremal]
Extremal.ConstructionCont.p_gt1 [variable, in mathcomp.solvable.extremal]
Extremal.ConstructionCont.q [variable, in mathcomp.solvable.extremal]
Extremal.ConstructionCont.q_gt1 [variable, 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.q [variable, in mathcomp.solvable.extremal]
Extremal.gact [abbreviation, in mathcomp.solvable.extremal]
Extremal.gact [definition, in mathcomp.solvable.extremal]
Extremal.Grp [lemma, in mathcomp.solvable.extremal]
Extremal.gtype [abbreviation, in mathcomp.solvable.extremal]
Extremal.gtype [module, in mathcomp.solvable.extremal]
Extremal.gtype_unlockable [definition, in mathcomp.solvable.extremal]
Extremal.gtype_unlock_subterm [definition, in mathcomp.solvable.extremal]
Extremal.gtype_Locked.unlock [axiom, in mathcomp.solvable.extremal]
Extremal.gtype_Locked.body [axiom, in mathcomp.solvable.extremal]
Extremal.gtype_Locked [module, in mathcomp.solvable.extremal]
Extremal.gtype.body [definition, in mathcomp.solvable.extremal]
Extremal.gtype.unlock [definition, 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_sind [definition, in mathcomp.ssreflect.ssrnat]
ex_minn_spec_rec [definition, in mathcomp.ssreflect.ssrnat]
ex_minn_spec_ind [definition, in mathcomp.ssreflect.ssrnat]
ex_minn_spec_rect [definition, 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]
E_G [abbreviation, in mathcomp.character.mxrepresentation]
E_ [abbreviation, in mathcomp.character.mxrepresentation]
E_G [abbreviation, in mathcomp.character.mxrepresentation]
E_G [abbreviation, in mathcomp.character.mxrepresentation]
e' [abbreviation, in mathcomp.ssreflect.generic_quotient]
e'E [abbreviation, in mathcomp.ssreflect.generic_quotient]
e0 [abbreviation, in mathcomp.character.mxrepresentation]

---

Global Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(54001 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

(1931 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

(1658 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

(7199 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

(97 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

(15214 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

(75 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

(224 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

(2371 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

(2266 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

(732 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

(21455 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

(647 entries)

---

Index

---

This page has been generated by coqdoc