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

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

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

(72 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)

---

S

S [abbreviation, in mathcomp.character.mxrepresentation]
same_pblock [lemma, in mathcomp.ssreflect.finset]
same_fconnect1_r [lemma, in mathcomp.ssreflect.fingraph]
same_fconnect1 [lemma, in mathcomp.ssreflect.fingraph]
same_fconnect_finv [lemma, in mathcomp.ssreflect.fingraph]
same_connect_rev [lemma, in mathcomp.ssreflect.fingraph]
same_connect1r [lemma, in mathcomp.ssreflect.fingraph]
same_connect1 [lemma, in mathcomp.ssreflect.fingraph]
same_connect_r [lemma, in mathcomp.ssreflect.fingraph]
same_connect [lemma, in mathcomp.ssreflect.fingraph]
scalar_mx_sum_delta [lemma, in mathcomp.algebra.matrix]
scalar_mxC [lemma, in mathcomp.algebra.matrix]
scalar_mx_is_multiplicative [lemma, in mathcomp.algebra.matrix]
scalar_mxM [lemma, in mathcomp.algebra.matrix]
scalar_mx_is_additive [lemma, in mathcomp.algebra.matrix]
scalar_mx_block [lemma, in mathcomp.algebra.matrix]
scalar_mx_is_trig [lemma, in mathcomp.algebra.matrix]
scalar_mx_is_diag [lemma, in mathcomp.algebra.matrix]
scalar_mx_is_scalar [lemma, in mathcomp.algebra.matrix]
scalar_mx_is_semi_additive [lemma, in mathcomp.algebra.matrix]
scalar_mx [definition, in mathcomp.algebra.matrix]
scalar_mx_key [lemma, in mathcomp.algebra.matrix]
scalar_mx_hom [lemma, in mathcomp.character.mxrepresentation]
scalar_mx_cent [lemma, in mathcomp.algebra.mxalgebra]
ScaleCompLfun [section, in mathcomp.algebra.vector]
ScaleCompLfun.aT [variable, in mathcomp.algebra.vector]
ScaleCompLfun.R [variable, in mathcomp.algebra.vector]
ScaleCompLfun.rT [variable, in mathcomp.algebra.vector]
ScaleCompLfun.vT [variable, in mathcomp.algebra.vector]
scalemx [definition, in mathcomp.algebra.matrix]
scalemxA [lemma, in mathcomp.algebra.matrix]
scalemxAl [lemma, in mathcomp.algebra.matrix]
scalemxAr [lemma, in mathcomp.algebra.matrix]
scalemxDl [lemma, in mathcomp.algebra.matrix]
scalemxDr [lemma, in mathcomp.algebra.matrix]
scalemx_inj [lemma, in mathcomp.algebra.matrix]
scalemx_eq0 [lemma, in mathcomp.algebra.matrix]
scalemx_const [lemma, in mathcomp.algebra.matrix]
scalemx_key [lemma, in mathcomp.algebra.matrix]
scalemx_sub [lemma, in mathcomp.algebra.mxalgebra]
scalemx1 [lemma, in mathcomp.algebra.matrix]
scalerMzl [lemma, in mathcomp.algebra.ssrint]
scalerMzr [lemma, in mathcomp.algebra.ssrint]
scaler_int [lemma, in mathcomp.algebra.ssrint]
scalezrE [lemma, in mathcomp.algebra.ssrint]
scale_zchar [lemma, in mathcomp.character.vcharacter]
scale_scalar_mx [lemma, in mathcomp.algebra.matrix]
scale_block_mx [lemma, in mathcomp.algebra.matrix]
scale_col_mx [lemma, in mathcomp.algebra.matrix]
scale_row_mx [lemma, in mathcomp.algebra.matrix]
scale_groupAction [definition, in mathcomp.character.mxabelem]
scale_is_groupAction [lemma, in mathcomp.character.mxabelem]
scale_action [definition, in mathcomp.character.mxabelem]
scale_is_action [lemma, in mathcomp.character.mxabelem]
scale_actE [lemma, in mathcomp.character.mxabelem]
scale_act [definition, in mathcomp.character.mxabelem]
scale_pair [definition, in mathcomp.algebra.ssralg]
scale_lfunE [lemma, in mathcomp.algebra.vector]
scale_lfun [definition, in mathcomp.algebra.vector]
scale_poly_eq0 [lemma, in mathcomp.algebra.poly]
scale_polyC [lemma, in mathcomp.algebra.poly]
scale_polyAl [lemma, in mathcomp.algebra.poly]
scale_polyDl [lemma, in mathcomp.algebra.poly]
scale_polyDr [lemma, in mathcomp.algebra.poly]
scale_1poly [lemma, in mathcomp.algebra.poly]
scale_polyA [lemma, in mathcomp.algebra.poly]
scale_polyE [lemma, in mathcomp.algebra.poly]
scale_poly_unlockable [definition, in mathcomp.algebra.poly]
scale_poly [definition, in mathcomp.algebra.poly]
scale_poly_key [lemma, in mathcomp.algebra.poly]
scale_poly_def [definition, in mathcomp.algebra.poly]
scale1mx [lemma, in mathcomp.algebra.matrix]
scalq [definition, in mathcomp.algebra.rat]
scalqE [lemma, in mathcomp.algebra.rat]
scalq_eq0 [lemma, in mathcomp.algebra.rat]
scalq_def [lemma, in mathcomp.algebra.rat]
Scan [section, in mathcomp.ssreflect.seq]
scanl [definition, in mathcomp.ssreflect.seq]
scanlK [lemma, in mathcomp.ssreflect.seq]
scanl_bseq [definition, in mathcomp.ssreflect.tuple]
scanl_bseqP [lemma, in mathcomp.ssreflect.tuple]
scanl_tuple [definition, in mathcomp.ssreflect.tuple]
scanl_tupleP [lemma, in mathcomp.ssreflect.tuple]
scanl_rcons [lemma, in mathcomp.ssreflect.seq]
scanl_cat [lemma, in mathcomp.ssreflect.seq]
Scan.f [variable, in mathcomp.ssreflect.seq]
Scan.g [variable, in mathcomp.ssreflect.seq]
Scan.T1 [variable, in mathcomp.ssreflect.seq]
Scan.T2 [variable, in mathcomp.ssreflect.seq]
Scan.x1 [variable, in mathcomp.ssreflect.seq]
Scan.x2 [variable, in mathcomp.ssreflect.seq]
schmidt [definition, in mathcomp.algebra.spectral]
schmidt_complete_unitarymx [lemma, in mathcomp.algebra.spectral]
schmidt_complete [definition, in mathcomp.algebra.spectral]
schmidt_sub [lemma, in mathcomp.algebra.spectral]
schmidt_unitarymx [lemma, in mathcomp.algebra.spectral]
schmidt_subproof [lemma, in mathcomp.algebra.spectral]
Schur [lemma, in mathcomp.algebra.spectral]
SchurZassenhaus_trans_actsol [lemma, in mathcomp.solvable.hall]
SchurZassenhaus_trans_sol [lemma, in mathcomp.solvable.hall]
SchurZassenhaus_split [lemma, in mathcomp.solvable.hall]
SCN [section, in mathcomp.solvable.maximal]
SCN [definition, in mathcomp.solvable.maximal]
SCN_max [lemma, in mathcomp.solvable.maximal]
SCN_abelian [lemma, in mathcomp.solvable.maximal]
SCN_P [lemma, in mathcomp.solvable.maximal]
SCN_at [definition, in mathcomp.solvable.maximal]
SCN.G [variable, in mathcomp.solvable.maximal]
SCN.gT [variable, in mathcomp.solvable.maximal]
SCN.p [variable, in mathcomp.solvable.maximal]
SCN.SCNseries [section, in mathcomp.solvable.maximal]
SCN.SCNseries.A [variable, in mathcomp.solvable.maximal]
SCN.SCNseries.cAA [variable, in mathcomp.solvable.maximal]
SCN.SCNseries.nZA [variable, in mathcomp.solvable.maximal]
SCN.SCNseries.SCN_A [variable, in mathcomp.solvable.maximal]
SCN.SCNseries.sZA [variable, in mathcomp.solvable.maximal]
SCN.SCNseries.Z [variable, in mathcomp.solvable.maximal]
SdPair [constructor, in mathcomp.fingroup.gproduct]
sdpairE [lemma, in mathcomp.fingroup.gproduct]
sdpair_setact [lemma, in mathcomp.fingroup.gproduct]
sdpair_act [lemma, in mathcomp.fingroup.gproduct]
sdpair1 [definition, in mathcomp.fingroup.gproduct]
sdpair1_morphism [definition, in mathcomp.fingroup.gproduct]
sdpair1_morphM [lemma, in mathcomp.fingroup.gproduct]
sdpair2 [definition, in mathcomp.fingroup.gproduct]
sdpair2_morphism [definition, in mathcomp.fingroup.gproduct]
sdpair2_morphM [lemma, in mathcomp.fingroup.gproduct]
sdprod [abbreviation, in mathcomp.fingroup.gproduct]
sdprod [abbreviation, in mathcomp.fingroup.gproduct]
Sdprod [section, in mathcomp.character.character]
sdprodE [lemma, in mathcomp.fingroup.gproduct]
sdprodEY [lemma, in mathcomp.fingroup.gproduct]
sdprodg1 [lemma, in mathcomp.fingroup.gproduct]
sdprodJ [lemma, in mathcomp.fingroup.gproduct]
sdprodm [definition, in mathcomp.fingroup.gproduct]
sdprodmE [lemma, in mathcomp.fingroup.gproduct]
sdprodmEl [lemma, in mathcomp.fingroup.gproduct]
sdprodmEr [lemma, in mathcomp.fingroup.gproduct]
sdprodm_morphism [definition, in mathcomp.fingroup.gproduct]
sdprodm_eqf [lemma, in mathcomp.fingroup.gproduct]
sdprodm_sub [lemma, in mathcomp.fingroup.gproduct]
sdprodm_norm [lemma, in mathcomp.fingroup.gproduct]
sdprodP [lemma, in mathcomp.fingroup.gproduct]
SDproduct [section, in mathcomp.character.classfun]
SDproduct.defG [variable, in mathcomp.character.classfun]
SDproduct.G [variable, in mathcomp.character.classfun]
SDproduct.gT [variable, in mathcomp.character.classfun]
SDproduct.H [variable, in mathcomp.character.classfun]
SDproduct.K [variable, in mathcomp.character.classfun]
SDproduct.nsKG [variable, in mathcomp.character.classfun]
SDproduct.sHG [variable, in mathcomp.character.classfun]
SDproduct.sKG [variable, in mathcomp.character.classfun]
sdprodW [lemma, in mathcomp.fingroup.gproduct]
sdprodWC [lemma, in mathcomp.fingroup.gproduct]
sdprodWpp [lemma, in mathcomp.fingroup.gproduct]
sdprodWY [lemma, in mathcomp.fingroup.gproduct]
sdprod_cfker [lemma, in mathcomp.character.classfun]
sdprod_p'core_HallP [lemma, in mathcomp.solvable.pgroup]
sdprod_Hall_p'coreP [lemma, in mathcomp.solvable.pgroup]
sdprod_pcore_HallP [lemma, in mathcomp.solvable.pgroup]
sdprod_Hall_pcoreP [lemma, in mathcomp.solvable.pgroup]
sdprod_normal_pHallP [lemma, in mathcomp.solvable.pgroup]
sdprod_normal_p'HallP [lemma, in mathcomp.solvable.pgroup]
sdprod_Hall [lemma, in mathcomp.solvable.pgroup]
sdprod_sdpair [lemma, in mathcomp.fingroup.gproduct]
sdprod_groupType [definition, in mathcomp.fingroup.gproduct]
sdprod_mulgA [lemma, in mathcomp.fingroup.gproduct]
sdprod_mulVg [lemma, in mathcomp.fingroup.gproduct]
sdprod_mul1g [lemma, in mathcomp.fingroup.gproduct]
sdprod_mul [definition, in mathcomp.fingroup.gproduct]
sdprod_mul_proof [lemma, in mathcomp.fingroup.gproduct]
sdprod_inv [definition, in mathcomp.fingroup.gproduct]
sdprod_inv_proof [lemma, in mathcomp.fingroup.gproduct]
sdprod_one [definition, in mathcomp.fingroup.gproduct]
sdprod_by_sind [definition, in mathcomp.fingroup.gproduct]
sdprod_by_rec [definition, in mathcomp.fingroup.gproduct]
sdprod_by_ind [definition, in mathcomp.fingroup.gproduct]
sdprod_by_rect [definition, in mathcomp.fingroup.gproduct]
sdprod_by [inductive, in mathcomp.fingroup.gproduct]
sdprod_recr [lemma, in mathcomp.fingroup.gproduct]
sdprod_recl [lemma, in mathcomp.fingroup.gproduct]
sdprod_modr [lemma, in mathcomp.fingroup.gproduct]
sdprod_modl [lemma, in mathcomp.fingroup.gproduct]
sdprod_subr [lemma, in mathcomp.fingroup.gproduct]
sdprod_isog [lemma, in mathcomp.fingroup.gproduct]
sdprod_isom [lemma, in mathcomp.fingroup.gproduct]
sdprod_card [lemma, in mathcomp.fingroup.gproduct]
sdprod_normal_complP [lemma, in mathcomp.fingroup.gproduct]
sdprod_compl [lemma, in mathcomp.fingroup.gproduct]
sdprod_context [lemma, in mathcomp.fingroup.gproduct]
sdprod_Res_IirrK [lemma, in mathcomp.character.character]
sdprod_Res_IirrE [lemma, in mathcomp.character.character]
sdprod_Iirr0 [lemma, in mathcomp.character.character]
sdprod_Iirr_eq0 [lemma, in mathcomp.character.character]
sdprod_Iirr_inj [lemma, in mathcomp.character.character]
sdprod_IirrK [lemma, in mathcomp.character.character]
sdprod_IirrE [lemma, in mathcomp.character.character]
sdprod_Iirr [definition, in mathcomp.character.character]
Sdprod.defG [variable, in mathcomp.character.character]
Sdprod.G [variable, in mathcomp.character.character]
Sdprod.gT [variable, in mathcomp.character.character]
Sdprod.H [variable, in mathcomp.character.character]
Sdprod.K [variable, in mathcomp.character.character]
Sdprod.nKG [variable, in mathcomp.character.character]
sdprod1g [lemma, in mathcomp.fingroup.gproduct]
sdT [abbreviation, in mathcomp.fingroup.gproduct]
sdval [abbreviation, in mathcomp.fingroup.gproduct]
sd1 [definition, in mathcomp.solvable.burnside_app]
Sd1 [definition, in mathcomp.solvable.burnside_app]
sd1_inv [lemma, in mathcomp.solvable.burnside_app]
Sd1_inj [lemma, in mathcomp.solvable.burnside_app]
sd2 [definition, in mathcomp.solvable.burnside_app]
Sd2 [definition, in mathcomp.solvable.burnside_app]
sd2_inv [lemma, in mathcomp.solvable.burnside_app]
Sd2_inj [lemma, in mathcomp.solvable.burnside_app]
SecondIsomorphism [section, in mathcomp.fingroup.quotient]
SecondIsomorphism.gT [variable, in mathcomp.fingroup.quotient]
SecondIsomorphism.H [variable, in mathcomp.fingroup.quotient]
SecondIsomorphism.K [variable, in mathcomp.fingroup.quotient]
SecondIsomorphism.nKH [variable, in mathcomp.fingroup.quotient]
second_isog [lemma, in mathcomp.fingroup.quotient]
second_isom [lemma, in mathcomp.fingroup.quotient]
second_orthogonality_relation [lemma, in mathcomp.character.character]
section [inductive, in mathcomp.solvable.jordanholder]
Sections [section, in mathcomp.solvable.jordanholder]
Sections.gT [variable, in mathcomp.solvable.jordanholder]
section_repr_isog [lemma, in mathcomp.solvable.jordanholder]
section_reprP [lemma, in mathcomp.solvable.jordanholder]
section_repr [definition, in mathcomp.solvable.jordanholder]
section_isog [definition, in mathcomp.solvable.jordanholder]
section_group [definition, in mathcomp.solvable.jordanholder]
section_sind [definition, in mathcomp.solvable.jordanholder]
section_rec [definition, in mathcomp.solvable.jordanholder]
section_ind [definition, in mathcomp.solvable.jordanholder]
section_rect [definition, in mathcomp.solvable.jordanholder]
section_eqmx [lemma, in mathcomp.character.mxrepresentation]
section_eqmx_add [lemma, in mathcomp.character.mxrepresentation]
section_repr [definition, in mathcomp.character.mxrepresentation]
section_module [lemma, in mathcomp.character.mxrepresentation]
SemiDihedral [constructor, in mathcomp.solvable.extremal]
semidihedral_classP [lemma, in mathcomp.solvable.extremal]
semidihedral_structure [lemma, in mathcomp.solvable.extremal]
semidihedral_gtype [definition, in mathcomp.solvable.extremal]
semidirect_product [definition, in mathcomp.fingroup.gproduct]
SemiGroup [module, in mathcomp.ssreflect.bigop]
SemiGroupProperties [section, in mathcomp.ssreflect.bigop]
SemiGroupProperties.Abelian [section, in mathcomp.ssreflect.bigop]
SemiGroupProperties.Abelian.Id [section, in mathcomp.ssreflect.bigop]
SemiGroupProperties.Abelian.Id.opxx [variable, in mathcomp.ssreflect.bigop]
SemiGroupProperties.Abelian.op [variable, in mathcomp.ssreflect.bigop]
SemiGroupProperties.Abelian.opCA [variable, in mathcomp.ssreflect.bigop]
SemiGroupProperties.Abelian.x [variable, in mathcomp.ssreflect.bigop]
SemiGroupProperties.Id [section, in mathcomp.ssreflect.bigop]
SemiGroupProperties.Id.op [variable, in mathcomp.ssreflect.bigop]
SemiGroupProperties.Id.opxx [variable, in mathcomp.ssreflect.bigop]
SemiGroupProperties.Id.x [variable, in mathcomp.ssreflect.bigop]
SemiGroupProperties.R [variable, in mathcomp.ssreflect.bigop]
SemiGroup.Builders_1.Builders_Export_7 [module, in mathcomp.ssreflect.bigop]
SemiGroup.Builders_1.Builders_1_op__canonical__SemiGroup_ComLaw [definition, in mathcomp.ssreflect.bigop]
SemiGroup.Builders_1.HB_unnamed_factory_5 [definition, in mathcomp.ssreflect.bigop]
SemiGroup.Builders_1.Builders_1_op__canonical__SemiGroup_Law [definition, in mathcomp.ssreflect.bigop]
SemiGroup.Builders_1.HB_unnamed_factory_3 [definition, in mathcomp.ssreflect.bigop]
SemiGroup.Builders_1.Builders_1.fresh_name_2 [variable, in mathcomp.ssreflect.bigop]
SemiGroup.Builders_1.Builders_1.op [variable, in mathcomp.ssreflect.bigop]
SemiGroup.Builders_1.Builders_1.T [variable, in mathcomp.ssreflect.bigop]
SemiGroup.Builders_1.Builders_1.Builders_1 [section, in mathcomp.ssreflect.bigop]
SemiGroup.Builders_1.Super [module, in mathcomp.ssreflect.bigop]
SemiGroup.Builders_1 [module, in mathcomp.ssreflect.bigop]
SemiGroup.ComLaw [module, in mathcomp.ssreflect.bigop]
SemiGroup.ComLawElpiOperations [module, in mathcomp.ssreflect.bigop]
SemiGroup.ComLaw.axioms_ [record, in mathcomp.ssreflect.bigop]
SemiGroup.ComLaw.class [projection, in mathcomp.ssreflect.bigop]
SemiGroup.ComLaw.Exports [module, in mathcomp.ssreflect.bigop]
SemiGroup.ComLaw.Exports.SemiGroup_ComLaw__to__SemiGroup_Law [definition, in mathcomp.ssreflect.bigop]
SemiGroup.ComLaw.Exports.SemiGroup_ComLaw_class__to__SemiGroup_Law_class [definition, in mathcomp.ssreflect.bigop]
SemiGroup.ComLaw.pack_ [definition, in mathcomp.ssreflect.bigop]
SemiGroup.ComLaw.phant_on_ [definition, in mathcomp.ssreflect.bigop]
SemiGroup.ComLaw.phant_clone [definition, in mathcomp.ssreflect.bigop]
SemiGroup.ComLaw.SemiGroup_isCommutativeLaw_mixin [projection, in mathcomp.ssreflect.bigop]
SemiGroup.ComLaw.SemiGroup_isLaw_mixin [projection, in mathcomp.ssreflect.bigop]
SemiGroup.ComLaw.sort [projection, in mathcomp.ssreflect.bigop]
SemiGroup.ComLaw.type [record, in mathcomp.ssreflect.bigop]
SemiGroup.com_law [abbreviation, in mathcomp.ssreflect.bigop]
SemiGroup.Exports [module, in mathcomp.ssreflect.bigop]
SemiGroup.isComLaw [module, in mathcomp.ssreflect.bigop]
SemiGroup.isComLaw.axioms_ [record, in mathcomp.ssreflect.bigop]
SemiGroup.isComLaw.Exports [module, in mathcomp.ssreflect.bigop]
SemiGroup.isComLaw.isComLaw.isComLaw [section, in mathcomp.ssreflect.bigop]
SemiGroup.isComLaw.isComLaw.op [variable, in mathcomp.ssreflect.bigop]
SemiGroup.isComLaw.isComLaw.T [variable, in mathcomp.ssreflect.bigop]
SemiGroup.isComLaw.opA [projection, in mathcomp.ssreflect.bigop]
SemiGroup.isComLaw.opC [projection, in mathcomp.ssreflect.bigop]
SemiGroup.isComLaw.phant_axioms [definition, in mathcomp.ssreflect.bigop]
SemiGroup.isComLaw.phant_Build [definition, in mathcomp.ssreflect.bigop]
SemiGroup.isCommutativeLaw [module, in mathcomp.ssreflect.bigop]
SemiGroup.isCommutativeLaw.axioms_ [record, in mathcomp.ssreflect.bigop]
SemiGroup.isCommutativeLaw.Exports [module, in mathcomp.ssreflect.bigop]
SemiGroup.isCommutativeLaw.identity_builder [definition, in mathcomp.ssreflect.bigop]
SemiGroup.isCommutativeLaw.isCommutativeLaw.isCommutativeLaw [section, in mathcomp.ssreflect.bigop]
SemiGroup.isCommutativeLaw.isCommutativeLaw.op [variable, in mathcomp.ssreflect.bigop]
SemiGroup.isCommutativeLaw.isCommutativeLaw.T [variable, in mathcomp.ssreflect.bigop]
SemiGroup.isCommutativeLaw.opC [projection, in mathcomp.ssreflect.bigop]
SemiGroup.isCommutativeLaw.phant_axioms [definition, in mathcomp.ssreflect.bigop]
SemiGroup.isCommutativeLaw.phant_Build [definition, in mathcomp.ssreflect.bigop]
SemiGroup.isLaw [module, in mathcomp.ssreflect.bigop]
SemiGroup.isLaw.axioms_ [record, in mathcomp.ssreflect.bigop]
SemiGroup.isLaw.Exports [module, in mathcomp.ssreflect.bigop]
SemiGroup.isLaw.identity_builder [definition, in mathcomp.ssreflect.bigop]
SemiGroup.isLaw.isLaw.isLaw [section, in mathcomp.ssreflect.bigop]
SemiGroup.isLaw.isLaw.op [variable, in mathcomp.ssreflect.bigop]
SemiGroup.isLaw.isLaw.T [variable, in mathcomp.ssreflect.bigop]
SemiGroup.isLaw.opA [projection, in mathcomp.ssreflect.bigop]
SemiGroup.isLaw.phant_axioms [definition, in mathcomp.ssreflect.bigop]
SemiGroup.isLaw.phant_Build [definition, in mathcomp.ssreflect.bigop]
SemiGroup.law [abbreviation, in mathcomp.ssreflect.bigop]
SemiGroup.Law [module, in mathcomp.ssreflect.bigop]
SemiGroup.LawElpiOperations [module, in mathcomp.ssreflect.bigop]
SemiGroup.Law.axioms_ [record, in mathcomp.ssreflect.bigop]
SemiGroup.Law.class [projection, in mathcomp.ssreflect.bigop]
SemiGroup.Law.Exports [module, in mathcomp.ssreflect.bigop]
SemiGroup.Law.pack_ [definition, in mathcomp.ssreflect.bigop]
SemiGroup.Law.phant_on_ [definition, in mathcomp.ssreflect.bigop]
SemiGroup.Law.phant_clone [definition, in mathcomp.ssreflect.bigop]
SemiGroup.Law.SemiGroup_isLaw_mixin [projection, in mathcomp.ssreflect.bigop]
SemiGroup.Law.sort [projection, in mathcomp.ssreflect.bigop]
SemiGroup.Law.type [record, in mathcomp.ssreflect.bigop]
SemiGroup.opA [definition, in mathcomp.ssreflect.bigop]
SemiGroup.opC [definition, in mathcomp.ssreflect.bigop]
SemiGroup.Theory [module, in mathcomp.ssreflect.bigop]
SemiGroup.Theory.mulmA [lemma, in mathcomp.ssreflect.bigop]
SemiGroup.Theory.mulmAC [lemma, in mathcomp.ssreflect.bigop]
SemiGroup.Theory.mulmACA [lemma, in mathcomp.ssreflect.bigop]
SemiGroup.Theory.mulmC [lemma, in mathcomp.ssreflect.bigop]
SemiGroup.Theory.mulmCA [lemma, in mathcomp.ssreflect.bigop]
SemiGroup.Theory.Theory [section, in mathcomp.ssreflect.bigop]
SemiGroup.Theory.Theory.Commutative [section, in mathcomp.ssreflect.bigop]
SemiGroup.Theory.Theory.Commutative.mul [variable, in mathcomp.ssreflect.bigop]
SemiGroup.Theory.Theory.Plain [section, in mathcomp.ssreflect.bigop]
SemiGroup.Theory.Theory.Plain.mul [variable, in mathcomp.ssreflect.bigop]
SemiGroup.Theory.Theory.T [variable, in mathcomp.ssreflect.bigop]
SemiPolynomialTheory [section, in mathcomp.algebra.poly]
SemiPolynomialTheory.R [variable, in mathcomp.algebra.poly]
_ %:P [notation, in mathcomp.algebra.poly]
\poly_ ( _ < _ ) _ [notation, in mathcomp.algebra.poly]
semiprime [definition, in mathcomp.solvable.frobenius]
semiprimeJ [lemma, in mathcomp.solvable.frobenius]
semiprimeS [lemma, in mathcomp.solvable.frobenius]
semiprime_regular [lemma, in mathcomp.solvable.frobenius]
semiregular [definition, in mathcomp.solvable.frobenius]
semiregularJ [lemma, in mathcomp.solvable.frobenius]
semiregularS [lemma, in mathcomp.solvable.frobenius]
semiregular_prime [lemma, in mathcomp.solvable.frobenius]
semiregular_sym [lemma, in mathcomp.solvable.frobenius]
semiregular1l [lemma, in mathcomp.solvable.frobenius]
semiregular1r [lemma, in mathcomp.solvable.frobenius]
semisimple_Socle [lemma, in mathcomp.character.mxrepresentation]
separable [definition, in mathcomp.field.separable]
Separable [section, in mathcomp.field.separable]
separable [abbreviation, in mathcomp.field.separable]
separable [library]
separableP [lemma, in mathcomp.field.separable]
separablePn [lemma, in mathcomp.field.separable]
SeparablePoly [section, in mathcomp.field.separable]
SeparablePoly.R [variable, in mathcomp.field.separable]
separableS [lemma, in mathcomp.field.separable]
separableSl [lemma, in mathcomp.field.separable]
separableSr [lemma, in mathcomp.field.separable]
separable_Xn_sub_1 [lemma, in mathcomp.field.cyclotomic]
separable_Fadjoin_seq [lemma, in mathcomp.field.separable]
separable_trans [lemma, in mathcomp.field.separable]
separable_refl [lemma, in mathcomp.field.separable]
separable_generator_maximal [lemma, in mathcomp.field.separable]
separable_generatorP [lemma, in mathcomp.field.separable]
separable_generator_mem [lemma, in mathcomp.field.separable]
separable_generator [definition, in mathcomp.field.separable]
separable_inseparable_decomposition [lemma, in mathcomp.field.separable]
separable_sum [lemma, in mathcomp.field.separable]
separable_add [lemma, in mathcomp.field.separable]
separable_inseparable_element [lemma, in mathcomp.field.separable]
separable_exponent [lemma, in mathcomp.field.separable]
separable_elementS [lemma, in mathcomp.field.separable]
separable_body__canonical__GRing_Linear [definition, in mathcomp.field.separable]
separable_body__canonical__GRing_Additive [definition, in mathcomp.field.separable]
separable_root_der [lemma, in mathcomp.field.separable]
separable_nz_der [lemma, in mathcomp.field.separable]
separable_elementP [lemma, in mathcomp.field.separable]
separable_element [definition, in mathcomp.field.separable]
separable_map [lemma, in mathcomp.field.separable]
separable_prod_XsubC [lemma, in mathcomp.field.separable]
separable_root [lemma, in mathcomp.field.separable]
separable_mul [lemma, in mathcomp.field.separable]
separable_deriv_eq0 [lemma, in mathcomp.field.separable]
separable_nosquare [lemma, in mathcomp.field.separable]
separable_coprime [lemma, in mathcomp.field.separable]
separable_polyP [lemma, in mathcomp.field.separable]
separable_poly_neq0 [lemma, in mathcomp.field.separable]
separable_poly_unlockable [definition, in mathcomp.field.separable]
separable_poly_unlock_subterm [definition, in mathcomp.field.separable]
separable_poly.unlock [definition, in mathcomp.field.separable]
separable_poly.body [definition, in mathcomp.field.separable]
separable_poly [module, in mathcomp.field.separable]
separable_poly_Locked.unlock [axiom, in mathcomp.field.separable]
separable_poly_Locked.body [axiom, in mathcomp.field.separable]
separable_poly_Locked [module, in mathcomp.field.separable]
Separable.Derivation [section, in mathcomp.field.separable]
Separable.DerivationAlgebra [section, in mathcomp.field.separable]
Separable.DerivationAlgebra.D [variable, in mathcomp.field.separable]
Separable.DerivationAlgebra.derD [variable, in mathcomp.field.separable]
Separable.DerivationAlgebra.E [variable, in mathcomp.field.separable]
Separable.Derivation.D [variable, in mathcomp.field.separable]
Separable.Derivation.derD [variable, in mathcomp.field.separable]
Separable.Derivation.K [variable, in mathcomp.field.separable]
Separable.F [variable, in mathcomp.field.separable]
Separable.L [variable, in mathcomp.field.separable]
Separable.PrimitiveElementTheorem [section, in mathcomp.field.separable]
Separable.PrimitiveElementTheorem.FiniteCase [section, in mathcomp.field.separable]
Separable.PrimitiveElementTheorem.FiniteCase.cyclic_or_large [variable, in mathcomp.field.separable]
Separable.PrimitiveElementTheorem.FiniteCase.K_is_large [variable, in mathcomp.field.separable]
Separable.PrimitiveElementTheorem.FiniteCase.N [variable, in mathcomp.field.separable]
Separable.PrimitiveElementTheorem.K [variable, in mathcomp.field.separable]
Separable.PrimitiveElementTheorem.sepKy [variable, in mathcomp.field.separable]
Separable.PrimitiveElementTheorem.x [variable, in mathcomp.field.separable]
Separable.PrimitiveElementTheorem.y [variable, in mathcomp.field.separable]
Separable.SeparableElement [section, in mathcomp.field.separable]
Separable.SeparableElement.ExtendDerivation [section, in mathcomp.field.separable]
Separable.SeparableElement.ExtendDerivation.D [variable, in mathcomp.field.separable]
Separable.SeparableElement.ExtendDerivation.derD [variable, in mathcomp.field.separable]
Separable.SeparableElement.ExtendDerivation.DerivationLinear [section, in mathcomp.field.separable]
Separable.SeparableElement.ExtendDerivation.DerivationLinear.body [variable, in mathcomp.field.separable]
Separable.SeparableElement.ExtendDerivation.DerivationLinear.E [variable, in mathcomp.field.separable]
Separable.SeparableElement.ExtendDerivation.DerivationLinear.extendDerivationLinear [variable, in mathcomp.field.separable]
Separable.SeparableElement.ExtendDerivation.Dx [variable, in mathcomp.field.separable]
Separable.SeparableElement.K [variable, in mathcomp.field.separable]
Separable.SeparableElement.Kx_x [variable, in mathcomp.field.separable]
Separable.SeparableElement.sKxK [variable, in mathcomp.field.separable]
Separable.SeparableElement.x [variable, in mathcomp.field.separable]
seq [abbreviation, in mathcomp.ssreflect.seq]
seq [library]
SeqBseq [section, in mathcomp.ssreflect.tuple]
SeqBseq.m [variable, in mathcomp.ssreflect.tuple]
SeqBseq.n [variable, in mathcomp.ssreflect.tuple]
SeqBseq.rT [variable, in mathcomp.ssreflect.tuple]
SeqBseq.T [variable, in mathcomp.ssreflect.tuple]
SeqBseq.U [variable, in mathcomp.ssreflect.tuple]
SeqFinType [section, in mathcomp.ssreflect.fintype]
SeqFinType.s [variable, in mathcomp.ssreflect.fintype]
SeqFinType.T [variable, in mathcomp.ssreflect.fintype]
seqn [definition, in mathcomp.ssreflect.seq]
seqn_rec [definition, in mathcomp.ssreflect.seq]
seqn_type [definition, in mathcomp.ssreflect.seq]
SeqReplace [section, in mathcomp.ssreflect.fintype]
SeqReplace.T [variable, in mathcomp.ssreflect.fintype]
SeqSubType [section, in mathcomp.ssreflect.fintype]
SeqSubType.s [variable, in mathcomp.ssreflect.fintype]
SeqSubType.T [variable, in mathcomp.ssreflect.fintype]
seqs1 [lemma, in mathcomp.solvable.burnside_app]
SeqTuple [section, in mathcomp.ssreflect.tuple]
SeqTuple.m [variable, in mathcomp.ssreflect.tuple]
SeqTuple.n [variable, in mathcomp.ssreflect.tuple]
SeqTuple.rT [variable, in mathcomp.ssreflect.tuple]
SeqTuple.T [variable, in mathcomp.ssreflect.tuple]
SeqTuple.U [variable, in mathcomp.ssreflect.tuple]
Sequences [section, in mathcomp.ssreflect.seq]
Sequences.n0 [variable, in mathcomp.ssreflect.seq]
Sequences.SeqFind [section, in mathcomp.ssreflect.seq]
Sequences.SeqFind.a [variable, in mathcomp.ssreflect.seq]
Sequences.SubPred [section, in mathcomp.ssreflect.seq]
Sequences.SubPred.a1 [variable, in mathcomp.ssreflect.seq]
Sequences.SubPred.a2 [variable, in mathcomp.ssreflect.seq]
Sequences.SubPred.s12 [variable, in mathcomp.ssreflect.seq]
Sequences.T [variable, in mathcomp.ssreflect.seq]
Sequences.x0 [variable, in mathcomp.ssreflect.seq]
_ ++ _ (seq_scope) [notation, in mathcomp.ssreflect.seq]
seqv_sub_adjoin [lemma, in mathcomp.field.falgebra]
seq_tnthP [lemma, in mathcomp.ssreflect.tuple]
seq_bitseq__canonical__eqtype_Equality [definition, in mathcomp.ssreflect.seq]
seq_predType [definition, in mathcomp.ssreflect.seq]
seq_eqclass [definition, in mathcomp.ssreflect.seq]
seq_ind2 [lemma, in mathcomp.ssreflect.seq]
seq_bitseq__canonical__choice_Countable [definition, in mathcomp.ssreflect.choice]
seq_bitseq__canonical__choice_Choice [definition, in mathcomp.ssreflect.choice]
seq_hasChoice [lemma, in mathcomp.ssreflect.choice]
seq_of_optK [lemma, in mathcomp.ssreflect.choice]
seq_of_opt [definition, in mathcomp.ssreflect.choice]
seq_of_cfun [definition, in mathcomp.character.classfun]
seq_iso3_L [definition, in mathcomp.solvable.burnside_app]
seq_iso_L [definition, in mathcomp.solvable.burnside_app]
seq_subE [lemma, in mathcomp.ssreflect.fintype]
seq_sub_default [lemma, in mathcomp.ssreflect.fintype]
seq_sub_isFinite [definition, in mathcomp.ssreflect.fintype]
seq_sub_axiom [lemma, in mathcomp.ssreflect.fintype]
seq_sub_isCountable [definition, in mathcomp.ssreflect.fintype]
seq_sub_pickleK [lemma, in mathcomp.ssreflect.fintype]
seq_sub_unpickle [definition, in mathcomp.ssreflect.fintype]
seq_sub_pickle [definition, in mathcomp.ssreflect.fintype]
seq_sub_enum [definition, in mathcomp.ssreflect.fintype]
seq_sub [record, in mathcomp.ssreflect.fintype]
seq_cat__canonical__Monoid_Law [definition, in mathcomp.ssreflect.bigop]
seq_cat__canonical__SemiGroup_Law [definition, in mathcomp.ssreflect.bigop]
seq1_basis [lemma, in mathcomp.algebra.vector]
seq1_free [lemma, in mathcomp.algebra.vector]
SeriesDefs [section, in mathcomp.solvable.nilpotent]
SeriesDefs.A [variable, in mathcomp.solvable.nilpotent]
SeriesDefs.gT [variable, in mathcomp.solvable.nilpotent]
SeriesDefs.n [variable, in mathcomp.solvable.nilpotent]
series_repr [definition, in mathcomp.character.mxrepresentation]
series_sol [lemma, in mathcomp.solvable.nilpotent]
sesqui [definition, in mathcomp.algebra.sesquilinear]
sesquiE [lemma, in mathcomp.algebra.sesquilinear]
Sesquilinear [section, in mathcomp.algebra.sesquilinear]
sesquilinear [library]
sesquilinear_Hermitian__to__sesquilinear_isHermitianSesquilinear [definition, in mathcomp.algebra.spectral]
sesquilinear_Hermitian__to__sesquilinear_isBilinear [definition, in mathcomp.algebra.spectral]
sesquilinear_Bilinear__to__sesquilinear_isBilinear [definition, in mathcomp.algebra.spectral]
sesquilinear_form_of_matrix__canonical__sesquilinear_Hermitian [definition, in mathcomp.algebra.sesquilinear]
sesquilinear_form_of_matrix__canonical__sesquilinear_Bilinear [definition, in mathcomp.algebra.sesquilinear]
sesquilinear_bilinear_isBilinear__to__sesquilinear_isBilinear__70 [definition, in mathcomp.algebra.sesquilinear]
sesquilinear_form_of_matrixr__canonical__GRing_Linear [definition, in mathcomp.algebra.sesquilinear]
sesquilinear_form_of_matrixr__canonical__GRing_Additive [definition, in mathcomp.algebra.sesquilinear]
sesquilinear_form_of_matrix__canonical__GRing_Linear [definition, in mathcomp.algebra.sesquilinear]
sesquilinear_form_of_matrix__canonical__GRing_Additive [definition, in mathcomp.algebra.sesquilinear]
sesquilinear_bilinear_isBilinear__to__sesquilinear_isBilinear [definition, in mathcomp.algebra.sesquilinear]
sesquilinear_applyr_head__canonical__GRing_Linear [definition, in mathcomp.algebra.sesquilinear]
sesquilinear_applyr_head__canonical__GRing_Additive [definition, in mathcomp.algebra.sesquilinear]
sesquilinear_conjC__canonical__sesquilinear_InvolutiveRMorphism [definition, in mathcomp.algebra.sesquilinear]
sesquilinear_conjC__canonical__GRing_RMorphism [definition, in mathcomp.algebra.sesquilinear]
sesquilinear_conjC__canonical__GRing_Additive [definition, in mathcomp.algebra.sesquilinear]
Sesquilinear.Def [section, in mathcomp.algebra.sesquilinear]
Sesquilinear.Def.eps_theta [variable, in mathcomp.algebra.sesquilinear]
Sesquilinear.eps [variable, in mathcomp.algebra.sesquilinear]
Sesquilinear.M [variable, in mathcomp.algebra.sesquilinear]
Sesquilinear.M_sesqui [variable, in mathcomp.algebra.sesquilinear]
Sesquilinear.n [variable, in mathcomp.algebra.sesquilinear]
Sesquilinear.R [variable, in mathcomp.algebra.sesquilinear]
Sesquilinear.theta [variable, in mathcomp.algebra.sesquilinear]
Sesquilinear.thetaK [variable, in mathcomp.algebra.sesquilinear]
_ '_|_ _ (ring_scope) [notation, in mathcomp.algebra.sesquilinear]
_ ^_|_ (ring_scope) [notation, in mathcomp.algebra.sesquilinear]
'[ _ ] (ring_scope) [notation, in mathcomp.algebra.sesquilinear]
'[ _ , _ ] (ring_scope) [notation, in mathcomp.algebra.sesquilinear]
_ .-sesqui [notation, in mathcomp.algebra.sesquilinear]
sesquiP [lemma, in mathcomp.algebra.sesquilinear]
sesqui_keyed [definition, in mathcomp.algebra.sesquilinear]
sesqui_key [lemma, in mathcomp.algebra.sesquilinear]
setact [definition, in mathcomp.fingroup.action]
setactE [lemma, in mathcomp.fingroup.action]
setactJ [lemma, in mathcomp.fingroup.action]
setactVin [lemma, in mathcomp.fingroup.action]
setact_orbit [lemma, in mathcomp.fingroup.action]
setact_is_action [lemma, in mathcomp.fingroup.action]
setC [definition, in mathcomp.ssreflect.finset]
setCD [lemma, in mathcomp.ssreflect.finset]
setCI [lemma, in mathcomp.ssreflect.finset]
setCK [lemma, in mathcomp.ssreflect.finset]
setCP [lemma, in mathcomp.ssreflect.finset]
setCS [lemma, in mathcomp.ssreflect.finset]
setCT [lemma, in mathcomp.ssreflect.finset]
setCU [lemma, in mathcomp.ssreflect.finset]
setC_bigcap [lemma, in mathcomp.ssreflect.finset]
setC_bigcup [lemma, in mathcomp.ssreflect.finset]
setC_inj [lemma, in mathcomp.ssreflect.finset]
setC0 [lemma, in mathcomp.ssreflect.finset]
setC11 [lemma, in mathcomp.ssreflect.finset]
setD [definition, in mathcomp.ssreflect.finset]
setDDl [lemma, in mathcomp.ssreflect.finset]
setDDr [lemma, in mathcomp.ssreflect.finset]
setDE [lemma, in mathcomp.ssreflect.finset]
setDidPl [lemma, in mathcomp.ssreflect.finset]
setDIl [lemma, in mathcomp.ssreflect.finset]
setDIr [lemma, in mathcomp.ssreflect.finset]
setDP [lemma, in mathcomp.ssreflect.finset]
setDS [lemma, in mathcomp.ssreflect.finset]
setDSS [lemma, in mathcomp.ssreflect.finset]
setDT [lemma, in mathcomp.ssreflect.finset]
setDUl [lemma, in mathcomp.ssreflect.finset]
setDUr [lemma, in mathcomp.ssreflect.finset]
setDv [lemma, in mathcomp.ssreflect.finset]
setD_eq0 [lemma, in mathcomp.ssreflect.finset]
setD0 [lemma, in mathcomp.ssreflect.finset]
setD1K [lemma, in mathcomp.ssreflect.finset]
setD1P [lemma, in mathcomp.ssreflect.finset]
setD11 [lemma, in mathcomp.ssreflect.finset]
SetFixpoint [section, in mathcomp.ssreflect.finset]
SetFixpoint.Greatest [section, in mathcomp.ssreflect.finset]
SetFixpoint.Greatest.F [variable, in mathcomp.ssreflect.finset]
SetFixpoint.Greatest.F_mono [variable, in mathcomp.ssreflect.finset]
SetFixpoint.Greatest.T [variable, in mathcomp.ssreflect.finset]
SetFixpoint.Least [section, in mathcomp.ssreflect.finset]
SetFixpoint.Least.F [variable, in mathcomp.ssreflect.finset]
SetFixpoint.Least.F_mono [variable, in mathcomp.ssreflect.finset]
SetFixpoint.Least.iterF [variable, in mathcomp.ssreflect.finset]
SetFixpoint.Least.n [variable, in mathcomp.ssreflect.finset]
SetFixpoint.Least.T [variable, in mathcomp.ssreflect.finset]
setI [definition, in mathcomp.ssreflect.finset]
setIA [lemma, in mathcomp.ssreflect.finset]
setIAC [lemma, in mathcomp.ssreflect.finset]
setIACA [lemma, in mathcomp.ssreflect.finset]
setIC [lemma, in mathcomp.ssreflect.finset]
setICA [lemma, in mathcomp.ssreflect.finset]
setICr [lemma, in mathcomp.ssreflect.finset]
setID [lemma, in mathcomp.ssreflect.finset]
setIDA [lemma, in mathcomp.ssreflect.finset]
setIDAC [lemma, in mathcomp.ssreflect.finset]
setIdE [lemma, in mathcomp.ssreflect.finset]
setIdP [lemma, in mathcomp.ssreflect.finset]
setId2P [lemma, in mathcomp.ssreflect.finset]
setIg1 [lemma, in mathcomp.fingroup.fingroup]
setIid [lemma, in mathcomp.ssreflect.finset]
setIidPl [lemma, in mathcomp.ssreflect.finset]
setIidPr [lemma, in mathcomp.ssreflect.finset]
setIIl [lemma, in mathcomp.ssreflect.finset]
setIIr [lemma, in mathcomp.ssreflect.finset]
setIK [lemma, in mathcomp.ssreflect.finset]
setIP [lemma, in mathcomp.ssreflect.finset]
setIS [lemma, in mathcomp.ssreflect.finset]
setISS [lemma, in mathcomp.ssreflect.finset]
setIT [lemma, in mathcomp.ssreflect.finset]
setIUl [lemma, in mathcomp.ssreflect.finset]
setIUr [lemma, in mathcomp.ssreflect.finset]
setI_transversal_pblock [lemma, in mathcomp.ssreflect.finset]
setI_eq0 [lemma, in mathcomp.ssreflect.finset]
setI_powerset [lemma, in mathcomp.ssreflect.finset]
setI_group [definition, in mathcomp.fingroup.fingroup]
setI_normal_Hall [lemma, in mathcomp.solvable.pgroup]
setI_subnormal [lemma, in mathcomp.solvable.gseries]
setI_im_cpair [lemma, in mathcomp.solvable.center]
setI0 [lemma, in mathcomp.ssreflect.finset]
setI1g [lemma, in mathcomp.fingroup.fingroup]
setKI [lemma, in mathcomp.ssreflect.finset]
setKU [lemma, in mathcomp.ssreflect.finset]
setOps [section, in mathcomp.ssreflect.finset]
setOpsAlgebra [section, in mathcomp.ssreflect.finset]
setOpsAlgebra.T [variable, in mathcomp.ssreflect.finset]
setOpsDefs [section, in mathcomp.ssreflect.finset]
setOpsDefs.T [variable, in mathcomp.ssreflect.finset]
setOps.T [variable, in mathcomp.ssreflect.finset]
setP [lemma, in mathcomp.ssreflect.finset]
setSD [lemma, in mathcomp.ssreflect.finset]
setSI [lemma, in mathcomp.ssreflect.finset]
setSU [lemma, in mathcomp.ssreflect.finset]
setT [abbreviation, in mathcomp.ssreflect.finset]
setTD [lemma, in mathcomp.ssreflect.finset]
setTfor [definition, in mathcomp.ssreflect.finset]
setTI [lemma, in mathcomp.ssreflect.finset]
setTU [lemma, in mathcomp.ssreflect.finset]
SetType [section, in mathcomp.ssreflect.finset]
SetType.T [variable, in mathcomp.ssreflect.finset]
setT_group [definition, in mathcomp.fingroup.fingroup]
setU [definition, in mathcomp.ssreflect.finset]
setUA [lemma, in mathcomp.ssreflect.finset]
setUAC [lemma, in mathcomp.ssreflect.finset]
setUACA [lemma, in mathcomp.ssreflect.finset]
setUC [lemma, in mathcomp.ssreflect.finset]
setUCA [lemma, in mathcomp.ssreflect.finset]
setUCr [lemma, in mathcomp.ssreflect.finset]
setUid [lemma, in mathcomp.ssreflect.finset]
setUidPl [lemma, in mathcomp.ssreflect.finset]
setUidPr [lemma, in mathcomp.ssreflect.finset]
setUIl [lemma, in mathcomp.ssreflect.finset]
setUIr [lemma, in mathcomp.ssreflect.finset]
setUK [lemma, in mathcomp.ssreflect.finset]
setUP [lemma, in mathcomp.ssreflect.finset]
setUS [lemma, in mathcomp.ssreflect.finset]
setUSS [lemma, in mathcomp.ssreflect.finset]
setUT [lemma, in mathcomp.ssreflect.finset]
setUUl [lemma, in mathcomp.ssreflect.finset]
setUUr [lemma, in mathcomp.ssreflect.finset]
setU_eq0 [lemma, in mathcomp.ssreflect.finset]
setU0 [lemma, in mathcomp.ssreflect.finset]
setU1K [lemma, in mathcomp.ssreflect.finset]
setU1P [lemma, in mathcomp.ssreflect.finset]
setU1r [lemma, in mathcomp.ssreflect.finset]
setU11 [lemma, in mathcomp.ssreflect.finset]
setX [definition, in mathcomp.ssreflect.finset]
setXn [definition, in mathcomp.ssreflect.finset]
setXnP [lemma, in mathcomp.ssreflect.finset]
setXnS [lemma, in mathcomp.ssreflect.finset]
setXn_gen [lemma, in mathcomp.fingroup.gproduct]
setXn_dprod [lemma, in mathcomp.fingroup.gproduct]
setXn_prod [lemma, in mathcomp.fingroup.gproduct]
setXn_group [definition, in mathcomp.fingroup.gproduct]
setXP [lemma, in mathcomp.ssreflect.finset]
setXS [lemma, in mathcomp.ssreflect.finset]
setX_gen [lemma, in mathcomp.fingroup.gproduct]
setX_dprod [lemma, in mathcomp.fingroup.gproduct]
setX_prod [lemma, in mathcomp.fingroup.gproduct]
setX_group [definition, in mathcomp.fingroup.gproduct]
set_gring_classM_coef [lemma, in mathcomp.character.integral_char]
set_of_coset [projection, in mathcomp.fingroup.quotient]
set_nth_default [lemma, in mathcomp.ssreflect.seq]
set_nthE [lemma, in mathcomp.ssreflect.seq]
set_set_nth [lemma, in mathcomp.ssreflect.seq]
set_nth_nil [lemma, in mathcomp.ssreflect.seq]
set_nth [definition, in mathcomp.ssreflect.seq]
set_partition_big [lemma, in mathcomp.ssreflect.finset]
set_partition_big_cond [lemma, in mathcomp.ssreflect.finset]
set_cons [lemma, in mathcomp.ssreflect.finset]
set_seq1 [lemma, in mathcomp.ssreflect.finset]
set_nil [lemma, in mathcomp.ssreflect.finset]
set_enum [lemma, in mathcomp.ssreflect.finset]
set_0Vmem [lemma, in mathcomp.ssreflect.finset]
set_predType [definition, in mathcomp.ssreflect.finset]
set_isSub [definition, in mathcomp.ssreflect.finset]
set_of [definition, in mathcomp.ssreflect.finset]
set_type_sind [definition, in mathcomp.ssreflect.finset]
set_type_rec [definition, in mathcomp.ssreflect.finset]
set_type_ind [definition, in mathcomp.ssreflect.finset]
set_type_rect [definition, in mathcomp.ssreflect.finset]
set_type [inductive, in mathcomp.ssreflect.finset]
set_action [definition, in mathcomp.fingroup.action]
set_base_group [definition, in mathcomp.fingroup.fingroup]
set_invgM [lemma, in mathcomp.fingroup.fingroup]
set_invgK [lemma, in mathcomp.fingroup.fingroup]
set_mulgA [lemma, in mathcomp.fingroup.fingroup]
set_mul1g [lemma, in mathcomp.fingroup.fingroup]
set_invg [definition, in mathcomp.fingroup.fingroup]
set_mulg [definition, in mathcomp.fingroup.fingroup]
set_Frobenius_compl [lemma, in mathcomp.solvable.frobenius]
set0 [definition, in mathcomp.ssreflect.finset]
set0D [lemma, in mathcomp.ssreflect.finset]
set0I [lemma, in mathcomp.ssreflect.finset]
set0Pn [lemma, in mathcomp.ssreflect.finset]
set0U [lemma, in mathcomp.ssreflect.finset]
set1 [module, in mathcomp.ssreflect.finset]
set1gE [lemma, in mathcomp.fingroup.fingroup]
set1gP [lemma, in mathcomp.fingroup.fingroup]
set1gXn [definition, in mathcomp.fingroup.gproduct]
set1gXnE [lemma, in mathcomp.fingroup.gproduct]
set1gXnP [lemma, in mathcomp.fingroup.gproduct]
set1gXn_commute [lemma, in mathcomp.fingroup.gproduct]
set1gXn_group_set [lemma, in mathcomp.fingroup.gproduct]
set1gXn_key [lemma, in mathcomp.fingroup.gproduct]
set1P [lemma, in mathcomp.ssreflect.finset]
set1Ul [lemma, in mathcomp.ssreflect.finset]
set1Ur [lemma, in mathcomp.ssreflect.finset]
set1_inj [lemma, in mathcomp.ssreflect.finset]
set1_unlock_subterm [definition, in mathcomp.ssreflect.finset]
set1_Locked.unlock [axiom, in mathcomp.ssreflect.finset]
set1_Locked.body [axiom, in mathcomp.ssreflect.finset]
set1_Locked [module, in mathcomp.ssreflect.finset]
set1_group [definition, in mathcomp.fingroup.fingroup]
set1.body [definition, in mathcomp.ssreflect.finset]
set1.unlock [definition, in mathcomp.ssreflect.finset]
set11 [lemma, in mathcomp.ssreflect.finset]
set2P [lemma, in mathcomp.ssreflect.finset]
set21 [lemma, in mathcomp.ssreflect.finset]
set22 [lemma, in mathcomp.ssreflect.finset]
sG [abbreviation, in mathcomp.character.mxrepresentation]
sgr [abbreviation, in mathcomp.algebra.ssrint]
sgr [abbreviation, in mathcomp.algebra.rat]
sgrEz [lemma, in mathcomp.algebra.ssrint]
sgrMz [lemma, in mathcomp.algebra.ssrint]
sgrz [lemma, in mathcomp.algebra.ssrint]
sgr_numq [lemma, in mathcomp.algebra.rat]
sgr_numq_div [lemma, in mathcomp.algebra.rat]
sgr_denq [lemma, in mathcomp.algebra.rat]
sgr_scalq [lemma, in mathcomp.algebra.rat]
sgval [definition, in mathcomp.fingroup.fingroup]
sgvalK [lemma, in mathcomp.fingroup.fingroup]
sgvalM [lemma, in mathcomp.fingroup.fingroup]
sgvalmK [lemma, in mathcomp.fingroup.morphism]
sgval_sub [lemma, in mathcomp.fingroup.morphism]
sgval_morphism [definition, in mathcomp.fingroup.morphism]
sgz [definition, in mathcomp.algebra.ssrint]
Sgz [section, in mathcomp.algebra.ssrint]
sgzE [definition, in mathcomp.algebra.ssrint]
sgzM [lemma, in mathcomp.algebra.ssrint]
sgzN [lemma, in mathcomp.algebra.ssrint]
SgzNeg [constructor, in mathcomp.algebra.ssrint]
SgzNull [constructor, in mathcomp.algebra.ssrint]
sgzN1 [lemma, in mathcomp.algebra.ssrint]
sgzP [lemma, in mathcomp.algebra.ssrint]
SgzPos [constructor, in mathcomp.algebra.ssrint]
SgzReal [section, in mathcomp.algebra.ssrint]
SgzReal.R [variable, in mathcomp.algebra.ssrint]
sgzX [lemma, in mathcomp.algebra.ssrint]
sgz_lead_primitive [lemma, in mathcomp.algebra.intdiv]
sgz_contents [lemma, in mathcomp.algebra.intdiv]
sgz_eq [lemma, in mathcomp.algebra.ssrint]
sgz_smul [lemma, in mathcomp.algebra.ssrint]
sgz_le0 [lemma, in mathcomp.algebra.ssrint]
sgz_ge0 [lemma, in mathcomp.algebra.ssrint]
sgz_lt0 [lemma, in mathcomp.algebra.ssrint]
sgz_gt0 [lemma, in mathcomp.algebra.ssrint]
sgz_odd [lemma, in mathcomp.algebra.ssrint]
sgz_eq0 [lemma, in mathcomp.algebra.ssrint]
sgz_val [inductive, in mathcomp.algebra.ssrint]
sgz_cp0 [lemma, in mathcomp.algebra.ssrint]
sgz_id [lemma, in mathcomp.algebra.ssrint]
sgz_int [lemma, in mathcomp.algebra.ssrint]
sgz_sgr [lemma, in mathcomp.algebra.ssrint]
sgz_def [lemma, in mathcomp.algebra.ssrint]
Sgz.R [variable, in mathcomp.algebra.ssrint]
sgz0 [lemma, in mathcomp.algebra.ssrint]
sgz1 [lemma, in mathcomp.algebra.ssrint]
sh [definition, in mathcomp.solvable.burnside_app]
Sh [definition, in mathcomp.solvable.burnside_app]
shape [definition, in mathcomp.ssreflect.seq]
shape_rev [lemma, in mathcomp.ssreflect.seq]
shorten [definition, in mathcomp.ssreflect.path]
shortenP [lemma, in mathcomp.ssreflect.path]
ShortenSpec [constructor, in mathcomp.ssreflect.path]
shorten_spec [inductive, in mathcomp.ssreflect.path]
sh_inv [lemma, in mathcomp.solvable.burnside_app]
Sh_inj [lemma, in mathcomp.solvable.burnside_app]
signr_scalq [lemma, in mathcomp.algebra.rat]
sign_morph [definition, in mathcomp.solvable.alt]
sigW [lemma, in mathcomp.ssreflect.choice]
sig_eqW [lemma, in mathcomp.ssreflect.choice]
sig_big_dep [lemma, in mathcomp.ssreflect.bigop]
sig_big_dep_idem [lemma, in mathcomp.ssreflect.bigop]
sig2W [lemma, in mathcomp.ssreflect.choice]
sig2_eqW [lemma, in mathcomp.ssreflect.choice]
similar [abbreviation, in mathcomp.algebra.mxred]
Similarity [section, in mathcomp.algebra.mxred]
Similarity.F [variable, in mathcomp.algebra.mxred]
Similarity.Similar [section, in mathcomp.algebra.mxred]
Similarity.Similar.n [variable, in mathcomp.algebra.mxred]
similarLR [lemma, in mathcomp.algebra.mxred]
similarP [lemma, in mathcomp.algebra.mxred]
similarPp [lemma, in mathcomp.algebra.mxred]
similarRL [lemma, in mathcomp.algebra.mxred]
similarW [lemma, in mathcomp.algebra.mxred]
similar_diag_sum [lemma, in mathcomp.algebra.mxred]
similar_diag_mxminpoly [lemma, in mathcomp.algebra.mxred]
similar_diagLR [lemma, in mathcomp.algebra.mxred]
similar_diagPex [lemma, in mathcomp.algebra.mxred]
similar_diagP [lemma, in mathcomp.algebra.mxred]
similar_diagPp [lemma, in mathcomp.algebra.mxred]
similar_diag_row_base [lemma, in mathcomp.algebra.mxred]
similar_mxminpoly [lemma, in mathcomp.algebra.mxred]
similar_trig [abbreviation, in mathcomp.algebra.mxred]
similar_diag [abbreviation, in mathcomp.algebra.mxred]
similar_in_to [abbreviation, in mathcomp.algebra.mxred]
similar_in [abbreviation, in mathcomp.algebra.mxred]
similar_to [definition, in mathcomp.algebra.mxred]
Simmxity [section, in mathcomp.algebra.mxpoly]
Simmxity.F [variable, in mathcomp.algebra.mxpoly]
Simmxity.Simmx [section, in mathcomp.algebra.mxpoly]
Simmxity.Simmx.n [variable, in mathcomp.algebra.mxpoly]
simmxLR [lemma, in mathcomp.algebra.mxpoly]
simmxP [lemma, in mathcomp.algebra.mxpoly]
simmxPp [lemma, in mathcomp.algebra.mxpoly]
simmxRL [lemma, in mathcomp.algebra.mxpoly]
simmxW [lemma, in mathcomp.algebra.mxpoly]
simmx_minpoly [lemma, in mathcomp.algebra.mxpoly]
simmx_in_to [abbreviation, in mathcomp.algebra.mxpoly]
simmx_in [abbreviation, in mathcomp.algebra.mxpoly]
simmx_for [abbreviation, in mathcomp.algebra.mxpoly]
simmx_to_for [definition, in mathcomp.algebra.mxpoly]
simp [abbreviation, in mathcomp.algebra.polydiv]
simp [abbreviation, in mathcomp.algebra.matrix]
simp [abbreviation, in mathcomp.algebra.poly]
simp [abbreviation, in mathcomp.algebra.mxalgebra]
Simple [section, in mathcomp.solvable.gseries]
simple [definition, in mathcomp.solvable.gseries]
simpleP [lemma, in mathcomp.solvable.gseries]
simple_Alt5 [lemma, in mathcomp.solvable.alt]
simple_Alt5_base [lemma, in mathcomp.solvable.alt]
simple_Alt_3 [lemma, in mathcomp.solvable.alt]
simple_compsP [lemma, in mathcomp.solvable.jordanholder]
simple_Socle [lemma, in mathcomp.character.mxrepresentation]
simple_maxnormal [lemma, in mathcomp.solvable.gseries]
simple_sol_prime [lemma, in mathcomp.solvable.maximal]
simplrefl [abbreviation, in mathcomp.ssreflect.ssrAC]
size [definition, in mathcomp.ssreflect.seq]
sizeY [definition, in mathcomp.algebra.polyXY]
sizeYE [lemma, in mathcomp.algebra.polyXY]
sizeY_mulX [lemma, in mathcomp.algebra.polyXY]
sizeY_eq0 [lemma, in mathcomp.algebra.polyXY]
size_rat_int_poly [lemma, in mathcomp.algebra.intdiv]
size_zprimitive [lemma, in mathcomp.algebra.intdiv]
size_widen_bseq [lemma, in mathcomp.ssreflect.tuple]
size_cast_bseq [lemma, in mathcomp.ssreflect.tuple]
size_insub_bseq [lemma, in mathcomp.ssreflect.tuple]
size_bseq [lemma, in mathcomp.ssreflect.tuple]
size_tuple [lemma, in mathcomp.ssreflect.tuple]
size_Cyclotomic [lemma, in mathcomp.field.cyclotomic]
size_cyclotomic [lemma, in mathcomp.field.cyclotomic]
size_permutations [lemma, in mathcomp.ssreflect.seq]
size_tally_seq [lemma, in mathcomp.ssreflect.seq]
size_allpairs [lemma, in mathcomp.ssreflect.seq]
size_allpairs_dep [lemma, in mathcomp.ssreflect.seq]
size_suffix [lemma, in mathcomp.ssreflect.seq]
size_prefix [lemma, in mathcomp.ssreflect.seq]
size_infix [lemma, in mathcomp.ssreflect.seq]
size_reshape [lemma, in mathcomp.ssreflect.seq]
size_flatten [lemma, in mathcomp.ssreflect.seq]
size_zip [lemma, in mathcomp.ssreflect.seq]
size_scanl [lemma, in mathcomp.ssreflect.seq]
size_pairmap [lemma, in mathcomp.ssreflect.seq]
size_mkseq [lemma, in mathcomp.ssreflect.seq]
size_iota [lemma, in mathcomp.ssreflect.seq]
size_pmap_sub [lemma, in mathcomp.ssreflect.seq]
size_pmap [lemma, in mathcomp.ssreflect.seq]
size_map [lemma, in mathcomp.ssreflect.seq]
size_rem [lemma, in mathcomp.ssreflect.seq]
size_subseq_leqif [lemma, in mathcomp.ssreflect.seq]
size_subseq [lemma, in mathcomp.ssreflect.seq]
size_mask [lemma, in mathcomp.ssreflect.seq]
size_rotr [lemma, in mathcomp.ssreflect.seq]
size_incr_nth [lemma, in mathcomp.ssreflect.seq]
size_undup [lemma, in mathcomp.ssreflect.seq]
size_eq0 [lemma, in mathcomp.ssreflect.seq]
size_rev [lemma, in mathcomp.ssreflect.seq]
size_rot [lemma, in mathcomp.ssreflect.seq]
size_take_min [lemma, in mathcomp.ssreflect.seq]
size_take [lemma, in mathcomp.ssreflect.seq]
size_takel [lemma, in mathcomp.ssreflect.seq]
size_drop [lemma, in mathcomp.ssreflect.seq]
size_filter [lemma, in mathcomp.ssreflect.seq]
size_set_nth [lemma, in mathcomp.ssreflect.seq]
size_belast [lemma, in mathcomp.ssreflect.seq]
size_rcons [lemma, in mathcomp.ssreflect.seq]
size_cat [lemma, in mathcomp.ssreflect.seq]
size_nseq [lemma, in mathcomp.ssreflect.seq]
size_ncons [lemma, in mathcomp.ssreflect.seq]
size_behead [lemma, in mathcomp.ssreflect.seq]
size_minCpoly [lemma, in mathcomp.field.algC]
size_minPoly [lemma, in mathcomp.field.fieldext]
size_Fadjoin_poly [lemma, in mathcomp.field.fieldext]
size_mod_mxminpoly [lemma, in mathcomp.algebra.mxpoly]
size_mxminpoly [lemma, in mathcomp.algebra.mxpoly]
size_char_poly [lemma, in mathcomp.algebra.mxpoly]
size_cfclass [lemma, in mathcomp.character.inertia]
size_traject [lemma, in mathcomp.ssreflect.path]
size_sort [lemma, in mathcomp.ssreflect.path]
size_merge_sort_push [lemma, in mathcomp.ssreflect.path]
size_merge [lemma, in mathcomp.ssreflect.path]
size_poly_XmY [lemma, in mathcomp.algebra.polyXY]
size_poly_XaY [lemma, in mathcomp.algebra.polyXY]
size_abelian_type [lemma, in mathcomp.solvable.abelian]
size_orbit [lemma, in mathcomp.ssreflect.fingraph]
size_basis [lemma, in mathcomp.algebra.vector]
size_enum_ord [lemma, in mathcomp.ssreflect.fintype]
size_codom [lemma, in mathcomp.ssreflect.fintype]
size_image [lemma, in mathcomp.ssreflect.fintype]
size_map_poly [lemma, in mathcomp.algebra.poly]
size_comp_poly2 [lemma, in mathcomp.algebra.poly]
size_comp_poly [lemma, in mathcomp.algebra.poly]
size_exp [lemma, in mathcomp.algebra.poly]
size_prod_eq1 [lemma, in mathcomp.algebra.poly]
size_prod_seq_eq1 [lemma, in mathcomp.algebra.poly]
size_mul_eq1 [lemma, in mathcomp.algebra.poly]
size_prod_seq [lemma, in mathcomp.algebra.poly]
size_prod [lemma, in mathcomp.algebra.poly]
size_Cmul [lemma, in mathcomp.algebra.poly]
size_scale [lemma, in mathcomp.algebra.poly]
size_mul [lemma, in mathcomp.algebra.poly]
size_drop_poly [lemma, in mathcomp.algebra.poly]
size_take_poly [lemma, in mathcomp.algebra.poly]
size_odd_poly_eq [lemma, in mathcomp.algebra.poly]
size_odd_poly [lemma, in mathcomp.algebra.poly]
size_even_poly_eq [lemma, in mathcomp.algebra.poly]
size_even_poly [lemma, in mathcomp.algebra.poly]
size_comp_poly_leq [lemma, in mathcomp.algebra.poly]
size_map_polyC [lemma, in mathcomp.algebra.poly]
size_map_inj_poly [lemma, in mathcomp.algebra.poly]
size_map_poly_id0 [lemma, in mathcomp.algebra.poly]
size_Xn_sub_1 [lemma, in mathcomp.algebra.poly]
size_exp_XsubC [lemma, in mathcomp.algebra.poly]
size_prod_XsubC [lemma, in mathcomp.algebra.poly]
size_Mmonic [lemma, in mathcomp.algebra.poly]
size_monicM [lemma, in mathcomp.algebra.poly]
size_mulXn [lemma, in mathcomp.algebra.poly]
size_XnsubC [lemma, in mathcomp.algebra.poly]
size_XnaddC [lemma, in mathcomp.algebra.poly]
size_polyXn [lemma, in mathcomp.algebra.poly]
size_XmulC [lemma, in mathcomp.algebra.poly]
size_mulX [lemma, in mathcomp.algebra.poly]
size_MXaddC [lemma, in mathcomp.algebra.poly]
size_XaddC [lemma, in mathcomp.algebra.poly]
size_XsubC [lemma, in mathcomp.algebra.poly]
size_polyX [lemma, in mathcomp.algebra.poly]
size_scale_leq [lemma, in mathcomp.algebra.poly]
size_Msign [lemma, in mathcomp.algebra.poly]
size_opp [lemma, in mathcomp.algebra.poly]
size_exp_leq [lemma, in mathcomp.algebra.poly]
size_prod_leq [lemma, in mathcomp.algebra.poly]
size_proper_mul [lemma, in mathcomp.algebra.poly]
size_mul_leq [lemma, in mathcomp.algebra.poly]
size_poly1 [lemma, in mathcomp.algebra.poly]
size_sum [lemma, in mathcomp.algebra.poly]
size_addl [lemma, in mathcomp.algebra.poly]
size_add [lemma, in mathcomp.algebra.poly]
size_polyC_leq1 [lemma, in mathcomp.algebra.poly]
size_poly1P [lemma, in mathcomp.algebra.poly]
size_poly_gt0 [lemma, in mathcomp.algebra.poly]
size_poly_leq0P [lemma, in mathcomp.algebra.poly]
size_poly_leq0 [lemma, in mathcomp.algebra.poly]
size_poly_eq0 [lemma, in mathcomp.algebra.poly]
size_poly0 [lemma, in mathcomp.algebra.poly]
size_poly_eq [lemma, in mathcomp.algebra.poly]
size_poly [lemma, in mathcomp.algebra.poly]
size_Poly [lemma, in mathcomp.algebra.poly]
size_cons_poly [lemma, in mathcomp.algebra.poly]
size_polyC [lemma, in mathcomp.algebra.poly]
size_mk_monic [lemma, in mathcomp.algebra.qpoly]
size_mk_monic_gt0 [lemma, in mathcomp.algebra.qpoly]
size_mk_monic_gt1 [lemma, in mathcomp.algebra.qpoly]
size_lagrange [lemma, in mathcomp.algebra.qpoly]
size_lagrange_ [lemma, in mathcomp.algebra.qpoly]
size_npoly0 [lemma, in mathcomp.algebra.qpoly]
size_npoly [lemma, in mathcomp.algebra.qpoly]
size0nil [lemma, in mathcomp.ssreflect.seq]
size1_zip [lemma, in mathcomp.ssreflect.seq]
size1_polyC [lemma, in mathcomp.algebra.poly]
size2_zip [lemma, in mathcomp.ssreflect.seq]
skew [abbreviation, in mathcomp.algebra.sesquilinear]
skewmx [abbreviation, in mathcomp.algebra.sesquilinear]
skew_field_dimS [lemma, in mathcomp.field.falgebra]
skew_field_module_dimS [lemma, in mathcomp.field.falgebra]
skew_field_module_semisimple [lemma, in mathcomp.field.falgebra]
skew_field_algid1 [lemma, in mathcomp.field.falgebra]
small_nil_class [lemma, in mathcomp.solvable.sylow]
snd_morphism [definition, in mathcomp.fingroup.gproduct]
snd_morphM [lemma, in mathcomp.fingroup.gproduct]
snd_is_scalable [lemma, in mathcomp.algebra.ssralg]
snd_is_multiplicative [lemma, in mathcomp.algebra.ssralg]
snd_is_semi_additive [lemma, in mathcomp.algebra.ssralg]
soc [abbreviation, in mathcomp.character.character]
Socle [definition, in mathcomp.character.mxrepresentation]
socleP [lemma, in mathcomp.character.mxrepresentation]
socleType [record, in mathcomp.character.mxrepresentation]
socle_rsimP [lemma, in mathcomp.character.mxrepresentation]
socle_irr [lemma, in mathcomp.character.mxrepresentation]
Socle_iso [lemma, in mathcomp.character.mxrepresentation]
Socle_direct [lemma, in mathcomp.character.mxrepresentation]
Socle_semisimple [lemma, in mathcomp.character.mxrepresentation]
Socle_module [lemma, in mathcomp.character.mxrepresentation]
socle_can_subproof [lemma, in mathcomp.character.mxrepresentation]
socle_mem [lemma, in mathcomp.character.mxrepresentation]
socle_repr [definition, in mathcomp.character.mxrepresentation]
socle_module [definition, in mathcomp.character.mxrepresentation]
socle_simple [lemma, in mathcomp.character.mxrepresentation]
socle_mult [definition, in mathcomp.character.mxrepresentation]
socle_val [definition, in mathcomp.character.mxrepresentation]
socle_base [definition, in mathcomp.character.mxrepresentation]
socle_sort_sind [definition, in mathcomp.character.mxrepresentation]
socle_sort_rec [definition, in mathcomp.character.mxrepresentation]
socle_sort_ind [definition, in mathcomp.character.mxrepresentation]
socle_sort_rect [definition, in mathcomp.character.mxrepresentation]
socle_sort [inductive, in mathcomp.character.mxrepresentation]
socle_enum [definition, in mathcomp.character.mxrepresentation]
socle_exists [lemma, in mathcomp.character.mxrepresentation]
socle_base_enum [projection, in mathcomp.character.mxrepresentation]
socle_of_Iirr_bij [lemma, in mathcomp.character.character]
socle_of_IirrK [lemma, in mathcomp.character.character]
socle_Iirr0 [lemma, in mathcomp.character.character]
socle_of_Iirr [definition, in mathcomp.character.character]
Solvable [section, in mathcomp.solvable.nilpotent]
solvable [definition, in mathcomp.solvable.nilpotent]
SolvablePrimeFactor [section, in mathcomp.solvable.maximal]
SolvablePrimeFactor.G [variable, in mathcomp.solvable.maximal]
SolvablePrimeFactor.gT [variable, in mathcomp.solvable.maximal]
solvableS [lemma, in mathcomp.solvable.nilpotent]
solvable_irr_extendible_from_det [lemma, in mathcomp.character.inertia]
solvable_has_lin_char [lemma, in mathcomp.character.character]
solvable_norm_abelem [lemma, in mathcomp.solvable.maximal]
Solvable.gT [variable, in mathcomp.solvable.nilpotent]
solvable1 [lemma, in mathcomp.solvable.nilpotent]
Solver [section, in mathcomp.algebra.vector]
Solver.K [variable, in mathcomp.algebra.vector]
Solver.lhs [variable, in mathcomp.algebra.vector]
Solver.lhsf [variable, in mathcomp.algebra.vector]
Solver.n [variable, in mathcomp.algebra.vector]
Solver.rhs [variable, in mathcomp.algebra.vector]
Solver.vT [variable, in mathcomp.algebra.vector]
sol_coprime_Sylow_subset [lemma, in mathcomp.solvable.hall]
sol_coprime_Sylow_trans [lemma, in mathcomp.solvable.hall]
sol_coprime_Sylow_exists [lemma, in mathcomp.solvable.hall]
sol_prime_factor_exists [lemma, in mathcomp.solvable.maximal]
sol_der1_proper [lemma, in mathcomp.solvable.nilpotent]
SomeHall [section, in mathcomp.solvable.sylow]
SomeHall.gT [variable, in mathcomp.solvable.sylow]
some_big_AC_mk_monoid [lemma, in mathcomp.ssreflect.bigop]
sop [definition, in mathcomp.solvable.burnside_app]
sop_morph [lemma, in mathcomp.solvable.burnside_app]
sop_spec [lemma, in mathcomp.solvable.burnside_app]
sop_inj [lemma, in mathcomp.solvable.burnside_app]
sort [definition, in mathcomp.ssreflect.path]
sortE [lemma, in mathcomp.ssreflect.path]
sorted [abbreviation, in mathcomp.ssreflect.path]
sorted [abbreviation, in mathcomp.ssreflect.path]
sorted [definition, in mathcomp.ssreflect.path]
sortedP [lemma, in mathcomp.ssreflect.path]
sorted_subseq_sort_in [lemma, in mathcomp.ssreflect.path]
sorted_subseq_sort [lemma, in mathcomp.ssreflect.path]
sorted_mask_sort_in [lemma, in mathcomp.ssreflect.path]
sorted_mask_sort [lemma, in mathcomp.ssreflect.path]
sorted_sort_in [lemma, in mathcomp.ssreflect.path]
sorted_sort [lemma, in mathcomp.ssreflect.path]
sorted_merge [lemma, in mathcomp.ssreflect.path]
sorted_eq_in [lemma, in mathcomp.ssreflect.path]
sorted_uniq_in [lemma, in mathcomp.ssreflect.path]
sorted_leq_index [lemma, in mathcomp.ssreflect.path]
sorted_ltn_index [lemma, in mathcomp.ssreflect.path]
sorted_eq [lemma, in mathcomp.ssreflect.path]
sorted_uniq [lemma, in mathcomp.ssreflect.path]
sorted_leq_index_in [lemma, in mathcomp.ssreflect.path]
sorted_ltn_index_in [lemma, in mathcomp.ssreflect.path]
sorted_map [lemma, in mathcomp.ssreflect.path]
sorted_leqpoly">size_map_inj_poly [lemma, in mathcomp.algebra.poly]
]
MapPoly.Definitions.rR [ncmathcomp.algebra.ssrnumrtSlomp.algebthcomp.algebthcomp.algebthcomp.algebthcomp.algebthcomp.algebthcomp.algebthcomp.algebp.algp.algealgebp.algp.alcompml#sortlgebp.algp.alcompml#sortlgebp.algp.TMnk_IBCp.albra.mxred]
similar_diagPp [lemma, in sizp.algebrlgebra.poly.html#MapPoly.Definitions.rR">MapPoly.Definitions.rR [ncsocle_rsicompmlrsimP">socle_rsicompmlrsi>ltn_exp2l [lemma, in mathcomp.ssreflect.ssrnat]
Record Index A B Num.Theory.Pdeg2.Real.deg2_poly_gt0l [lemma, in mathcomp.algebra.sd>GRing.additive.S [variable, in mathcomp.algebra.ssralg] mat>socle_rsicompmlrsimP">socle_rsicompmlrsi>ltn_exp2l [lemma, in mathcomp.ssreflect.ois.htmler.chef="mathcomp.algebra.poly.html">> B[definition, in mathcomp.solvable.alt]
mathcogp.alohtml#Num.Ngt0l">Num.Theory.Pdeg2.Real.deg2_poly_gt0l [lemma, in mathcomp.algebra.sd>] mat>socle_rsicompmlrsimP">socle_rsicompmlrsi>ltn_exp2l [lemma, in mathcomp.algebra.sd>] mat>socle_rsicompmlrsimP">socle_rsicompmlrsi>ltn_exemma, in uNum.Ngt0l">Num.Theory.Pdeg2.Real.deg2_poly_gt0l [lemma, in mathcomp.algebra.sd> [definition, in mathcomp.algebra.archimedean]bra.html#simp">simp [abbreviation, in mathcomp.algebra.mxalgebra]skew_field_dimS [lemma, in mathcomp.field.falgebra [definition, in mathcomp.algebra.mxred]
mathcomp.fingroup.fingroup]
ef="mathcomp.algebra.mxred.html">mathcomp.algebra.mxred]
skew_field_algid1 [lemma, in mathcomp.fPntation.htmlemma,.31df[lemma,.31df[lemma,.31df[lhcomp.aomp.field.falgebra.html#skew_field_algid1">skew_field_algid1 [lemma, in mathcomp.fPntation.htmlemma,.31df[lemma,.31df[lemma,.31df[lhcomp.aomp.field.falgebra.html#skmxred<3lgesJthcomp.algesJthcomp.algesJthcomp.algesJthcesJthc.pgroup.hthcomp.al02_poly_gt0l [lemma,.31df[lemma,.31df[lemma,.31df[lemma,.31df[lemreflea,.a, in _poly_gt0l [lemma, in mathcomp.algebra.sd>] maa>]
[definition, in mathcomp.algebra.ssralg]
size_sort [lemma, in mathcomp.sscomp.algebra.vector]
passmx.passmx.hommx_comp e, in set0I [lemma, in mathcomp.algebra.ssrnum]
mathcomp.algebra.matrix]
map_tperm_mxmathcomp.algebra.matrix]
map_tperm_mxmathcomp.algebra.ssrint]
sgz0 [lemma, in matmrm_mx">map_tperm_mxsgr_denq [lemma, in mathcomp.algebra.rat]
mathcomp.algebra.polydiv]
sgval [definition, in mathcomp.fingroup.fingroup]href="math.fingroup.html#sgval">sgval [definition, in mathcomp.fingroup.fingroup]href="math.roup]href=d_sort_in">sorted_sort_in [lemma, in mathcomp.ssreflect.path]
v]href=d_v]href=d_v]href=d_v]hv]href=d__v]ooice.html#sig2Wrchimhref="mathcomomp.algn.html">ma mathcomp.algebra.vector]
ma mathcomp.algebra.vector]mathcomp.ssreflect.finset]
mathcomp.algebra.vector]
ma mamamamamamathcomp.character.mxrepresentation]
mathcomp.ssreflect.path]
Num.Theory.sqr_sqrtr [lemma, hcomp.href=lect.pathmathcomp.characdean]
Num.Theory.sqr_sqrtr [lemma, hil#sk>Num.gn.html">mamamathcomp.character.mxrepresentation]
Delgeba>]
Delgeba>]
Delgeba>]
Delgeba>]
Delgeba>]
DelgeEthcomp.character.mxrepresentation]
Delgeba>]
Delgeba>]
Delgeba>]
]href="math.fingroup.html#sgval">sgval [definition, in ]
]href="math.fingroup.html#sgval">sgval [definition, in mathcomp.character.mxrepresentation]
Socle_direc.html">mathcomp.algebra.poly]
]
Socle_direc.html">mathcomp.algebra.poly]
mathcomp.algebra.mxalgebra]
Simple [section, inharacion]] mat>socle_rsicompmlrsimP">socle_rsicompmlrsi>ltn_exp2l [lemma, in ]] mat>socle_rsicompmlrsimP">socle_rsicompmlrsi>ltn_exp2l [lemma, in 0fPICChcomp.character.mxrepresentation]
Delgeba>]
Delgeba>]
Delgeba>]
[lemma, in 0fPICChcomp.character.mxrepresentation]
Delgeba>]
Delgeba>]
]href="math.fingroup.html#sgval">sgval [definition, in mathcomp.algebra.ssralg]
snd_is_semi_additi"mathcomp.ef=d__v]compmlrsi>ltn_exp2l [lemma, in ]] mat>socle_ratml">mat>socle_ratml">mat>socle_ratml">mat>socle_ratml">mat>socle_ratml">mat>socle_ratml">mat>socle_ratml">mat>socle_ratl ]
Delgeba>]
Delgeba>]
_rsicom in 0fPICChcomp.character.mxrepresentation]
Delgeba>]
Delgeba>]
]
snd_is_semi_additi"mathcomp.ef=d__v]compmlrsi>ltn_exp2lr/8reMrbrhrer/8reMrbrhrer/8reMrbrhrer/8reelg> ]
simmx_in [abbreviation, in mathcomp.alghgebra.ssralg.html#s/> simmx_in [abbreviation, in mathcomp.alghgebra.ssralg.html#s/> simmx_inimmx_e.hall]
sol_coprime_Sylow_exists [lemma, in sol_coprime_Sylow_exists [lemma, in socle_of_IirrK [lemma, in mathcomp.character.charactf="matha>haramp.fingrobp.fif>]
snd_is_semi_additi"mathcomp.ef=d__v]compmlrsi>r__v]compmlrsi>r__v]compmlrsi>r__v]compmlrsi>r__v]compmlrsi>r__v]compmlrsi>r__v]compmlrsi>r__v]compmlrsi>r__v]compmlrthcomp0r__v]compmlrthcomp0r__v]compmlrthcomp0r__v]compmlrthcomp0r__v]compmlrthcomp0r__v]compmlrthcomp0r__v]compmlrthcomp0r__v]compmlrthcomp0r__v]csentation.html#socle_base_enum">socle_base_enum [projection, in mathcoralg.html#s/>athcomp.ssreflect<.algebra.lgebcfum">socle_base_enum [projection, in mathcoralg.html#s/>athied.html">mathcomp.algebra.mxred]
similar_diagP [lemma, in mathcom sgz_odd [lemma, in mathcomp.algebra.ssrpD>mathcomp.solvable.nilpotent]
SomeHall [section, in similar_diag_sum [lemma, in mathcomp.algebra.mcWo similar_diag_sum [lemma, in simmx_inimmx_e.hall]
Num.Theory.sqr_sqrtr [lemmasqrtr [lemmasqrtr [lemmasqrtr [lemmasqrtr [lemmasqrtr [lemmasqrtr [lemmasqrtr [lemmasqrtr [lemmasll]
mathcomp.ssreflect.path]
sorttml#sortedP">sorin mathcomp.ssreflect.path]
sorttr [lemmasqrtr [lemmasqrtr [lemmasqrtr [lemmasqrtr [lemmasqrtr [lemmasqrtr [lemmasqrtr [lemmhref="mathcomp.ssreflect.path.html">mathcomp.ssreflect.path]
sortta> [leqrtr [lemmasqrtr [lemmasll]
mathcomp.ssreflect.path]
mp.solvmathcomp.ssreflect.path]
so/> Solver.n [variable, in mathcompmathcomp.algebra.poly.html#size_poly">size_poly [lemma, in mathcomp.algebra.poly]m> [variable, in mathcompmathcomp.algebra.poly.html#size_poly">size_poly [lly.html#Qref="mathcomp.algebra.qpoly.html">mathcomp.algebra.qpoly]
polynomialmathcon <