Top

S (Global Index)

Files

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

_

Definitions

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

_

Lemmas

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

_

Abbreviations

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

_

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

_

Notations

S

S [abbrev, in mathcomp.group_representation.mxrepresentation]
s0 [def, in mathcomp.solvable.burnside_app]
S0 [def, in mathcomp.solvable.burnside_app]
s05 [def, in mathcomp.solvable.burnside_app]
S05 [def, in mathcomp.solvable.burnside_app]
S05_inj [prf, in mathcomp.solvable.burnside_app]
S05f [def, in mathcomp.solvable.burnside_app]
S0_inv [prf, in mathcomp.solvable.burnside_app]
S0f [def, in mathcomp.solvable.burnside_app]
s1 [def, in mathcomp.solvable.burnside_app]
S1 [def, in mathcomp.solvable.burnside_app]
s14 [def, in mathcomp.solvable.burnside_app]
S14 [def, in mathcomp.solvable.burnside_app]
S14_inj [prf, in mathcomp.solvable.burnside_app]
S14f [def, in mathcomp.solvable.burnside_app]
S1_inv [prf, in mathcomp.solvable.burnside_app]
S1f [def, in mathcomp.solvable.burnside_app]
s2 [def, in mathcomp.solvable.burnside_app]
S2 [def, in mathcomp.solvable.burnside_app]
s23 [def, in mathcomp.solvable.burnside_app]
S23 [def, in mathcomp.solvable.burnside_app]
s23_inv [prf, in mathcomp.solvable.burnside_app]
S23_inv [prf, in mathcomp.solvable.burnside_app]
S23f [def, in mathcomp.solvable.burnside_app]
S2_inv [prf, in mathcomp.solvable.burnside_app]
S2f [def, in mathcomp.solvable.burnside_app]
s3 [def, in mathcomp.solvable.burnside_app]
S3 [def, in mathcomp.solvable.burnside_app]
S3_inv [prf, in mathcomp.solvable.burnside_app]
S3f [def, in mathcomp.solvable.burnside_app]
s4 [def, in mathcomp.solvable.burnside_app]
S4 [def, in mathcomp.solvable.burnside_app]
S4_inv [prf, in mathcomp.solvable.burnside_app]
S4f [def, in mathcomp.solvable.burnside_app]
s5 [def, in mathcomp.solvable.burnside_app]
S5 [def, in mathcomp.solvable.burnside_app]
S5_inv [prf, in mathcomp.solvable.burnside_app]
S5f [def, in mathcomp.solvable.burnside_app]
s6 [def, in mathcomp.solvable.burnside_app]
S6 [def, in mathcomp.solvable.burnside_app]
S6_inv [prf, in mathcomp.solvable.burnside_app]
S6f [def, in mathcomp.solvable.burnside_app]
same_connect [prf, in mathcomp.boot.fingraph]
same_connect1 [prf, in mathcomp.boot.fingraph]
same_connect1r [prf, in mathcomp.boot.fingraph]
same_connect_r [prf, in mathcomp.boot.fingraph]
same_connect_rev [prf, in mathcomp.boot.fingraph]
same_fconnect1 [prf, in mathcomp.boot.fingraph]
same_fconnect1_r [prf, in mathcomp.boot.fingraph]
same_fconnect_finv [prf, in mathcomp.boot.fingraph]
same_pblock [prf, in mathcomp.boot.finset]
scalar_mx [def, in mathcomp.algebra.matrix]
scalar_mx_block [prf, in mathcomp.algebra.matrix]
scalar_mx_cent [prf, in mathcomp.algebra.mxalgebra]
scalar_mx_hom [prf, in mathcomp.group_representation.mxrepresentation]
scalar_mx_is_additive [def, in mathcomp.algebra.matrix]
scalar_mx_is_diag [prf, in mathcomp.algebra.matrix]
scalar_mx_is_monoid_morphism [prf, in mathcomp.algebra.matrix]
scalar_mx_is_multiplicative [def, in mathcomp.algebra.matrix]
scalar_mx_is_nmod_morphism [prf, in mathcomp.algebra.matrix]
scalar_mx_is_scalar [prf, in mathcomp.algebra.matrix]
scalar_mx_is_semi_additive [def, in mathcomp.algebra.matrix]
scalar_mx_is_trig [prf, in mathcomp.algebra.matrix]
scalar_mx_is_zmod_morphism [prf, in mathcomp.algebra.matrix]
scalar_mx_key [prf, in mathcomp.algebra.matrix]
scalar_mx_sum_delta [prf, in mathcomp.algebra.matrix]
scalar_mxC [prf, in mathcomp.algebra.matrix]
scalar_mxM [prf, in mathcomp.algebra.matrix]
scale0mx [prf, in mathcomp.algebra.matrix]
scale1mx [prf, in mathcomp.algebra.matrix]
scale_0poly [prf, in mathcomp.algebra.poly]
scale_1poly [prf, in mathcomp.algebra.poly]
scale_act [def, in mathcomp.group_representation.mxabelem]
scale_actE [prf, in mathcomp.group_representation.mxabelem]
scale_action [def, in mathcomp.group_representation.mxabelem]
scale_block_mx [prf, in mathcomp.algebra.matrix]
scale_col_mx [prf, in mathcomp.algebra.matrix]
scale_groupAction [def, in mathcomp.group_representation.mxabelem]
scale_is_action [prf, in mathcomp.group_representation.mxabelem]
scale_is_groupAction [prf, in mathcomp.group_representation.mxabelem]
scale_lfun [def, in mathcomp.algebra.vector]
scale_lfunE [prf, in mathcomp.algebra.vector]
scale_pair [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
scale_poly [def, in mathcomp.algebra.poly]
scale_poly_def [def, in mathcomp.algebra.poly]
scale_poly_eq0 [prf, in mathcomp.algebra.poly]
scale_poly_key [prf, in mathcomp.algebra.poly]
scale_poly_unlockable [def, in mathcomp.algebra.poly]
scale_polyA [prf, in mathcomp.algebra.poly]
scale_polyAl [prf, in mathcomp.algebra.poly]
scale_polyC [prf, in mathcomp.algebra.poly]
scale_polyDl [prf, in mathcomp.algebra.poly]
scale_polyDr [prf, in mathcomp.algebra.poly]
scale_polyE [prf, in mathcomp.algebra.poly]
scale_row_mx [prf, in mathcomp.algebra.matrix]
scale_scalar_mx [prf, in mathcomp.algebra.matrix]
scale_zchar [prf, in mathcomp.group_representation.vcharacter]
scalemx [def, in mathcomp.algebra.matrix]
scalemx1 [prf, in mathcomp.algebra.matrix]
scalemx_const [prf, in mathcomp.algebra.matrix]
scalemx_eq0 [prf, in mathcomp.algebra.matrix]
scalemx_inj [prf, in mathcomp.algebra.matrix]
scalemx_key [prf, in mathcomp.algebra.matrix]
scalemx_sub [prf, in mathcomp.algebra.mxalgebra]
scalemxA [prf, in mathcomp.algebra.matrix]
scalemxAl [prf, in mathcomp.algebra.matrix]
scalemxAr [prf, in mathcomp.algebra.matrix]
scalemxDl [prf, in mathcomp.algebra.matrix]
scalemxDr [prf, in mathcomp.algebra.matrix]
scaler_int [prf, in mathcomp.algebra.ssrint]
scalerMzl [prf, in mathcomp.algebra.ssrint]
scalerMzr [prf, in mathcomp.algebra.ssrint]
scalezrE [prf, in mathcomp.algebra.ssrint]
scalq [def, in mathcomp.algebra.rat]
scalq_def [prf, in mathcomp.algebra.rat]
scalq_eq0 [prf, in mathcomp.algebra.rat]
scalqE [prf, in mathcomp.algebra.rat]
scanl [def, in mathcomp.boot.seq]
scanl_bseq [def, in mathcomp.boot.tuple]
scanl_bseqP [prf, in mathcomp.boot.tuple]
scanl_cat [prf, in mathcomp.boot.seq]
scanl_rcons [prf, in mathcomp.boot.seq]
scanl_tuple [def, in mathcomp.boot.tuple]
scanl_tupleP [prf, in mathcomp.boot.tuple]
scanlK [prf, in mathcomp.boot.seq]
schmidt [def, in mathcomp.algebra.spectral]
schmidt_complete [def, in mathcomp.algebra.spectral]
schmidt_complete_unitarymx [prf, in mathcomp.algebra.spectral]
schmidt_sub [prf, in mathcomp.algebra.spectral]
schmidt_unitarymx [prf, in mathcomp.algebra.spectral]
Schur [prf, in mathcomp.algebra.spectral]
SchurZassenhaus_split [prf, in mathcomp.solvable.hall]
SchurZassenhaus_trans_actsol [prf, in mathcomp.solvable.hall]
SchurZassenhaus_trans_sol [prf, in mathcomp.solvable.hall]
SCN [def, in mathcomp.solvable.maximal]
SCN_abelian [prf, in mathcomp.solvable.maximal]
SCN_at [def, in mathcomp.solvable.maximal]
SCN_max [prf, in mathcomp.solvable.maximal]
SCN_P [prf, in mathcomp.solvable.maximal]
sd1 [def, in mathcomp.solvable.burnside_app]
Sd1 [def, in mathcomp.solvable.burnside_app]
Sd1_inj [prf, in mathcomp.solvable.burnside_app]
sd1_inv [prf, in mathcomp.solvable.burnside_app]
sd2 [def, in mathcomp.solvable.burnside_app]
Sd2 [def, in mathcomp.solvable.burnside_app]
Sd2_inj [prf, in mathcomp.solvable.burnside_app]
sd2_inv [prf, in mathcomp.solvable.burnside_app]
SdPair [constr, in mathcomp.finite_group.gproduct]
sdpair1 [def, in mathcomp.finite_group.gproduct]
sdpair1_morphism [def, in mathcomp.finite_group.gproduct]
sdpair1_morphM [prf, in mathcomp.finite_group.gproduct]
sdpair2 [def, in mathcomp.finite_group.gproduct]
sdpair2_morphism [def, in mathcomp.finite_group.gproduct]
sdpair2_morphM [prf, in mathcomp.finite_group.gproduct]
sdpair_act [prf, in mathcomp.finite_group.gproduct]
sdpair_setact [prf, in mathcomp.finite_group.gproduct]
sdpairE [prf, in mathcomp.finite_group.gproduct]
sdprod [abbrev, in mathcomp.finite_group.gproduct]
sdprod [abbrev, in mathcomp.finite_group.gproduct]
sdprod1g [prf, in mathcomp.finite_group.gproduct]
sdprod_by [ind, in mathcomp.finite_group.gproduct]
sdprod_by_ind [scheme, in mathcomp.finite_group.gproduct]
sdprod_by_rec [scheme, in mathcomp.finite_group.gproduct]
sdprod_by_rect [scheme, in mathcomp.finite_group.gproduct]
sdprod_by_sind [scheme, in mathcomp.finite_group.gproduct]
sdprod_card [prf, in mathcomp.finite_group.gproduct]
sdprod_cfker [prf, in mathcomp.group_representation.classfun]
sdprod_compl [prf, in mathcomp.finite_group.gproduct]
sdprod_context [prf, in mathcomp.finite_group.gproduct]
sdprod_groupType [def, in mathcomp.finite_group.gproduct]
sdprod_Hall [prf, in mathcomp.solvable.pgroup]
sdprod_Hall_p'coreP [prf, in mathcomp.solvable.pgroup]
sdprod_Hall_pcoreP [prf, in mathcomp.solvable.pgroup]
sdprod_Iirr [def, in mathcomp.group_representation.character]
sdprod_Iirr0 [prf, in mathcomp.group_representation.character]
sdprod_Iirr_eq0 [prf, in mathcomp.group_representation.character]
sdprod_Iirr_inj [prf, in mathcomp.group_representation.character]
sdprod_IirrE [prf, in mathcomp.group_representation.character]
sdprod_IirrK [prf, in mathcomp.group_representation.character]
sdprod_inv [def, in mathcomp.finite_group.gproduct]
sdprod_inv_proof [prf, in mathcomp.finite_group.gproduct]
sdprod_isog [prf, in mathcomp.finite_group.gproduct]
sdprod_isom [prf, in mathcomp.finite_group.gproduct]
sdprod_modl [prf, in mathcomp.finite_group.gproduct]
sdprod_modr [prf, in mathcomp.finite_group.gproduct]
sdprod_mul [def, in mathcomp.finite_group.gproduct]
sdprod_mul1g [prf, in mathcomp.finite_group.gproduct]
sdprod_mul_proof [prf, in mathcomp.finite_group.gproduct]
sdprod_mulgA [prf, in mathcomp.finite_group.gproduct]
sdprod_mulVg [prf, in mathcomp.finite_group.gproduct]
sdprod_normal_complP [prf, in mathcomp.finite_group.gproduct]
sdprod_normal_p'HallP [prf, in mathcomp.solvable.pgroup]
sdprod_normal_pHallP [prf, in mathcomp.solvable.pgroup]
sdprod_one [def, in mathcomp.finite_group.gproduct]
sdprod_p'core_HallP [prf, in mathcomp.solvable.pgroup]
sdprod_pcore_HallP [prf, in mathcomp.solvable.pgroup]
sdprod_recl [prf, in mathcomp.finite_group.gproduct]
sdprod_recr [prf, in mathcomp.finite_group.gproduct]
sdprod_Res_IirrE [prf, in mathcomp.group_representation.character]
sdprod_Res_IirrK [prf, in mathcomp.group_representation.character]
sdprod_sdpair [prf, in mathcomp.finite_group.gproduct]
sdprod_subr [prf, in mathcomp.finite_group.gproduct]
sdprodE [prf, in mathcomp.finite_group.gproduct]
sdprodEY [prf, in mathcomp.finite_group.gproduct]
sdprodg1 [prf, in mathcomp.finite_group.gproduct]
sdprodJ [prf, in mathcomp.finite_group.gproduct]
sdprodm [def, in mathcomp.finite_group.gproduct]
sdprodm_eqf [prf, in mathcomp.finite_group.gproduct]
sdprodm_morphism [def, in mathcomp.finite_group.gproduct]
sdprodm_norm [prf, in mathcomp.finite_group.gproduct]
sdprodm_sub [prf, in mathcomp.finite_group.gproduct]
sdprodmE [prf, in mathcomp.finite_group.gproduct]
sdprodmEl [prf, in mathcomp.finite_group.gproduct]
sdprodmEr [prf, in mathcomp.finite_group.gproduct]
sdprodP [prf, in mathcomp.finite_group.gproduct]
sdprodW [prf, in mathcomp.finite_group.gproduct]
sdprodWC [prf, in mathcomp.finite_group.gproduct]
sdprodWpp [prf, in mathcomp.finite_group.gproduct]
sdprodWY [prf, in mathcomp.finite_group.gproduct]
sdT [abbrev, in mathcomp.finite_group.gproduct]
sdval [abbrev, in mathcomp.finite_group.gproduct]
second_isog [prf, in mathcomp.finite_group.quotient]
second_isom [prf, in mathcomp.finite_group.quotient]
second_orthogonality_relation [prf, in mathcomp.group_representation.character]
section [ind, in mathcomp.solvable.jordanholder]
section_eqmx [prf, in mathcomp.group_representation.mxrepresentation]
section_eqmx_add [prf, in mathcomp.group_representation.mxrepresentation]
section_group [def, in mathcomp.solvable.jordanholder]
section_ind [scheme, in mathcomp.solvable.jordanholder]
section_isog [def, in mathcomp.solvable.jordanholder]
section_module [prf, in mathcomp.group_representation.mxrepresentation]
section_rec [scheme, in mathcomp.solvable.jordanholder]
section_rect [scheme, in mathcomp.solvable.jordanholder]
section_repr [def, in mathcomp.solvable.jordanholder]
section_repr [def, in mathcomp.group_representation.mxrepresentation]
section_repr_isog [prf, in mathcomp.solvable.jordanholder]
section_reprP [prf, in mathcomp.solvable.jordanholder]
section_sind [scheme, in mathcomp.solvable.jordanholder]
semiAlgType [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
SemiDihedral [constr, in mathcomp.solvable.extremal]
semidihedral_classP [prf, in mathcomp.solvable.extremal]
semidihedral_gtype [def, in mathcomp.solvable.extremal]
semidihedral_structure [prf, in mathcomp.solvable.extremal]
semidirect_product [def, in mathcomp.finite_group.gproduct]
Semigroup [abbrev, in mathcomp.boot.monoid]
Semigroup [mod, in mathcomp.boot.monoid]
SemiGroup [mod, in mathcomp.boot.bigop]
Semigroup.axioms_ [rec, in mathcomp.boot.monoid]
SemiGroup.Builders_1 [mod, in mathcomp.boot.bigop]
SemiGroup.Builders_1.Builders_Export_7 [mod, in mathcomp.boot.bigop]
SemiGroup.Builders_1.opA [abbrev, in mathcomp.boot.bigop]
SemiGroup.Builders_1.opC [abbrev, in mathcomp.boot.bigop]
SemiGroup.Builders_1.Super [mod, in mathcomp.boot.bigop]
Semigroup.choice_hasChoice_mixin [proj, in mathcomp.boot.monoid]
Semigroup.class [proj, in mathcomp.boot.monoid]
Semigroup.clone [abbrev, in mathcomp.boot.monoid]
SemiGroup.com_law [abbrev, in mathcomp.boot.bigop]
SemiGroup.ComLaw [abbrev, in mathcomp.boot.bigop]
SemiGroup.ComLaw [mod, in mathcomp.boot.bigop]
SemiGroup.ComLaw.axioms_ [rec, in mathcomp.boot.bigop]
SemiGroup.ComLaw.class [proj, in mathcomp.boot.bigop]
SemiGroup.ComLaw.clone [abbrev, in mathcomp.boot.bigop]
SemiGroup.ComLaw.copy [abbrev, in mathcomp.boot.bigop]
SemiGroup.ComLaw.Exports [mod, in mathcomp.boot.bigop]
SemiGroup.ComLaw.on [abbrev, in mathcomp.boot.bigop]
SemiGroup.ComLaw.on_ [abbrev, in mathcomp.boot.bigop]
SemiGroup.ComLaw.pack_ [def, in mathcomp.boot.bigop]
SemiGroup.ComLaw.phant_clone [def, in mathcomp.boot.bigop]
SemiGroup.ComLaw.phant_on_ [def, in mathcomp.boot.bigop]
SemiGroup.ComLaw.SemiGroup_isCommutativeLaw_mixin [proj, in mathcomp.boot.bigop]
SemiGroup.ComLaw.SemiGroup_isLaw_mixin [proj, in mathcomp.boot.bigop]
SemiGroup.ComLaw.sort [proj, in mathcomp.boot.bigop]
SemiGroup.ComLaw.type [rec, in mathcomp.boot.bigop]
SemiGroup.ComLawElpiOperations [mod, in mathcomp.boot.bigop]
Semigroup.copy [abbrev, in mathcomp.boot.monoid]
Semigroup.eqtype_hasDecEq_mixin [proj, in mathcomp.boot.monoid]
Semigroup.Exports [mod, in mathcomp.boot.monoid]
SemiGroup.Exports [mod, in mathcomp.boot.bigop]
Semigroup.Exports.semigroupType [abbrev, in mathcomp.boot.monoid]
SemiGroup.isComLaw [abbrev, in mathcomp.boot.bigop]
SemiGroup.isComLaw [mod, in mathcomp.boot.bigop]
SemiGroup.isComLaw.axioms [abbrev, in mathcomp.boot.bigop]
SemiGroup.isComLaw.axioms_ [rec, in mathcomp.boot.bigop]
SemiGroup.isComLaw.Build [abbrev, in mathcomp.boot.bigop]
SemiGroup.isComLaw.Exports [mod, in mathcomp.boot.bigop]
SemiGroup.isComLaw.opA [proj, in mathcomp.boot.bigop]
SemiGroup.isComLaw.opC [proj, in mathcomp.boot.bigop]
SemiGroup.isComLaw.phant_axioms [def, in mathcomp.boot.bigop]
SemiGroup.isComLaw.phant_Build [def, in mathcomp.boot.bigop]
SemiGroup.isCommutativeLaw [abbrev, in mathcomp.boot.bigop]
SemiGroup.isCommutativeLaw [mod, in mathcomp.boot.bigop]
SemiGroup.isCommutativeLaw.axioms [abbrev, in mathcomp.boot.bigop]
SemiGroup.isCommutativeLaw.axioms_ [rec, in mathcomp.boot.bigop]
SemiGroup.isCommutativeLaw.Build [abbrev, in mathcomp.boot.bigop]
SemiGroup.isCommutativeLaw.Exports [mod, in mathcomp.boot.bigop]
SemiGroup.isCommutativeLaw.identity_builder [def, in mathcomp.boot.bigop]
SemiGroup.isCommutativeLaw.opC [proj, in mathcomp.boot.bigop]
SemiGroup.isCommutativeLaw.phant_axioms [def, in mathcomp.boot.bigop]
SemiGroup.isCommutativeLaw.phant_Build [def, in mathcomp.boot.bigop]
SemiGroup.isLaw [abbrev, in mathcomp.boot.bigop]
SemiGroup.isLaw [mod, in mathcomp.boot.bigop]
SemiGroup.isLaw.axioms [abbrev, in mathcomp.boot.bigop]
SemiGroup.isLaw.axioms_ [rec, in mathcomp.boot.bigop]
SemiGroup.isLaw.Build [abbrev, in mathcomp.boot.bigop]
SemiGroup.isLaw.Exports [mod, in mathcomp.boot.bigop]
SemiGroup.isLaw.identity_builder [def, in mathcomp.boot.bigop]
SemiGroup.isLaw.opA [proj, in mathcomp.boot.bigop]
SemiGroup.isLaw.phant_axioms [def, in mathcomp.boot.bigop]
SemiGroup.isLaw.phant_Build [def, in mathcomp.boot.bigop]
SemiGroup.law [abbrev, in mathcomp.boot.bigop]
SemiGroup.Law [abbrev, in mathcomp.boot.bigop]
SemiGroup.Law [mod, in mathcomp.boot.bigop]
SemiGroup.Law.axioms_ [rec, in mathcomp.boot.bigop]
SemiGroup.Law.class [proj, in mathcomp.boot.bigop]
SemiGroup.Law.clone [abbrev, in mathcomp.boot.bigop]
SemiGroup.Law.copy [abbrev, in mathcomp.boot.bigop]
SemiGroup.Law.Exports [mod, in mathcomp.boot.bigop]
SemiGroup.Law.on [abbrev, in mathcomp.boot.bigop]
SemiGroup.Law.on_ [abbrev, in mathcomp.boot.bigop]
SemiGroup.Law.pack_ [def, in mathcomp.boot.bigop]
SemiGroup.Law.phant_clone [def, in mathcomp.boot.bigop]
SemiGroup.Law.phant_on_ [def, in mathcomp.boot.bigop]
SemiGroup.Law.SemiGroup_isLaw_mixin [proj, in mathcomp.boot.bigop]
SemiGroup.Law.sort [proj, in mathcomp.boot.bigop]
SemiGroup.Law.type [rec, in mathcomp.boot.bigop]
SemiGroup.LawElpiOperations [mod, in mathcomp.boot.bigop]
Semigroup.monoid_hasMul_mixin [proj, in mathcomp.boot.monoid]
Semigroup.monoid_Magma_isSemigroup_mixin [proj, in mathcomp.boot.monoid]
Semigroup.on [abbrev, in mathcomp.boot.monoid]
Semigroup.on_ [abbrev, in mathcomp.boot.monoid]
SemiGroup.opA [def, in mathcomp.boot.bigop]
SemiGroup.opC [def, in mathcomp.boot.bigop]
Semigroup.pack_ [def, in mathcomp.boot.monoid]
Semigroup.phant_clone [def, in mathcomp.boot.monoid]
Semigroup.phant_on_ [def, in mathcomp.boot.monoid]
Semigroup.sort [proj, in mathcomp.boot.monoid]
SemiGroup.Theory [mod, in mathcomp.boot.bigop]
SemiGroup.Theory.mulmA [prf, in mathcomp.boot.bigop]
SemiGroup.Theory.mulmAC [prf, in mathcomp.boot.bigop]
SemiGroup.Theory.mulmACA [prf, in mathcomp.boot.bigop]
SemiGroup.Theory.mulmC [prf, in mathcomp.boot.bigop]
SemiGroup.Theory.mulmCA [prf, in mathcomp.boot.bigop]
Semigroup.type [rec, in mathcomp.boot.monoid]
Semigroup_isMonoid [abbrev, in mathcomp.boot.monoid]
Semigroup_isMonoid [mod, in mathcomp.boot.monoid]
Semigroup_isMonoid.axioms [abbrev, in mathcomp.boot.monoid]
Semigroup_isMonoid.axioms_ [rec, in mathcomp.boot.monoid]
Semigroup_isMonoid.Build [abbrev, in mathcomp.boot.monoid]
Semigroup_isMonoid.Exports [mod, in mathcomp.boot.monoid]
Semigroup_isMonoid.mul1g [proj, in mathcomp.boot.monoid]
Semigroup_isMonoid.mulg1 [proj, in mathcomp.boot.monoid]
Semigroup_isMonoid.one [proj, in mathcomp.boot.monoid]
Semigroup_isMonoid.phant_axioms [def, in mathcomp.boot.monoid]
Semigroup_isMonoid.phant_Build [def, in mathcomp.boot.monoid]
SemigroupElpiOperations [mod, in mathcomp.boot.monoid]
semiprime [def, in mathcomp.solvable.frobenius]
semiprime_regular [prf, in mathcomp.solvable.frobenius]
semiprimeJ [prf, in mathcomp.solvable.frobenius]
semiprimeS [prf, in mathcomp.solvable.frobenius]
semiregular [def, in mathcomp.solvable.frobenius]
semiregular1l [prf, in mathcomp.solvable.frobenius]
semiregular1r [prf, in mathcomp.solvable.frobenius]
semiregular_prime [prf, in mathcomp.solvable.frobenius]
semiregular_sym [prf, in mathcomp.solvable.frobenius]
semiregularJ [prf, in mathcomp.solvable.frobenius]
semiregularS [prf, in mathcomp.solvable.frobenius]
semiRingType [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
semisimple_Socle [prf, in mathcomp.group_representation.mxrepresentation]
SemiVector [abbrev, in mathcomp.algebra.vector]
SemiVector [mod, in mathcomp.algebra.vector]
SemiVector.Algebra_AddMagma_isAddSemigroup_mixin [proj, in mathcomp.algebra.vector]
SemiVector.Algebra_BaseAddMagma_isAddMagma_mixin [proj, in mathcomp.algebra.vector]
SemiVector.Algebra_BaseAddUMagma_isAddUMagma_mixin [proj, in mathcomp.algebra.vector]
SemiVector.Algebra_hasAdd_mixin [proj, in mathcomp.algebra.vector]
SemiVector.Algebra_hasZero_mixin [proj, in mathcomp.algebra.vector]
SemiVector.axioms_ [rec, in mathcomp.algebra.vector]
SemiVector.choice_hasChoice_mixin [proj, in mathcomp.algebra.vector]
SemiVector.class [proj, in mathcomp.algebra.vector]
SemiVector.clone [abbrev, in mathcomp.algebra.vector]
SemiVector.copy [abbrev, in mathcomp.algebra.vector]
SemiVector.eqtype_hasDecEq_mixin [proj, in mathcomp.algebra.vector]
SemiVector.Exports [mod, in mathcomp.algebra.vector]
SemiVector.Exports.semiVectType [abbrev, in mathcomp.algebra.vector]
SemiVector.GRing_Nmodule_isLSemiModule_mixin [proj, in mathcomp.algebra.vector]
SemiVector.on [abbrev, in mathcomp.algebra.vector]
SemiVector.on_ [abbrev, in mathcomp.algebra.vector]
SemiVector.pack_ [def, in mathcomp.algebra.vector]
SemiVector.phant_clone [def, in mathcomp.algebra.vector]
SemiVector.phant_on_ [def, in mathcomp.algebra.vector]
SemiVector.sort [proj, in mathcomp.algebra.vector]
SemiVector.type [rec, in mathcomp.algebra.vector]
SemiVector.vector_LSemiModule_hasFinDim_mixin [proj, in mathcomp.algebra.vector]
semivector_axiom_def [rec, in mathcomp.algebra.vector]
SemiVector_isProper [abbrev, in mathcomp.algebra.vector]
SemiVector_isProper [mod, in mathcomp.algebra.vector]
SemiVector_isProper.axioms [abbrev, in mathcomp.algebra.vector]
SemiVector_isProper.axioms_ [rec, in mathcomp.algebra.vector]
SemiVector_isProper.Build [abbrev, in mathcomp.algebra.vector]
SemiVector_isProper.dim_gt0 [proj, in mathcomp.algebra.vector]
SemiVector_isProper.Exports [mod, in mathcomp.algebra.vector]
SemiVector_isProper.identity_builder [def, in mathcomp.algebra.vector]
SemiVector_isProper.phant_axioms [def, in mathcomp.algebra.vector]
SemiVector_isProper.phant_Build [def, in mathcomp.algebra.vector]
SemiVectorElpiOperations [mod, in mathcomp.algebra.vector]
separable [file, in mathcomp.field.separable]
separable [def, in mathcomp.field.separable]
separable [abbrev, in mathcomp.field.separable]
separable_add [prf, in mathcomp.field.separable]
separable_coprime [prf, in mathcomp.field.separable]
separable_deriv_eq0 [prf, in mathcomp.field.separable]
separable_element [def, in mathcomp.field.separable]
separable_elementP [prf, in mathcomp.field.separable]
separable_elementS [prf, in mathcomp.field.separable]
separable_exponent [abbrev, in mathcomp.field.separable]
separable_exponent_pchar [prf, in mathcomp.field.separable]
separable_Fadjoin_seq [prf, in mathcomp.field.separable]
separable_generator [def, in mathcomp.field.separable]
separable_generator_maximal [prf, in mathcomp.field.separable]
separable_generator_mem [prf, in mathcomp.field.separable]
separable_generatorP [prf, in mathcomp.field.separable]
separable_inseparable_decomposition [prf, in mathcomp.field.separable]
separable_inseparable_element [prf, in mathcomp.field.separable]
separable_map [prf, in mathcomp.field.separable]
separable_mul [prf, in mathcomp.field.separable]
separable_nosquare [prf, in mathcomp.field.separable]
separable_nz_der [prf, in mathcomp.field.separable]
separable_poly [abbrev, in mathcomp.field.separable]
separable_poly [mod, in mathcomp.field.separable]
separable_poly.body [def, in mathcomp.field.separable]
separable_poly.unlock [def, in mathcomp.field.separable]
separable_poly_Locked [modtype, in mathcomp.field.separable]
separable_poly_Locked.body [ax, in mathcomp.field.separable]
separable_poly_Locked.unlock [ax, in mathcomp.field.separable]
separable_poly_neq0 [prf, in mathcomp.field.separable]
separable_poly_unlock_subterm [def, in mathcomp.field.separable]
separable_poly_unlockable [def, in mathcomp.field.separable]
separable_polyP [prf, in mathcomp.field.separable]
separable_prod_XsubC [prf, in mathcomp.field.separable]
separable_refl [prf, in mathcomp.field.separable]
separable_root [prf, in mathcomp.field.separable]
separable_root_der [prf, in mathcomp.field.separable]
separable_sum [prf, in mathcomp.field.separable]
separable_trans [prf, in mathcomp.field.separable]
separable_Xn_sub_1 [prf, in mathcomp.field.cyclotomic]
separableP [prf, in mathcomp.field.separable]
separablePn [abbrev, in mathcomp.field.separable]
separablePn_pchar [prf, in mathcomp.field.separable]
separableS [prf, in mathcomp.field.separable]
separableSl [prf, in mathcomp.field.separable]
separableSr [prf, in mathcomp.field.separable]
seq [file, in mathcomp.boot.seq]
seq [abbrev, in mathcomp.boot.seq]
seq1_basis [prf, in mathcomp.algebra.vector]
seq1_free [prf, in mathcomp.algebra.vector]
seq_eqclass [def, in mathcomp.boot.seq]
seq_hasChoice [prf, in mathcomp.boot.choice]
seq_ind2 [prf, in mathcomp.boot.seq]
seq_iso3_L [def, in mathcomp.solvable.burnside_app]
seq_iso_L [def, in mathcomp.solvable.burnside_app]
seq_of_cfun [def, in mathcomp.group_representation.classfun]
seq_of_opt [def, in mathcomp.boot.choice]
seq_of_optK [prf, in mathcomp.boot.choice]
seq_predType [def, in mathcomp.boot.seq]
seq_sub [rec, in mathcomp.boot.fintype]
seq_sub_axiom [prf, in mathcomp.boot.fintype]
seq_sub_default [prf, in mathcomp.boot.fintype]
seq_sub_enum [def, in mathcomp.boot.fintype]
seq_sub_isCountable [def, in mathcomp.boot.fintype]
seq_sub_isFinite [def, in mathcomp.boot.fintype]
seq_sub_pickle [def, in mathcomp.boot.fintype]
seq_sub_pickleK [prf, in mathcomp.boot.fintype]
seq_sub_unpickle [def, in mathcomp.boot.fintype]
seq_subE [prf, in mathcomp.boot.fintype]
seq_tnthP [prf, in mathcomp.boot.tuple]
seqn [def, in mathcomp.boot.seq]
seqn_rec [def, in mathcomp.boot.seq]
seqn_type [def, in mathcomp.boot.seq]
seqs1 [prf, in mathcomp.solvable.burnside_app]
seqv_sub_adjoin [prf, in mathcomp.field.falgebra]
series_repr [def, in mathcomp.group_representation.mxrepresentation]
series_sol [prf, in mathcomp.solvable.nilpotent]
sesqui [def, in mathcomp.algebra.sesquilinear]
sesqui_key [prf, in mathcomp.algebra.sesquilinear]
sesqui_keyed [def, in mathcomp.algebra.sesquilinear]
sesquiE [prf, in mathcomp.algebra.sesquilinear]
sesquilinear [file, in mathcomp.algebra.sesquilinear]
sesquiP [prf, in mathcomp.algebra.sesquilinear]
set0 [def, in mathcomp.boot.finset]
set0_Nexists [prf, in mathcomp.boot.finset]
set0D [prf, in mathcomp.boot.finset]
set0I [prf, in mathcomp.boot.finset]
set0Pn [prf, in mathcomp.boot.finset]
set0U [prf, in mathcomp.boot.finset]
set1 [abbrev, in mathcomp.boot.finset]
set1 [mod, in mathcomp.boot.finset]
set1.body [def, in mathcomp.boot.finset]
set1.unlock [def, in mathcomp.boot.finset]
set11 [prf, in mathcomp.boot.finset]
set1_group [def, in mathcomp.finite_group.fingroup]
set1_inj [prf, in mathcomp.boot.finset]
set1_Locked [modtype, in mathcomp.boot.finset]
set1_Locked.body [ax, in mathcomp.boot.finset]
set1_Locked.unlock [ax, in mathcomp.boot.finset]
set1_unlock_subterm [def, in mathcomp.boot.finset]
set1gE [prf, in mathcomp.finite_group.fingroup]
set1gP [prf, in mathcomp.finite_group.fingroup]
set1gXn [def, in mathcomp.finite_group.gproduct]
set1gXn_commute [prf, in mathcomp.finite_group.gproduct]
set1gXn_group_set [prf, in mathcomp.finite_group.gproduct]
set1gXn_key [prf, in mathcomp.finite_group.gproduct]
set1gXnE [prf, in mathcomp.finite_group.gproduct]
set1gXnP [prf, in mathcomp.finite_group.gproduct]
set1K [prf, in mathcomp.boot.finset]
set1P [prf, in mathcomp.boot.finset]
set1Ul [prf, in mathcomp.boot.finset]
set1Ur [prf, in mathcomp.boot.finset]
set21 [prf, in mathcomp.boot.finset]
set22 [prf, in mathcomp.boot.finset]
set2P [prf, in mathcomp.boot.finset]
set_0Vmem [prf, in mathcomp.boot.finset]
set_action [def, in mathcomp.finite_group.action]
set_base_group [def, in mathcomp.finite_group.fingroup]
set_cons [prf, in mathcomp.boot.finset]
set_enum [prf, in mathcomp.boot.finset]
set_Frobenius_compl [prf, in mathcomp.solvable.frobenius]
set_gring_classM_coef [prf, in mathcomp.group_representation.integral_char]
set_invg [def, in mathcomp.finite_group.fingroup]
set_invgK [prf, in mathcomp.finite_group.fingroup]
set_invgM [prf, in mathcomp.finite_group.fingroup]
set_isSub [def, in mathcomp.boot.finset]
set_last_default [prf, in mathcomp.boot.seq]
set_mul1g [prf, in mathcomp.finite_group.fingroup]
set_mulg [def, in mathcomp.finite_group.fingroup]
set_mulgA [prf, in mathcomp.finite_group.fingroup]
set_nil [prf, in mathcomp.boot.finset]
set_nth [def, in mathcomp.boot.seq]
set_nth_default [prf, in mathcomp.boot.seq]
set_nth_nil [prf, in mathcomp.boot.seq]
set_nthE [prf, in mathcomp.boot.seq]
set_of [def, in mathcomp.boot.finset]
set_of_coset [proj, in mathcomp.finite_group.quotient]
set_partition_big [prf, in mathcomp.boot.finset]
set_partition_big_cond [prf, in mathcomp.boot.finset]
set_predType [def, in mathcomp.boot.finset]
set_seq1 [prf, in mathcomp.boot.finset]
set_set_nth [prf, in mathcomp.boot.seq]
set_type [ind, in mathcomp.boot.finset]
set_type_ind [scheme, in mathcomp.boot.finset]
set_type_rec [scheme, in mathcomp.boot.finset]
set_type_rect [scheme, in mathcomp.boot.finset]
set_type_sind [scheme, in mathcomp.boot.finset]
setact [def, in mathcomp.finite_group.action]
setact_is_action [prf, in mathcomp.finite_group.action]
setact_orbit [prf, in mathcomp.finite_group.action]
setactE [prf, in mathcomp.finite_group.action]
setactJ [prf, in mathcomp.finite_group.action]
setactVin [prf, in mathcomp.finite_group.action]
setC [def, in mathcomp.boot.finset]
setC0 [prf, in mathcomp.boot.finset]
setC11 [prf, in mathcomp.boot.finset]
setC_bigcap [prf, in mathcomp.boot.finset]
setC_bigcup [prf, in mathcomp.boot.finset]
setC_inj [prf, in mathcomp.boot.finset]
setCD [prf, in mathcomp.boot.finset]
setCI [prf, in mathcomp.boot.finset]
setCK [prf, in mathcomp.boot.finset]
setCP [prf, in mathcomp.boot.finset]
setCS [prf, in mathcomp.boot.finset]
setCT [prf, in mathcomp.boot.finset]
setCU [prf, in mathcomp.boot.finset]
setD [def, in mathcomp.boot.finset]
setD0 [prf, in mathcomp.boot.finset]
setD11 [prf, in mathcomp.boot.finset]
setD1K [prf, in mathcomp.boot.finset]
setD1P [prf, in mathcomp.boot.finset]
setD_eq0 [prf, in mathcomp.boot.finset]
setDDl [prf, in mathcomp.boot.finset]
setDDr [prf, in mathcomp.boot.finset]
setDE [prf, in mathcomp.boot.finset]
setDidPl [prf, in mathcomp.boot.finset]
setDIl [prf, in mathcomp.boot.finset]
setDIr [prf, in mathcomp.boot.finset]
setDP [prf, in mathcomp.boot.finset]
setDS [prf, in mathcomp.boot.finset]
setDSS [prf, in mathcomp.boot.finset]
setDT [prf, in mathcomp.boot.finset]
setDUl [prf, in mathcomp.boot.finset]
setDUr [prf, in mathcomp.boot.finset]
setDv [prf, in mathcomp.boot.finset]
setI [def, in mathcomp.boot.finset]
setI0 [prf, in mathcomp.boot.finset]
setI1g [prf, in mathcomp.finite_group.fingroup]
setI_eq0 [prf, in mathcomp.boot.finset]
setI_group [def, in mathcomp.finite_group.fingroup]
setI_im_cpair [prf, in mathcomp.solvable.center]
setI_normal_Hall [prf, in mathcomp.solvable.pgroup]
setI_powerset [prf, in mathcomp.boot.finset]
setI_subnormal [prf, in mathcomp.solvable.gseries]
setI_transversal_pblock [prf, in mathcomp.boot.finset]
setIA [prf, in mathcomp.boot.finset]
setIAC [prf, in mathcomp.boot.finset]
setIACA [prf, in mathcomp.boot.finset]
setIC [prf, in mathcomp.boot.finset]
setICA [prf, in mathcomp.boot.finset]
setICr [prf, in mathcomp.boot.finset]
setID [prf, in mathcomp.boot.finset]
setId2P [prf, in mathcomp.boot.finset]
setIDA [prf, in mathcomp.boot.finset]
setIDAC [prf, in mathcomp.boot.finset]
setIdE [prf, in mathcomp.boot.finset]
setIdP [prf, in mathcomp.boot.finset]
setIg1 [prf, in mathcomp.finite_group.fingroup]
setIid [prf, in mathcomp.boot.finset]
setIidPl [prf, in mathcomp.boot.finset]
setIidPr [prf, in mathcomp.boot.finset]
setIIl [prf, in mathcomp.boot.finset]
setIIr [prf, in mathcomp.boot.finset]
setIK [prf, in mathcomp.boot.finset]
setIP [prf, in mathcomp.boot.finset]
setIS [prf, in mathcomp.boot.finset]
setISS [prf, in mathcomp.boot.finset]
setIT [prf, in mathcomp.boot.finset]
setIUl [prf, in mathcomp.boot.finset]
setIUr [prf, in mathcomp.boot.finset]
setKI [prf, in mathcomp.boot.finset]
setKU [prf, in mathcomp.boot.finset]
setP [prf, in mathcomp.boot.finset]
setSD [prf, in mathcomp.boot.finset]
setSI [prf, in mathcomp.boot.finset]
setSU [prf, in mathcomp.boot.finset]
setT [abbrev, in mathcomp.boot.finset]
setT_group [def, in mathcomp.finite_group.fingroup]
setTD [prf, in mathcomp.boot.finset]
setTfor [def, in mathcomp.boot.finset]
setTI [prf, in mathcomp.boot.finset]
setTU [prf, in mathcomp.boot.finset]
setU [def, in mathcomp.boot.finset]
setU0 [prf, in mathcomp.boot.finset]
setU11 [prf, in mathcomp.boot.finset]
setU1K [prf, in mathcomp.boot.finset]
setU1P [prf, in mathcomp.boot.finset]
setU1r [prf, in mathcomp.boot.finset]
setU_eq0 [prf, in mathcomp.boot.finset]
setUA [prf, in mathcomp.boot.finset]
setUAC [prf, in mathcomp.boot.finset]
setUACA [prf, in mathcomp.boot.finset]
setUC [prf, in mathcomp.boot.finset]
setUCA [prf, in mathcomp.boot.finset]
setUCr [prf, in mathcomp.boot.finset]
setUD [prf, in mathcomp.boot.finset]
setUDl [prf, in mathcomp.boot.finset]
setUid [prf, in mathcomp.boot.finset]
setUidPl [prf, in mathcomp.boot.finset]
setUidPr [prf, in mathcomp.boot.finset]
setUIl [prf, in mathcomp.boot.finset]
setUIr [prf, in mathcomp.boot.finset]
setUK [prf, in mathcomp.boot.finset]
setUP [prf, in mathcomp.boot.finset]
setUS [prf, in mathcomp.boot.finset]
setUSS [prf, in mathcomp.boot.finset]
setUT [prf, in mathcomp.boot.finset]
setUUl [prf, in mathcomp.boot.finset]
setUUr [prf, in mathcomp.boot.finset]
setX [def, in mathcomp.boot.finset]
setX_dprod [prf, in mathcomp.finite_group.gproduct]
setX_gen [prf, in mathcomp.finite_group.gproduct]
setX_group [def, in mathcomp.finite_group.gproduct]
setX_prod [prf, in mathcomp.finite_group.gproduct]
setXn [def, in mathcomp.boot.finset]
setXn_dprod [prf, in mathcomp.finite_group.gproduct]
setXn_gen [prf, in mathcomp.finite_group.gproduct]
setXn_group [def, in mathcomp.finite_group.gproduct]
setXn_prod [prf, in mathcomp.finite_group.gproduct]
setXn_sol [prf, in mathcomp.solvable.nilpotent]
setXnP [prf, in mathcomp.boot.finset]
setXnS [prf, in mathcomp.boot.finset]
setXP [prf, in mathcomp.boot.finset]
setXS [prf, in mathcomp.boot.finset]
sG [abbrev, in mathcomp.group_representation.mxrepresentation]
sgr [abbrev, in mathcomp.algebra.ssrint]
sgr [abbrev, in mathcomp.algebra.rat]
sgr_denq [prf, in mathcomp.algebra.rat]
sgr_numq [prf, in mathcomp.algebra.rat]
sgr_numq_div [prf, in mathcomp.algebra.rat]
sgr_scalq [prf, in mathcomp.algebra.rat]
sgrEz [prf, in mathcomp.algebra.ssrint]
sgrMz [prf, in mathcomp.algebra.ssrint]
sgrz [prf, in mathcomp.algebra.ssrint]
sgval [def, in mathcomp.finite_group.fingroup]
sgval_morphism [def, in mathcomp.finite_group.morphism]
sgval_sub [prf, in mathcomp.finite_group.morphism]
sgvalK [prf, in mathcomp.finite_group.fingroup]
sgvalM [prf, in mathcomp.finite_group.fingroup]
sgvalmK [prf, in mathcomp.finite_group.morphism]
sgz [def, in mathcomp.algebra.ssrint]
sgz0 [prf, in mathcomp.algebra.ssrint]
sgz1 [prf, in mathcomp.algebra.ssrint]
sgz_contents [prf, in mathcomp.algebra.intdiv]
sgz_cp0 [prf, in mathcomp.algebra.ssrint]
sgz_def [prf, in mathcomp.algebra.ssrint]
sgz_eq [prf, in mathcomp.algebra.ssrint]
sgz_eq0 [prf, in mathcomp.algebra.ssrint]
sgz_ge0 [prf, in mathcomp.algebra.ssrint]
sgz_gt0 [prf, in mathcomp.algebra.ssrint]
sgz_id [prf, in mathcomp.algebra.ssrint]
sgz_int [prf, in mathcomp.algebra.ssrint]
sgz_le0 [prf, in mathcomp.algebra.ssrint]
sgz_lead_primitive [prf, in mathcomp.algebra.intdiv]
sgz_lt0 [prf, in mathcomp.algebra.ssrint]
sgz_odd [prf, in mathcomp.algebra.ssrint]
sgz_sgr [prf, in mathcomp.algebra.ssrint]
sgz_smul [prf, in mathcomp.algebra.ssrint]
sgz_val [ind, in mathcomp.algebra.ssrint]
sgzE [def, in mathcomp.algebra.ssrint]
sgzM [prf, in mathcomp.algebra.ssrint]
sgzN [prf, in mathcomp.algebra.ssrint]
sgzN1 [prf, in mathcomp.algebra.ssrint]
SgzNeg [constr, in mathcomp.algebra.ssrint]
SgzNull [constr, in mathcomp.algebra.ssrint]
sgzP [prf, in mathcomp.algebra.ssrint]
SgzPos [constr, in mathcomp.algebra.ssrint]
sgzX [prf, in mathcomp.algebra.ssrint]
sh [def, in mathcomp.solvable.burnside_app]
Sh [def, in mathcomp.solvable.burnside_app]
Sh_inj [prf, in mathcomp.solvable.burnside_app]
sh_inv [prf, in mathcomp.solvable.burnside_app]
shape [def, in mathcomp.boot.seq]
shape_rev [prf, in mathcomp.boot.seq]
shorten [def, in mathcomp.boot.path]
shorten_spec [ind, in mathcomp.boot.path]
shortenP [prf, in mathcomp.boot.path]
ShortenSpec [constr, in mathcomp.boot.path]
sig2_eqW [prf, in mathcomp.boot.choice]
sig2W [prf, in mathcomp.boot.choice]
sig_big_dep [prf, in mathcomp.boot.bigop]
sig_big_dep_idem [prf, in mathcomp.boot.bigop]
sig_eq2W [prf, in mathcomp.boot.choice]
sig_eqW [prf, in mathcomp.boot.choice]
sign_morph [def, in mathcomp.solvable.alt]
signr_scalq [prf, in mathcomp.algebra.rat]
sigW [prf, in mathcomp.boot.choice]
similar [abbrev, in mathcomp.algebra.mxred]
similar_diag [abbrev, in mathcomp.algebra.mxred]
similar_diag_mxminpoly [prf, in mathcomp.algebra.mxred]
similar_diag_row_base [prf, in mathcomp.algebra.mxred]
similar_diag_sum [prf, in mathcomp.algebra.mxred]
similar_diagLR [prf, in mathcomp.algebra.mxred]
similar_diagP [prf, in mathcomp.algebra.mxred]
similar_diagPex [prf, in mathcomp.algebra.mxred]
similar_diagPp [prf, in mathcomp.algebra.mxred]
similar_in [abbrev, in mathcomp.algebra.mxred]
similar_in_to [abbrev, in mathcomp.algebra.mxred]
similar_mxminpoly [prf, in mathcomp.algebra.mxred]
similar_to [def, in mathcomp.algebra.mxred]
similar_trig [abbrev, in mathcomp.algebra.mxred]
similarLR [prf, in mathcomp.algebra.mxred]
similarP [prf, in mathcomp.algebra.mxred]
similarPp [prf, in mathcomp.algebra.mxred]
similarRL [prf, in mathcomp.algebra.mxred]
similarW [prf, in mathcomp.algebra.mxred]
simmx_for [abbrev, in mathcomp.algebra.mxpoly]
simmx_in [abbrev, in mathcomp.algebra.mxpoly]
simmx_in_to [abbrev, in mathcomp.algebra.mxpoly]
simmx_minpoly [prf, in mathcomp.algebra.mxpoly]
simmx_to_for [def, in mathcomp.algebra.mxpoly]
simmxLR [prf, in mathcomp.algebra.mxpoly]
simmxP [prf, in mathcomp.algebra.mxpoly]
simmxPp [prf, in mathcomp.algebra.mxpoly]
simmxRL [prf, in mathcomp.algebra.mxpoly]
simmxW [prf, in mathcomp.algebra.mxpoly]
simp [abbrev, in mathcomp.algebra.polydiv]
simp [abbrev, in mathcomp.algebra.poly]
simp [abbrev, in mathcomp.algebra.mxalgebra]
simp [abbrev, in mathcomp.algebra.matrix]
simple [def, in mathcomp.solvable.gseries]
simple_Alt5 [prf, in mathcomp.solvable.alt]
simple_Alt5_base [prf, in mathcomp.solvable.alt]
simple_Alt_3 [prf, in mathcomp.solvable.alt]
simple_compsP [prf, in mathcomp.solvable.jordanholder]
simple_maxnormal [prf, in mathcomp.solvable.gseries]
simple_Socle [prf, in mathcomp.group_representation.mxrepresentation]
simple_sol_prime [prf, in mathcomp.solvable.maximal]
simpleP [prf, in mathcomp.solvable.gseries]
simplrefl [abbrev, in mathcomp.boot.ssrAC]
size [def, in mathcomp.boot.seq]
size0nil [prf, in mathcomp.boot.seq]
size1_polyC [prf, in mathcomp.algebra.poly]
size1_zip [prf, in mathcomp.boot.seq]
size2_zip [prf, in mathcomp.boot.seq]
size_abelian_type [prf, in mathcomp.solvable.abelian]
size_add [abbrev, in mathcomp.algebra.poly]
size_addl [abbrev, in mathcomp.algebra.poly]
size_algC_pfactor [prf, in mathcomp.field.algC]
size_algR_pfactor [prf, in mathcomp.field.algC]
size_allpairs [prf, in mathcomp.boot.seq]
size_allpairs_dep [prf, in mathcomp.boot.seq]
size_basis [prf, in mathcomp.algebra.vector]
size_behead [prf, in mathcomp.boot.seq]
size_belast [prf, in mathcomp.boot.seq]
size_bseq [prf, in mathcomp.boot.tuple]
size_cast_bseq [prf, in mathcomp.boot.tuple]
size_cat [prf, in mathcomp.boot.seq]
size_cfclass [prf, in mathcomp.group_representation.inertia]
size_char_poly [prf, in mathcomp.algebra.mxpoly]
size_Cmul [prf, in mathcomp.algebra.poly]
size_codom [prf, in mathcomp.boot.fintype]
size_comp_poly [prf, in mathcomp.algebra.poly]
size_comp_poly2 [prf, in mathcomp.algebra.poly]
size_comp_poly_leq [prf, in mathcomp.algebra.poly]
size_cons_poly [prf, in mathcomp.algebra.poly]
size_Cyclotomic [prf, in mathcomp.field.cyclotomic]
size_cyclotomic [prf, in mathcomp.field.cyclotomic]
size_drop [prf, in mathcomp.boot.seq]
size_drop_poly [prf, in mathcomp.algebra.poly]
size_enum_ord [prf, in mathcomp.boot.fintype]
size_eq0 [prf, in mathcomp.boot.seq]
size_even_poly [prf, in mathcomp.algebra.poly]
size_even_poly_eq [prf, in mathcomp.algebra.poly]
size_exp [prf, in mathcomp.algebra.poly]
size_exp_leq [abbrev, in mathcomp.algebra.poly]
size_exp_XsubC [prf, in mathcomp.algebra.poly]
size_Fadjoin_poly [prf, in mathcomp.field.fieldext]
size_filter [prf, in mathcomp.boot.seq]
size_filter_gt0 [prf, in mathcomp.boot.seq]
size_flatten [prf, in mathcomp.boot.seq]
size_image [prf, in mathcomp.boot.fintype]
size_incr_nth [prf, in mathcomp.boot.seq]
size_infix [prf, in mathcomp.boot.seq]
size_insub_bseq [prf, in mathcomp.boot.tuple]
size_iota [prf, in mathcomp.boot.seq]
size_lagrange [prf, in mathcomp.algebra.qpoly]
size_lagrange_ [prf, in mathcomp.algebra.qpoly]
size_map [prf, in mathcomp.boot.seq]
size_map_inj_poly [prf, in mathcomp.algebra.poly]
size_map_poly [prf, in mathcomp.algebra.poly]
size_map_poly_id0 [prf, in mathcomp.algebra.poly]
size_map_polyC [prf, in mathcomp.algebra.poly]
size_mask [prf, in mathcomp.boot.seq]
size_merge [prf, in mathcomp.boot.path]
size_merge_sort_push [prf, in mathcomp.boot.path]
size_minCpoly [prf, in mathcomp.field.algC]
size_minPoly [prf, in mathcomp.field.fieldext]
size_mk_monic [prf, in mathcomp.algebra.qpoly]
size_mk_monic_gt0 [prf, in mathcomp.algebra.qpoly]
size_mk_monic_gt1 [prf, in mathcomp.algebra.qpoly]
size_mkseq [prf, in mathcomp.boot.seq]
size_Mmonic [prf, in mathcomp.algebra.poly]
size_mod_mxminpoly [prf, in mathcomp.algebra.mxpoly]
size_monicM [prf, in mathcomp.algebra.poly]
size_Msign [prf, in mathcomp.algebra.poly]
size_mul [prf, in mathcomp.algebra.poly]
size_mul_eq1 [prf, in mathcomp.algebra.poly]
size_mul_leq [abbrev, in mathcomp.algebra.poly]
size_mulX [prf, in mathcomp.algebra.poly]
size_mulXn [prf, in mathcomp.algebra.poly]
size_MXaddC [prf, in mathcomp.algebra.poly]
size_mxminpoly [prf, in mathcomp.algebra.mxpoly]
size_ncons [prf, in mathcomp.boot.seq]
size_npoly [prf, in mathcomp.algebra.qpoly]
size_npoly0 [prf, in mathcomp.algebra.qpoly]
size_nseq [prf, in mathcomp.boot.seq]
size_odd_poly [prf, in mathcomp.algebra.poly]
size_odd_poly_eq [prf, in mathcomp.algebra.poly]
size_opp [abbrev, in mathcomp.algebra.poly]
size_orbit [prf, in mathcomp.boot.fingraph]
size_pairmap [prf, in mathcomp.boot.seq]
size_permutations [prf, in mathcomp.boot.seq]
size_pmap [prf, in mathcomp.boot.seq]
size_pmap_sub [prf, in mathcomp.boot.seq]
size_poly [prf, in mathcomp.algebra.poly]
size_Poly [prf, in mathcomp.algebra.poly]
size_poly0 [prf, in mathcomp.algebra.poly]
size_poly1 [prf, in mathcomp.algebra.poly]
size_poly1P [prf, in mathcomp.algebra.poly]
size_poly_eq [prf, in mathcomp.algebra.poly]
size_poly_eq0 [prf, in mathcomp.algebra.poly]
size_poly_exp_leq [prf, in mathcomp.algebra.poly]
size_poly_gt0 [prf, in mathcomp.algebra.poly]
size_poly_leq0 [prf, in mathcomp.algebra.poly]
size_poly_leq0P [prf, in mathcomp.algebra.poly]
size_poly_prod_leq [prf, in mathcomp.algebra.poly]
size_poly_XaY [prf, in mathcomp.algebra.polyXY]
size_poly_XmY [prf, in mathcomp.algebra.polyXY]
size_polyC [prf, in mathcomp.algebra.poly]
size_polyC_leq1 [prf, in mathcomp.algebra.poly]
size_polyD [prf, in mathcomp.algebra.poly]
size_polyDl [prf, in mathcomp.algebra.poly]
size_polyMleq [prf, in mathcomp.algebra.poly]
size_polyN [prf, in mathcomp.algebra.poly]
size_polyX [prf, in mathcomp.algebra.poly]
size_polyXn [prf, in mathcomp.algebra.poly]
size_prefix [prf, in mathcomp.boot.seq]
size_prod [prf, in mathcomp.algebra.poly]
size_prod_eq1 [prf, in mathcomp.algebra.poly]
size_prod_leq [abbrev, in mathcomp.algebra.poly]
size_prod_seq [prf, in mathcomp.algebra.poly]
size_prod_seq_eq1 [prf, in mathcomp.algebra.poly]
size_prod_XsubC [prf, in mathcomp.algebra.poly]
size_proper_mul [prf, in mathcomp.algebra.poly]
size_rat_int_poly [prf, in mathcomp.algebra.rat]
size_rcons [prf, in mathcomp.boot.seq]
size_rem [prf, in mathcomp.boot.seq]
size_reshape [prf, in mathcomp.boot.seq]
size_rev [prf, in mathcomp.boot.seq]
size_rot [prf, in mathcomp.boot.seq]
size_rotr [prf, in mathcomp.boot.seq]
size_scale [prf, in mathcomp.algebra.poly]
size_scale_leq [prf, in mathcomp.algebra.poly]
size_scanl [prf, in mathcomp.boot.seq]
size_set_nth [prf, in mathcomp.boot.seq]
size_sort [prf, in mathcomp.boot.path]
size_subseq [prf, in mathcomp.boot.seq]
size_subseq_leqif [prf, in mathcomp.boot.seq]
size_suffix [prf, in mathcomp.boot.seq]
size_sum [prf, in mathcomp.algebra.poly]
size_take [prf, in mathcomp.boot.seq]
size_take_min [prf, in mathcomp.boot.seq]
size_take_poly [prf, in mathcomp.algebra.poly]
size_takel [prf, in mathcomp.boot.seq]
size_tally_seq [prf, in mathcomp.boot.seq]
size_traject [prf, in mathcomp.boot.path]
size_tuple [prf, in mathcomp.boot.tuple]
size_undup [prf, in mathcomp.boot.seq]
size_widen_bseq [prf, in mathcomp.boot.tuple]
size_XaddC [prf, in mathcomp.algebra.poly]
size_XmulC [prf, in mathcomp.algebra.poly]
size_Xn_sub_1 [prf, in mathcomp.algebra.poly]
size_XnaddC [prf, in mathcomp.algebra.poly]
size_XnsubC [prf, in mathcomp.algebra.poly]
size_XsubC [prf, in mathcomp.algebra.poly]
size_zip [prf, in mathcomp.boot.seq]
size_zprimitive [prf, in mathcomp.algebra.intdiv]
sizeY [def, in mathcomp.algebra.polyXY]
sizeY_eq0 [prf, in mathcomp.algebra.polyXY]
sizeY_mulX [prf, in mathcomp.algebra.polyXY]
sizeYE [prf, in mathcomp.algebra.polyXY]
skew [abbrev, in mathcomp.algebra.sesquilinear]
skew_field_algid1 [prf, in mathcomp.field.falgebra]
skew_field_dimS [prf, in mathcomp.field.falgebra]
skew_field_module_dimS [prf, in mathcomp.field.falgebra]
skew_field_module_semisimple [prf, in mathcomp.field.falgebra]
skewmx [abbrev, in mathcomp.algebra.sesquilinear]
small_nil_class [prf, in mathcomp.solvable.sylow]
snd_is_monoid_morphism [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
snd_is_multiplicative [prf, in mathcomp.boot.monoid]
snd_is_scalable [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
snd_is_umagma_morphism [prf, in mathcomp.boot.monoid]
snd_is_zmod_morphism [prf, in mathcomp.boot.nmodule]
snd_morphism [def, in mathcomp.finite_group.gproduct]
snd_morphM [prf, in mathcomp.finite_group.gproduct]
soc [abbrev, in mathcomp.group_representation.character]
Socle [def, in mathcomp.group_representation.mxrepresentation]
socle_base [def, in mathcomp.group_representation.mxrepresentation]
socle_base_enum [proj, in mathcomp.group_representation.mxrepresentation]
Socle_direct [prf, in mathcomp.group_representation.mxrepresentation]
socle_enum [def, in mathcomp.group_representation.mxrepresentation]
socle_exists [prf, in mathcomp.group_representation.mxrepresentation]
socle_Iirr0 [prf, in mathcomp.group_representation.character]
socle_irr [prf, in mathcomp.group_representation.mxrepresentation]
Socle_iso [prf, in mathcomp.group_representation.mxrepresentation]
socle_mem [prf, in mathcomp.group_representation.mxrepresentation]
Socle_module [prf, in mathcomp.group_representation.mxrepresentation]
socle_module [def, in mathcomp.group_representation.mxrepresentation]
socle_mult [def, in mathcomp.group_representation.mxrepresentation]
socle_of_Iirr [def, in mathcomp.group_representation.character]
socle_of_Iirr_bij [prf, in mathcomp.group_representation.character]
socle_of_IirrK [prf, in mathcomp.group_representation.character]
socle_repr [def, in mathcomp.group_representation.mxrepresentation]
socle_rsimP [prf, in mathcomp.group_representation.mxrepresentation]
Socle_semisimple [prf, in mathcomp.group_representation.mxrepresentation]
socle_simple [prf, in mathcomp.group_representation.mxrepresentation]
socle_sort [ind, in mathcomp.group_representation.mxrepresentation]
socle_sort_ind [scheme, in mathcomp.group_representation.mxrepresentation]
socle_sort_rec [scheme, in mathcomp.group_representation.mxrepresentation]
socle_sort_rect [scheme, in mathcomp.group_representation.mxrepresentation]
socle_sort_sind [scheme, in mathcomp.group_representation.mxrepresentation]
socle_val [def, in mathcomp.group_representation.mxrepresentation]
socleP [prf, in mathcomp.group_representation.mxrepresentation]
socleType [rec, in mathcomp.group_representation.mxrepresentation]
sol_coprime_Sylow_exists [prf, in mathcomp.solvable.hall]
sol_coprime_Sylow_subset [prf, in mathcomp.solvable.hall]
sol_coprime_Sylow_trans [prf, in mathcomp.solvable.hall]
sol_der1_proper [prf, in mathcomp.solvable.nilpotent]
sol_prime_factor_exists [prf, in mathcomp.solvable.maximal]
solvable [file, in mathcomp.solvable.solvable]
solvable [def, in mathcomp.solvable.nilpotent]
solvable1 [prf, in mathcomp.solvable.nilpotent]
solvable_AltF [prf, in mathcomp.solvable.alt]
solvable_has_lin_char [prf, in mathcomp.group_representation.character]
solvable_irr_extendible_from_det [prf, in mathcomp.group_representation.inertia]
solvable_norm_abelem [prf, in mathcomp.solvable.maximal]
solvable_SymF [prf, in mathcomp.solvable.alt]
solvableS [prf, in mathcomp.solvable.nilpotent]
solve_Qint_span [prf, in mathcomp.algebra.rat]
some_big_AC_mk_monoid [prf, in mathcomp.boot.bigop]
some_big_mk_monoid [prf, in mathcomp.boot.bigop]
sop [def, in mathcomp.solvable.burnside_app]
sop_inj [prf, in mathcomp.solvable.burnside_app]
sop_morph [prf, in mathcomp.solvable.burnside_app]
sop_spec [prf, in mathcomp.solvable.burnside_app]
sort [def, in mathcomp.boot.path]
sort_bseq [def, in mathcomp.boot.tuple]
sort_bseqP [prf, in mathcomp.boot.tuple]
sort_iota_stable [prf, in mathcomp.boot.path]
sort_map [prf, in mathcomp.boot.path]
sort_pairwise_stable [prf, in mathcomp.boot.path]
sort_rec1 [def, in mathcomp.boot.path]
sort_sorted [prf, in mathcomp.boot.path]
sort_sorted_in [prf, in mathcomp.boot.path]
sort_stable [prf, in mathcomp.boot.path]
sort_stable_in [prf, in mathcomp.boot.path]
sort_tuple [def, in mathcomp.boot.tuple]
sort_tupleP [prf, in mathcomp.boot.tuple]
sort_uniq [prf, in mathcomp.boot.path]
sortE [prf, in mathcomp.boot.path]
sorted [abbrev, in mathcomp.boot.path]
sorted [abbrev, in mathcomp.boot.path]
sorted [def, in mathcomp.boot.path]
sorted_cat_cons [prf, in mathcomp.boot.path]
sorted_divisors [prf, in mathcomp.boot.prime]
sorted_divisors_ltn [prf, in mathcomp.boot.prime]
sorted_eq [prf, in mathcomp.boot.path]
sorted_eq_in [prf, in mathcomp.boot.path]
sorted_filter [prf, in mathcomp.boot.path]
sorted_filter_in [prf, in mathcomp.boot.path]
sorted_leq_index [prf, in mathcomp.boot.path]
sorted_leq_index_in [prf, in mathcomp.boot.path]
sorted_leq_nth [prf, in mathcomp.boot.path]
sorted_leq_nth_in [prf, in mathcomp.boot.path]
sorted_ltn_index [prf, in mathcomp.boot.path]
sorted_ltn_index_in [prf, in mathcomp.boot.path]
sorted_ltn_nth [prf, in mathcomp.boot.path]
sorted_ltn_nth_in [prf, in mathcomp.boot.path]
sorted_map [prf, in mathcomp.boot.path]
sorted_mask [prf, in mathcomp.boot.path]
sorted_mask_in [prf, in mathcomp.boot.path]
sorted_mask_sort [prf, in mathcomp.boot.path]
sorted_mask_sort_in [prf, in mathcomp.boot.path]
sorted_merge [prf, in mathcomp.boot.path]
sorted_pairwise [prf, in mathcomp.boot.path]
sorted_pairwise_in [prf, in mathcomp.boot.path]
sorted_primes [prf, in mathcomp.boot.prime]
sorted_relI [prf, in mathcomp.boot.path]
sorted_sort [prf, in mathcomp.boot.path]
sorted_sort_in [prf, in mathcomp.boot.path]
sorted_subseq_sort [prf, in mathcomp.boot.path]
sorted_subseq_sort_in [prf, in mathcomp.boot.path]
sorted_uniq [prf, in mathcomp.boot.path]
sorted_uniq_in [prf, in mathcomp.boot.path]
sortedP [prf, in mathcomp.boot.path]
sp [abbrev, in mathcomp.algebra.matrix]
sp [abbrev, in mathcomp.algebra.matrix]
sp [abbrev, in mathcomp.algebra.matrix]
sp [abbrev, in mathcomp.algebra.matrix]
sp [abbrev, in mathcomp.algebra.matrix]
sp [abbrev, in mathcomp.algebra.matrix]
sp [abbrev, in mathcomp.algebra.matrix]
sp [abbrev, in mathcomp.algebra.matrix]
sp [abbrev, in mathcomp.algebra.matrix]
sp [abbrev, in mathcomp.algebra.matrix]
sp [abbrev, in mathcomp.algebra.matrix]
sp [abbrev, in mathcomp.algebra.matrix]
Space [constr, in mathcomp.algebra.vector]
space [ind, in mathcomp.algebra.vector]
space_ind [scheme, in mathcomp.algebra.vector]
space_rec [scheme, in mathcomp.algebra.vector]
space_rect [scheme, in mathcomp.algebra.vector]
space_sind [scheme, in mathcomp.algebra.vector]
span [def, in mathcomp.algebra.vector]
span_basis [prf, in mathcomp.algebra.vector]
span_bigcat [prf, in mathcomp.algebra.vector]
span_cat [prf, in mathcomp.algebra.vector]
span_cons [prf, in mathcomp.algebra.vector]
span_def [prf, in mathcomp.algebra.vector]
span_expanded_def [def, in mathcomp.algebra.vector]
span_key [prf, in mathcomp.algebra.vector]
span_lfunP [prf, in mathcomp.algebra.vector]
span_nil [prf, in mathcomp.algebra.vector]
span_orthogonal [prf, in mathcomp.group_representation.classfun]
span_orthogonal [prf, in mathcomp.algebra.sesquilinear]
span_seq1 [prf, in mathcomp.algebra.vector]
span_subvP [prf, in mathcomp.algebra.vector]
span_unlockable [def, in mathcomp.algebra.vector]
special [def, in mathcomp.solvable.maximal]
spectral [file, in mathcomp.algebra.spectral]
spectral_diag [def, in mathcomp.algebra.spectral]
spectral_unit [prf, in mathcomp.algebra.spectral]
spectral_unitarymx [prf, in mathcomp.algebra.spectral]
spectralmx [def, in mathcomp.algebra.spectral]
Split [constr, in mathcomp.boot.path]
split [ind, in mathcomp.boot.path]
split [def, in mathcomp.boot.fintype]
split1 [prf, in mathcomp.boot.nmodule]
split1_extraspecial [prf, in mathcomp.solvable.maximal]
Split2r [constr, in mathcomp.boot.path]
split2r [ind, in mathcomp.boot.path]
split_find [prf, in mathcomp.boot.seq]
split_find_nth [prf, in mathcomp.boot.seq]
split_find_nth_spec [ind, in mathcomp.boot.seq]
split_find_spec [ind, in mathcomp.boot.seq]
split_ord_spec [ind, in mathcomp.boot.fintype]
split_ordP [prf, in mathcomp.boot.fintype]
split_spec [ind, in mathcomp.boot.fintype]
SplitHi [constr, in mathcomp.boot.fintype]
splitK [prf, in mathcomp.boot.fintype]
Splitl [constr, in mathcomp.boot.path]
splitl [ind, in mathcomp.boot.path]
SplitLo [constr, in mathcomp.boot.fintype]
SplitOrdHi [constr, in mathcomp.boot.fintype]
SplitOrdLo [constr, in mathcomp.boot.fintype]
splitP [prf, in mathcomp.boot.path]
splitP [prf, in mathcomp.boot.fintype]
splitP2r [prf, in mathcomp.boot.path]
splitPl [prf, in mathcomp.boot.path]
splitPr [prf, in mathcomp.boot.path]
Splitr [constr, in mathcomp.boot.path]
splitr [ind, in mathcomp.boot.path]
splits_over [def, in mathcomp.finite_group.gproduct]
splitsP [prf, in mathcomp.finite_group.gproduct]
splitting_cyclic_primitive_root [abbrev, in mathcomp.group_representation.mxrepresentation]
splitting_cyclic_primitive_root_pchar [prf, in mathcomp.group_representation.mxrepresentation]
splitting_field_axiom [def, in mathcomp.field.galois]
splitting_field_normal [prf, in mathcomp.field.galois]
splitting_galoisField [prf, in mathcomp.field.galois]
splitting_normalField [prf, in mathcomp.field.galois]
SplittingField [abbrev, in mathcomp.field.galois]
SplittingField [mod, in mathcomp.field.galois]
SplittingField.Algebra_AddMagma_isAddSemigroup_mixin [proj, in mathcomp.field.galois]
SplittingField.Algebra_BaseAddMagma_isAddMagma_mixin [proj, in mathcomp.field.galois]
SplittingField.Algebra_BaseAddUMagma_isAddUMagma_mixin [proj, in mathcomp.field.galois]
SplittingField.Algebra_BaseZmoduleNmodule_isZmodule_mixin [proj, in mathcomp.field.galois]
SplittingField.Algebra_hasAdd_mixin [proj, in mathcomp.field.galois]
SplittingField.Algebra_hasOpp_mixin [proj, in mathcomp.field.galois]
SplittingField.Algebra_hasZero_mixin [proj, in mathcomp.field.galois]
SplittingField.axioms_ [rec, in mathcomp.field.galois]
SplittingField.choice_hasChoice_mixin [proj, in mathcomp.field.galois]
SplittingField.class [proj, in mathcomp.field.galois]
SplittingField.clone [abbrev, in mathcomp.field.galois]
SplittingField.copy [abbrev, in mathcomp.field.galois]
SplittingField.eqtype_hasDecEq_mixin [proj, in mathcomp.field.galois]
SplittingField.Exports [mod, in mathcomp.field.galois]
SplittingField.Exports.splittingFieldType [abbrev, in mathcomp.field.galois]
SplittingField.galois_FieldExt_isSplittingField_mixin [proj, in mathcomp.field.galois]
SplittingField.GRing_ComUnitRing_isIntegral_mixin [proj, in mathcomp.field.galois]
SplittingField.GRing_LSemiAlgebra_isSemiAlgebra_mixin [proj, in mathcomp.field.galois]
SplittingField.GRing_LSemiModule_isLSemiAlgebra_mixin [proj, in mathcomp.field.galois]
SplittingField.GRing_Nmodule_isLSemiModule_mixin [proj, in mathcomp.field.galois]
SplittingField.GRing_Nmodule_isPzSemiRing_mixin [proj, in mathcomp.field.galois]
SplittingField.GRing_NzRing_hasMulInverse_mixin [proj, in mathcomp.field.galois]
SplittingField.GRing_PzSemiRing_isNonZero_mixin [proj, in mathcomp.field.galois]
SplittingField.GRing_SemiRing_hasCommutativeMul_mixin [proj, in mathcomp.field.galois]
SplittingField.GRing_UnitRing_isField_mixin [proj, in mathcomp.field.galois]
SplittingField.on [abbrev, in mathcomp.field.galois]
SplittingField.on_ [abbrev, in mathcomp.field.galois]
SplittingField.pack_ [def, in mathcomp.field.galois]
SplittingField.phant_clone [def, in mathcomp.field.galois]
SplittingField.phant_on_ [def, in mathcomp.field.galois]
SplittingField.sort [proj, in mathcomp.field.galois]
SplittingField.type [rec, in mathcomp.field.galois]
SplittingField.vector_LSemiModule_hasFinDim_mixin [proj, in mathcomp.field.galois]
SplittingField.vector_SemiVector_isProper_mixin [proj, in mathcomp.field.galois]
SplittingFieldElpiOperations [mod, in mathcomp.field.galois]
SplittingFieldExports [mod, in mathcomp.field.galois]
splittingFieldFor [def, in mathcomp.field.galois]
splittingFieldForS [prf, in mathcomp.field.galois]
splittingFieldP [prf, in mathcomp.field.galois]
splittingPoly [prf, in mathcomp.field.galois]
sq [abbrev, in mathcomp.algebra.matrix]
sq [abbrev, in mathcomp.algebra.matrix]
sq [abbrev, in mathcomp.algebra.matrix]
sq [abbrev, in mathcomp.algebra.matrix]
sq [abbrev, in mathcomp.algebra.matrix]
sq [abbrev, in mathcomp.algebra.matrix]
sq [abbrev, in mathcomp.algebra.matrix]
sqmx_ind [prf, in mathcomp.algebra.matrix]
sqrn_gt0 [prf, in mathcomp.boot.ssrnat]
sqrn_inj [prf, in mathcomp.boot.ssrnat]
sqrnB [prf, in mathcomp.boot.ssrnat]
sqrnD [prf, in mathcomp.boot.ssrnat]
sqrnD_sub [prf, in mathcomp.boot.ssrnat]
sqrt_cfnorm_eq0 [prf, in mathcomp.group_representation.classfun]
sqrt_cfnorm_ge0 [prf, in mathcomp.group_representation.classfun]
sqrt_cfnorm_gt0 [prf, in mathcomp.group_representation.classfun]
sqrt_dnorm_eq0 [prf, in mathcomp.algebra.sesquilinear]
sqrt_dnorm_ge0 [prf, in mathcomp.algebra.sesquilinear]
sqrt_dnorm_gt0 [prf, in mathcomp.algebra.sesquilinear]
square [def, in mathcomp.solvable.burnside_app]
square_coloring_number2 [def, in mathcomp.solvable.burnside_app]
square_coloring_number4 [def, in mathcomp.solvable.burnside_app]
square_coloring_number8 [def, in mathcomp.solvable.burnside_app]
sr [abbrev, in mathcomp.group_representation.mxrepresentation]
ssetI [def, in mathcomp.boot.finset]
ssimS [abbrev, in mathcomp.group_representation.mxrepresentation]
ssrAC [file, in mathcomp.boot.ssrAC]
ssralg [file, in mathcomp.algebra.algebraic_hierarchy.ssralg]
ssrbool [file, in mathcomp.boot.ssrbool]
ssreflect [file, in mathcomp.boot.ssreflect]
ssrfun [file, in mathcomp.boot.ssrfun]
ssrint [file, in mathcomp.algebra.ssrint]
ssrmatching [file, in mathcomp.boot.ssrmatching]
ssrnat [file, in mathcomp.boot.ssrnat]
ssrnotations [file, in mathcomp.boot.ssrnotations]
ssrnum [file, in mathcomp.algebra.numeric_hierarchy.ssrnum]
ssval [proj, in mathcomp.boot.fintype]
ssvalP [proj, in mathcomp.boot.fintype]
sT [abbrev, in mathcomp.finite_group.fingroup]
sT [abbrev, in mathcomp.boot.fintype]
sT [abbrev, in mathcomp.boot.finset]
stab_ntransitive [prf, in mathcomp.solvable.primitive_action]
stab_ntransitiveI [prf, in mathcomp.solvable.primitive_action]
stab_semiprime [prf, in mathcomp.solvable.frobenius]
stable [prf, in mathcomp.solvable.burnside_app]
stable0mx [prf, in mathcomp.algebra.mxalgebra]
stable_factor [def, in mathcomp.solvable.gseries]
stable_rowg_mxK [prf, in mathcomp.group_representation.mxabelem]
stableCmx [prf, in mathcomp.algebra.mxalgebra]
stableDmx [prf, in mathcomp.algebra.mxalgebra]
stablemx [abbrev, in mathcomp.algebra.mxalgebra]
stablemx [abbrev, in mathcomp.algebra.mxalgebra]
stablemx0 [prf, in mathcomp.algebra.mxalgebra]
stablemx_comp [prf, in mathcomp.algebra.mxred]
stablemx_comp [prf, in mathcomp.algebra.mxpoly]
stablemx_full [prf, in mathcomp.algebra.mxalgebra]
stablemx_restrict [prf, in mathcomp.algebra.mxred]
stablemx_restrict [prf, in mathcomp.algebra.mxpoly]
stablemx_row_base [prf, in mathcomp.algebra.mxalgebra]
stablemx_sums [prf, in mathcomp.algebra.mxalgebra]
stablemx_unit [prf, in mathcomp.algebra.mxalgebra]
stablemxC [prf, in mathcomp.algebra.mxalgebra]
stablemxD [prf, in mathcomp.algebra.mxalgebra]
stablemxM [prf, in mathcomp.algebra.mxalgebra]
stablemxN [prf, in mathcomp.algebra.mxalgebra]
stableNmx [prf, in mathcomp.algebra.mxalgebra]
standard_grepr [def, in mathcomp.group_representation.character]
standard_irr [def, in mathcomp.group_representation.character]
standard_irr_coef [def, in mathcomp.group_representation.character]
standard_socle [def, in mathcomp.group_representation.character]
StarMonoid [abbrev, in mathcomp.boot.monoid]
StarMonoid [mod, in mathcomp.boot.monoid]
StarMonoid.axioms_ [rec, in mathcomp.boot.monoid]
StarMonoid.choice_hasChoice_mixin [proj, in mathcomp.boot.monoid]
StarMonoid.class [proj, in mathcomp.boot.monoid]
StarMonoid.clone [abbrev, in mathcomp.boot.monoid]
StarMonoid.copy [abbrev, in mathcomp.boot.monoid]
StarMonoid.eqtype_hasDecEq_mixin [proj, in mathcomp.boot.monoid]
StarMonoid.Exports [mod, in mathcomp.boot.monoid]
StarMonoid.Exports.join_monoid_StarMonoid_between_monoid_BaseGroup_and_choice_Choice [def, in mathcomp.boot.monoid]
StarMonoid.Exports.join_monoid_StarMonoid_between_monoid_BaseGroup_and_eqtype_Equality [def, in mathcomp.boot.monoid]
StarMonoid.Exports.join_monoid_StarMonoid_between_monoid_BaseGroup_and_monoid_ChoiceBaseUMagma [def, in mathcomp.boot.monoid]
StarMonoid.Exports.join_monoid_StarMonoid_between_monoid_BaseGroup_and_monoid_ChoiceMagma [def, in mathcomp.boot.monoid]
StarMonoid.Exports.join_monoid_StarMonoid_between_monoid_BaseGroup_and_monoid_Monoid [def, in mathcomp.boot.monoid]
StarMonoid.Exports.join_monoid_StarMonoid_between_monoid_BaseGroup_and_monoid_Semigroup [def, in mathcomp.boot.monoid]
StarMonoid.Exports.join_monoid_StarMonoid_between_monoid_BaseGroup_and_monoid_UMagma [def, in mathcomp.boot.monoid]
StarMonoid.Exports.starMonoidType [abbrev, in mathcomp.boot.monoid]
StarMonoid.monoid_BaseUMagma_isUMagma_mixin [proj, in mathcomp.boot.monoid]
StarMonoid.monoid_hasInv_mixin [proj, in mathcomp.boot.monoid]
StarMonoid.monoid_hasMul_mixin [proj, in mathcomp.boot.monoid]
StarMonoid.monoid_hasOne_mixin [proj, in mathcomp.boot.monoid]
StarMonoid.monoid_Magma_isSemigroup_mixin [proj, in mathcomp.boot.monoid]
StarMonoid.monoid_Monoid_isStarMonoid_mixin [proj, in mathcomp.boot.monoid]
StarMonoid.on [abbrev, in mathcomp.boot.monoid]
StarMonoid.on_ [abbrev, in mathcomp.boot.monoid]
StarMonoid.pack_ [def, in mathcomp.boot.monoid]
StarMonoid.phant_clone [def, in mathcomp.boot.monoid]
StarMonoid.phant_on_ [def, in mathcomp.boot.monoid]
StarMonoid.sort [proj, in mathcomp.boot.monoid]
StarMonoid.type [rec, in mathcomp.boot.monoid]
StarMonoid_isGroup [abbrev, in mathcomp.boot.monoid]
StarMonoid_isGroup [mod, in mathcomp.boot.monoid]
StarMonoid_isGroup.axioms [abbrev, in mathcomp.boot.monoid]
StarMonoid_isGroup.axioms_ [rec, in mathcomp.boot.monoid]
StarMonoid_isGroup.Build [abbrev, in mathcomp.boot.monoid]
StarMonoid_isGroup.Exports [mod, in mathcomp.boot.monoid]
StarMonoid_isGroup.identity_builder [def, in mathcomp.boot.monoid]
StarMonoid_isGroup.mulVg [proj, in mathcomp.boot.monoid]
StarMonoid_isGroup.phant_axioms [def, in mathcomp.boot.monoid]
StarMonoid_isGroup.phant_Build [def, in mathcomp.boot.monoid]
StarMonoidElpiOperations [mod, in mathcomp.boot.monoid]
strict_adjunction [prf, in mathcomp.boot.fingraph]
strong_Primitive_Element_Theorem [prf, in mathcomp.field.separable]
strongest_coprime_quotient_cent [prf, in mathcomp.solvable.hall]
StrongJordanHolderUniqueness [prf, in mathcomp.solvable.jordanholder]
Sub [abbrev, in mathcomp.boot.eqtype]
Sub [def, in mathcomp.boot.eqtype]
sub0mx [prf, in mathcomp.algebra.mxalgebra]
sub0n [prf, in mathcomp.boot.ssrnat]
sub0seq [prf, in mathcomp.boot.seq]
sub0set [prf, in mathcomp.boot.finset]
sub0v [prf, in mathcomp.algebra.vector]
sub1_agenv [prf, in mathcomp.field.falgebra]
sub1b [prf, in mathcomp.boot.ssrnat]
sub1G [prf, in mathcomp.finite_group.fingroup]
sub1mx [prf, in mathcomp.algebra.mxalgebra]
sub1seq [prf, in mathcomp.boot.seq]
sub1set [prf, in mathcomp.boot.finset]
sub1v [prf, in mathcomp.field.fieldext]
sub_abelem_rV_im [prf, in mathcomp.group_representation.mxabelem]
sub_abelian_cent [prf, in mathcomp.finite_group.fingroup]
sub_abelian_cent2 [prf, in mathcomp.finite_group.fingroup]
sub_abelian_norm [prf, in mathcomp.finite_group.fingroup]
sub_abelian_normal [prf, in mathcomp.finite_group.fingroup]
sub_act_proof [prf, in mathcomp.finite_group.action]
sub_adds_genmx_ortho [prf, in mathcomp.algebra.spectral]
sub_addsmxP [prf, in mathcomp.algebra.mxalgebra]
sub_adjoin1v [prf, in mathcomp.field.fieldext]
sub_adjoin_separable_generator [prf, in mathcomp.field.separable]
sub_afixRs_norm [prf, in mathcomp.finite_group.action]
sub_afixRs_norms [prf, in mathcomp.finite_group.action]
sub_agenv [prf, in mathcomp.field.falgebra]
sub_all [prf, in mathcomp.boot.seq]
sub_allrel [prf, in mathcomp.boot.seq]
sub_annihilant [def, in mathcomp.algebra.polyXY]
sub_annihilant_in_ideal [prf, in mathcomp.algebra.polyXY]
sub_annihilant_neq0 [prf, in mathcomp.algebra.polyXY]
sub_annihilantP [prf, in mathcomp.algebra.polyXY]
sub_astab1 [prf, in mathcomp.finite_group.action]
sub_astab1_in [prf, in mathcomp.finite_group.action]
sub_astabQ [prf, in mathcomp.finite_group.action]
sub_astabQR [prf, in mathcomp.finite_group.action]
sub_aut_zchar [prf, in mathcomp.group_representation.vcharacter]
sub_baseField [prf, in mathcomp.field.fieldext]
sub_bigcapmxP [prf, in mathcomp.algebra.mxalgebra]
sub_capmx [prf, in mathcomp.algebra.mxalgebra]
sub_capmx_gen [prf, in mathcomp.algebra.mxalgebra]
sub_cent1 [prf, in mathcomp.finite_group.fingroup]
sub_center_normal [prf, in mathcomp.solvable.center]
sub_cfker_mod [prf, in mathcomp.group_representation.classfun]
sub_cfker_morph [prf, in mathcomp.group_representation.classfun]
sub_cfker_Res [prf, in mathcomp.group_representation.classfun]
sub_class_support [prf, in mathcomp.finite_group.fingroup]
sub_conjC_vchar [prf, in mathcomp.group_representation.vcharacter]
sub_conjg [prf, in mathcomp.finite_group.fingroup]
sub_conjgV [prf, in mathcomp.finite_group.fingroup]
sub_cosetpre [prf, in mathcomp.finite_group.quotient]
sub_cosetpre_quo [prf, in mathcomp.finite_group.quotient]
sub_count [prf, in mathcomp.boot.seq]
sub_cycle [prf, in mathcomp.boot.path]
sub_cyclic_char [prf, in mathcomp.solvable.cyclic]
sub_daddsmx [prf, in mathcomp.algebra.mxalgebra]
sub_daddsmx_spec [ind, in mathcomp.algebra.mxalgebra]
sub_der1_abelian [prf, in mathcomp.solvable.commutator]
sub_der1_norm [prf, in mathcomp.solvable.commutator]
sub_der1_normal [prf, in mathcomp.solvable.commutator]
sub_dsumsmx [prf, in mathcomp.algebra.mxalgebra]
sub_dsumsmx_spec [ind, in mathcomp.algebra.mxalgebra]
sub_eigenspace_conjmx [prf, in mathcomp.algebra.mxred]
sub_eigenspace_conjmx [prf, in mathcomp.algebra.mxpoly]
sub_find [prf, in mathcomp.boot.seq]
sub_gcore [prf, in mathcomp.finite_group.fingroup]
sub_gen [prf, in mathcomp.finite_group.fingroup]
sub_Hall_pcore [prf, in mathcomp.solvable.pgroup]
sub_has [prf, in mathcomp.boot.seq]
sub_im_abelem_rV [prf, in mathcomp.group_representation.mxabelem]
sub_im_coset [prf, in mathcomp.finite_group.quotient]
sub_imset_pre [prf, in mathcomp.boot.finset]
sub_in_allrel [prf, in mathcomp.boot.seq]
sub_in_constt [prf, in mathcomp.solvable.pgroup]
sub_in_cycle [prf, in mathcomp.boot.path]
sub_in_le_big [prf, in mathcomp.boot.bigop]
sub_in_pairwise [prf, in mathcomp.boot.seq]
sub_in_partn [prf, in mathcomp.boot.prime]
sub_in_path [prf, in mathcomp.boot.path]
sub_in_pcore [prf, in mathcomp.solvable.pgroup]
sub_in_pnat [prf, in mathcomp.boot.prime]
sub_in_sorted [prf, in mathcomp.boot.path]
sub_Inertia [prf, in mathcomp.group_representation.inertia]
sub_inertia [prf, in mathcomp.group_representation.inertia]
sub_inertia_Ind [prf, in mathcomp.group_representation.inertia]
sub_inertia_Res [prf, in mathcomp.group_representation.inertia]
sub_inseparable [prf, in mathcomp.field.separable]
sub_iso_to [prf, in mathcomp.group_representation.classfun]
sub_isog [prf, in mathcomp.finite_group.morphism]
sub_isom [prf, in mathcomp.finite_group.morphism]
sub_kermx [prf, in mathcomp.algebra.mxalgebra]
sub_kermxP [prf, in mathcomp.algebra.mxalgebra]
sub_kermxpoly_conjmx [prf, in mathcomp.algebra.mxred]
sub_kermxpoly_conjmx [prf, in mathcomp.algebra.mxpoly]
sub_lcoset [prf, in mathcomp.finite_group.fingroup]
sub_lcosetV [prf, in mathcomp.finite_group.fingroup]
sub_Ldiv [prf, in mathcomp.solvable.abelian]
sub_LdivT [prf, in mathcomp.solvable.abelian]
sub_le_big [prf, in mathcomp.boot.bigop]
sub_le_big_seq [prf, in mathcomp.boot.bigop]
sub_le_big_seq_cond [prf, in mathcomp.boot.bigop]
sub_ltmx_trans [prf, in mathcomp.algebra.mxalgebra]
sub_map [prf, in mathcomp.boot.seq]
sub_morphim_cfker [prf, in mathcomp.group_representation.classfun]
sub_morphim_pre [prf, in mathcomp.finite_group.morphism]
sub_morphpre_im [prf, in mathcomp.finite_group.morphism]
sub_morphpre_injm [prf, in mathcomp.finite_group.morphism]
sub_nilpotent_cent2 [prf, in mathcomp.solvable.sylow]
sub_normal_Hall [prf, in mathcomp.solvable.pgroup]
sub_ord [def, in mathcomp.boot.fintype]
sub_ord_proof [prf, in mathcomp.boot.fintype]
sub_ordK [prf, in mathcomp.boot.fintype]
sub_orthonormal [prf, in mathcomp.group_representation.classfun]
sub_orthonormal [prf, in mathcomp.algebra.sesquilinear]
sub_p_elt [prf, in mathcomp.solvable.pgroup]
sub_pairwise [prf, in mathcomp.boot.seq]
sub_pairwise_orthogonal [prf, in mathcomp.group_representation.classfun]
sub_pairwise_orthogonal [prf, in mathcomp.algebra.sesquilinear]
sub_path [prf, in mathcomp.boot.path]
sub_pcore [prf, in mathcomp.solvable.pgroup]
sub_pgroup [prf, in mathcomp.solvable.pgroup]
sub_pHall [prf, in mathcomp.solvable.pgroup]
sub_pnat_coprime [prf, in mathcomp.boot.prime]
sub_proper_trans [prf, in mathcomp.boot.fintype]
sub_quotient_pre [prf, in mathcomp.finite_group.quotient]
sub_rcoset [prf, in mathcomp.finite_group.fingroup]
sub_rcosetV [prf, in mathcomp.finite_group.fingroup]
Sub_rect [def, in mathcomp.boot.eqtype]
sub_rowg_mx [prf, in mathcomp.group_representation.mxabelem]
sub_rVabelem [prf, in mathcomp.group_representation.mxabelem]
sub_rVabelem_im [prf, in mathcomp.group_representation.mxabelem]
sub_rVP [prf, in mathcomp.algebra.mxalgebra]
sub_sorted [prf, in mathcomp.boot.path]
sub_span [prf, in mathcomp.algebra.vector]
Sub_spec [ind, in mathcomp.boot.eqtype]
sub_sums_genmxP [prf, in mathcomp.algebra.mxalgebra]
sub_sumsmxP [prf, in mathcomp.algebra.mxalgebra]
sub_type [def, in mathcomp.boot.eqtype]
sub_Zp_1 [prf, in mathcomp.algebra.zmodp]
subact [def, in mathcomp.finite_group.action]
subact_dom [def, in mathcomp.finite_group.action]
subact_dom_group [def, in mathcomp.finite_group.action]
subact_is_action [prf, in mathcomp.finite_group.action]
subaction [def, in mathcomp.finite_group.action]
subAlgType [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
SubBaseUMagma [abbrev, in mathcomp.boot.monoid]
SubBaseUMagma [mod, in mathcomp.boot.monoid]
SubBaseUMagma.axioms_ [rec, in mathcomp.boot.monoid]
SubBaseUMagma.choice_hasChoice_mixin [proj, in mathcomp.boot.monoid]
SubBaseUMagma.class [proj, in mathcomp.boot.monoid]
SubBaseUMagma.clone [abbrev, in mathcomp.boot.monoid]
SubBaseUMagma.copy [abbrev, in mathcomp.boot.monoid]
SubBaseUMagma.eqtype_hasDecEq_mixin [proj, in mathcomp.boot.monoid]
SubBaseUMagma.eqtype_isSub_mixin [proj, in mathcomp.boot.monoid]
SubBaseUMagma.Exports [mod, in mathcomp.boot.monoid]
SubBaseUMagma.Exports.join_monoid_SubBaseUMagma_between_monoid_BaseUMagma_and_choice_SubChoice [def, in mathcomp.boot.monoid]
SubBaseUMagma.Exports.join_monoid_SubBaseUMagma_between_monoid_BaseUMagma_and_eqtype_SubEquality [def, in mathcomp.boot.monoid]
SubBaseUMagma.Exports.join_monoid_SubBaseUMagma_between_monoid_BaseUMagma_and_eqtype_SubType [def, in mathcomp.boot.monoid]
SubBaseUMagma.Exports.join_monoid_SubBaseUMagma_between_monoid_BaseUMagma_and_monoid_SubMagma [def, in mathcomp.boot.monoid]
SubBaseUMagma.Exports.join_monoid_SubBaseUMagma_between_monoid_ChoiceBaseUMagma_and_choice_SubChoice [def, in mathcomp.boot.monoid]
SubBaseUMagma.Exports.join_monoid_SubBaseUMagma_between_monoid_ChoiceBaseUMagma_and_eqtype_SubEquality [def, in mathcomp.boot.monoid]
SubBaseUMagma.Exports.join_monoid_SubBaseUMagma_between_monoid_ChoiceBaseUMagma_and_eqtype_SubType [def, in mathcomp.boot.monoid]
SubBaseUMagma.Exports.join_monoid_SubBaseUMagma_between_monoid_ChoiceBaseUMagma_and_monoid_SubMagma [def, in mathcomp.boot.monoid]
SubBaseUMagma.Exports.subBaseUMagmaType [abbrev, in mathcomp.boot.monoid]
SubBaseUMagma.monoid_hasMul_mixin [proj, in mathcomp.boot.monoid]
SubBaseUMagma.monoid_hasOne_mixin [proj, in mathcomp.boot.monoid]
SubBaseUMagma.monoid_isSubBaseUMagma_mixin [proj, in mathcomp.boot.monoid]
SubBaseUMagma.monoid_isSubMagma_mixin [proj, in mathcomp.boot.monoid]
SubBaseUMagma.on [abbrev, in mathcomp.boot.monoid]
SubBaseUMagma.on_ [abbrev, in mathcomp.boot.monoid]
SubBaseUMagma.pack_ [def, in mathcomp.boot.monoid]
SubBaseUMagma.phant_clone [def, in mathcomp.boot.monoid]
SubBaseUMagma.phant_on_ [def, in mathcomp.boot.monoid]
SubBaseUMagma.sort [proj, in mathcomp.boot.monoid]
SubBaseUMagma.type [rec, in mathcomp.boot.monoid]
SubBaseUMagmaElpiOperations [mod, in mathcomp.boot.monoid]
subBnAC [prf, in mathcomp.boot.ssrnat]
subcent1_cycle_norm [prf, in mathcomp.solvable.center]
subcent1_cycle_normal [prf, in mathcomp.solvable.center]
subcent1_cycle_sub [prf, in mathcomp.solvable.center]
subcent1_extraspecial_maximal [prf, in mathcomp.solvable.maximal]
subcent1_id [prf, in mathcomp.solvable.center]
subcent1_sub [prf, in mathcomp.solvable.center]
subcent1C [prf, in mathcomp.solvable.center]
subcent1P [prf, in mathcomp.solvable.center]
subcent_char [prf, in mathcomp.solvable.center]
subcent_dprod [prf, in mathcomp.finite_group.gproduct]
subcent_norm [prf, in mathcomp.solvable.center]
subcent_normal [prf, in mathcomp.solvable.center]
subcent_sdprod [prf, in mathcomp.finite_group.gproduct]
subcent_sub [prf, in mathcomp.solvable.center]
subcent_TImulg [prf, in mathcomp.finite_group.gproduct]
subcentP [prf, in mathcomp.solvable.center]
SubChoice [abbrev, in mathcomp.boot.choice]
SubChoice [mod, in mathcomp.boot.choice]
SubChoice.axioms_ [rec, in mathcomp.boot.choice]
SubChoice.choice_hasChoice_mixin [proj, in mathcomp.boot.choice]
SubChoice.class [proj, in mathcomp.boot.choice]
SubChoice.clone [abbrev, in mathcomp.boot.choice]
SubChoice.copy [abbrev, in mathcomp.boot.choice]
SubChoice.eqtype_hasDecEq_mixin [proj, in mathcomp.boot.choice]
SubChoice.eqtype_isSub_mixin [proj, in mathcomp.boot.choice]
SubChoice.Exports [mod, in mathcomp.boot.choice]
SubChoice.Exports.join_choice_SubChoice_between_choice_Choice_and_eqtype_SubEquality [def, in mathcomp.boot.choice]
SubChoice.Exports.join_choice_SubChoice_between_choice_Choice_and_eqtype_SubType [def, in mathcomp.boot.choice]
SubChoice.Exports.subChoiceType [abbrev, in mathcomp.boot.choice]
SubChoice.on [abbrev, in mathcomp.boot.choice]
SubChoice.on_ [abbrev, in mathcomp.boot.choice]
SubChoice.pack_ [def, in mathcomp.boot.choice]
SubChoice.phant_clone [def, in mathcomp.boot.choice]
SubChoice.phant_on_ [def, in mathcomp.boot.choice]
SubChoice.sort [proj, in mathcomp.boot.choice]
SubChoice.type [rec, in mathcomp.boot.choice]
SubChoice_isSubGroup [abbrev, in mathcomp.boot.monoid]
SubChoice_isSubGroup [mod, in mathcomp.boot.monoid]
SubChoice_isSubGroup.axioms [abbrev, in mathcomp.boot.monoid]
SubChoice_isSubGroup.axioms_ [rec, in mathcomp.boot.monoid]
SubChoice_isSubGroup.Build [abbrev, in mathcomp.boot.monoid]
SubChoice_isSubGroup.Exports [mod, in mathcomp.boot.monoid]
SubChoice_isSubGroup.phant_axioms [def, in mathcomp.boot.monoid]
SubChoice_isSubGroup.phant_Build [def, in mathcomp.boot.monoid]
SubChoice_isSubMagma [abbrev, in mathcomp.boot.monoid]
SubChoice_isSubMagma [mod, in mathcomp.boot.monoid]
SubChoice_isSubMagma.axioms [abbrev, in mathcomp.boot.monoid]
SubChoice_isSubMagma.axioms_ [rec, in mathcomp.boot.monoid]
SubChoice_isSubMagma.Build [abbrev, in mathcomp.boot.monoid]
SubChoice_isSubMagma.Exports [mod, in mathcomp.boot.monoid]
SubChoice_isSubMagma.phant_axioms [def, in mathcomp.boot.monoid]
SubChoice_isSubMagma.phant_Build [def, in mathcomp.boot.monoid]
SubChoice_isSubMonoid [abbrev, in mathcomp.boot.monoid]
SubChoice_isSubMonoid [mod, in mathcomp.boot.monoid]
SubChoice_isSubMonoid.axioms [abbrev, in mathcomp.boot.monoid]
SubChoice_isSubMonoid.axioms_ [rec, in mathcomp.boot.monoid]
SubChoice_isSubMonoid.Build [abbrev, in mathcomp.boot.monoid]
SubChoice_isSubMonoid.Exports [mod, in mathcomp.boot.monoid]
SubChoice_isSubMonoid.phant_axioms [def, in mathcomp.boot.monoid]
SubChoice_isSubMonoid.phant_Build [def, in mathcomp.boot.monoid]
SubChoice_isSubSemigroup [abbrev, in mathcomp.boot.monoid]
SubChoice_isSubSemigroup [mod, in mathcomp.boot.monoid]
SubChoice_isSubSemigroup.axioms [abbrev, in mathcomp.boot.monoid]
SubChoice_isSubSemigroup.axioms_ [rec, in mathcomp.boot.monoid]
SubChoice_isSubSemigroup.Build [abbrev, in mathcomp.boot.monoid]
SubChoice_isSubSemigroup.Exports [mod, in mathcomp.boot.monoid]
SubChoice_isSubSemigroup.phant_axioms [def, in mathcomp.boot.monoid]
SubChoice_isSubSemigroup.phant_Build [def, in mathcomp.boot.monoid]
SubChoice_isSubUMagma [abbrev, in mathcomp.boot.monoid]
SubChoice_isSubUMagma [mod, in mathcomp.boot.monoid]
SubChoice_isSubUMagma.axioms [abbrev, in mathcomp.boot.monoid]
SubChoice_isSubUMagma.axioms_ [rec, in mathcomp.boot.monoid]
SubChoice_isSubUMagma.Build [abbrev, in mathcomp.boot.monoid]
SubChoice_isSubUMagma.Exports [mod, in mathcomp.boot.monoid]
SubChoice_isSubUMagma.phant_axioms [def, in mathcomp.boot.monoid]
SubChoice_isSubUMagma.phant_Build [def, in mathcomp.boot.monoid]
SubChoiceElpiOperations [mod, in mathcomp.boot.choice]
subComRingType [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
subComSemiRingType [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
SubCountable [abbrev, in mathcomp.boot.choice]
SubCountable [mod, in mathcomp.boot.choice]
SubCountable.axioms_ [rec, in mathcomp.boot.choice]
SubCountable.choice_Choice_isCountable_mixin [proj, in mathcomp.boot.choice]
SubCountable.choice_hasChoice_mixin [proj, in mathcomp.boot.choice]
SubCountable.class [proj, in mathcomp.boot.choice]
SubCountable.clone [abbrev, in mathcomp.boot.choice]
SubCountable.copy [abbrev, in mathcomp.boot.choice]
SubCountable.eqtype_hasDecEq_mixin [proj, in mathcomp.boot.choice]
SubCountable.eqtype_isSub_mixin [proj, in mathcomp.boot.choice]
SubCountable.Exports [mod, in mathcomp.boot.choice]
SubCountable.Exports.join_choice_SubCountable_between_choice_Countable_and_choice_SubChoice [def, in mathcomp.boot.choice]
SubCountable.Exports.join_choice_SubCountable_between_choice_Countable_and_eqtype_SubEquality [def, in mathcomp.boot.choice]
SubCountable.Exports.join_choice_SubCountable_between_choice_Countable_and_eqtype_SubType [def, in mathcomp.boot.choice]
SubCountable.Exports.subCountType [abbrev, in mathcomp.boot.choice]
SubCountable.on [abbrev, in mathcomp.boot.choice]
SubCountable.on_ [abbrev, in mathcomp.boot.choice]
SubCountable.pack_ [def, in mathcomp.boot.choice]
SubCountable.phant_clone [def, in mathcomp.boot.choice]
SubCountable.phant_on_ [def, in mathcomp.boot.choice]
SubCountable.sort [proj, in mathcomp.boot.choice]
SubCountable.type [rec, in mathcomp.boot.choice]
SubCountable_isFinite [abbrev, in mathcomp.boot.fintype]
SubCountable_isFinite [mod, in mathcomp.boot.fintype]
SubCountable_isFinite.axioms [abbrev, in mathcomp.boot.fintype]
SubCountable_isFinite.axioms_ [rec, in mathcomp.boot.fintype]
SubCountable_isFinite.Build [abbrev, in mathcomp.boot.fintype]
SubCountable_isFinite.Exports [mod, in mathcomp.boot.fintype]
SubCountable_isFinite.phant_axioms [def, in mathcomp.boot.fintype]
SubCountable_isFinite.phant_Build [def, in mathcomp.boot.fintype]
SubCountableElpiOperations [mod, in mathcomp.boot.choice]
subCset [prf, in mathcomp.boot.finset]
subD1set [prf, in mathcomp.boot.finset]
SubDaddsmxSpec [constr, in mathcomp.algebra.mxalgebra]
subDnAC [prf, in mathcomp.boot.ssrnat]
subDnCA [prf, in mathcomp.boot.ssrnat]
subDnCAC [prf, in mathcomp.boot.ssrnat]
subdom [abbrev, in mathcomp.finite_group.action]
subDset [prf, in mathcomp.boot.finset]
SubDsumsmxSpec [constr, in mathcomp.algebra.mxalgebra]
subEproper [prf, in mathcomp.boot.finset]
SubEquality [abbrev, in mathcomp.boot.eqtype]
SubEquality [mod, in mathcomp.boot.eqtype]
SubEquality.axioms_ [rec, in mathcomp.boot.eqtype]
SubEquality.class [proj, in mathcomp.boot.eqtype]
SubEquality.clone [abbrev, in mathcomp.boot.eqtype]
SubEquality.copy [abbrev, in mathcomp.boot.eqtype]
SubEquality.eqtype_hasDecEq_mixin [proj, in mathcomp.boot.eqtype]
SubEquality.eqtype_isSub_mixin [proj, in mathcomp.boot.eqtype]
SubEquality.Exports [mod, in mathcomp.boot.eqtype]
SubEquality.Exports.join_eqtype_SubEquality_between_eqtype_Equality_and_eqtype_SubType [def, in mathcomp.boot.eqtype]
SubEquality.Exports.subEqType [abbrev, in mathcomp.boot.eqtype]
SubEquality.on [abbrev, in mathcomp.boot.eqtype]
SubEquality.on_ [abbrev, in mathcomp.boot.eqtype]
SubEquality.pack_ [def, in mathcomp.boot.eqtype]
SubEquality.phant_clone [def, in mathcomp.boot.eqtype]
SubEquality.phant_on_ [def, in mathcomp.boot.eqtype]
SubEquality.sort [proj, in mathcomp.boot.eqtype]
SubEquality.type [rec, in mathcomp.boot.eqtype]
SubEqualityElpiOperations [mod, in mathcomp.boot.eqtype]
subfext0 [def, in mathcomp.field.fieldext]
subfext0_morph [def, in mathcomp.field.fieldext]
subfext1 [def, in mathcomp.field.fieldext]
subfext1_morph [def, in mathcomp.field.fieldext]
subfext_add [def, in mathcomp.field.fieldext]
subfext_inv [def, in mathcomp.field.fieldext]
subfext_mul [def, in mathcomp.field.fieldext]
subfext_opp [def, in mathcomp.field.fieldext]
subFExtend [def, in mathcomp.field.fieldext]
subfield_closed [prf, in mathcomp.field.fieldext]
SubFieldExtType [def, in mathcomp.field.fieldext]
SubFinite [abbrev, in mathcomp.boot.fintype]
SubFinite [mod, in mathcomp.boot.fintype]
SubFinite.axioms_ [rec, in mathcomp.boot.fintype]
SubFinite.choice_Choice_isCountable_mixin [proj, in mathcomp.boot.fintype]
SubFinite.choice_hasChoice_mixin [proj, in mathcomp.boot.fintype]
SubFinite.class [proj, in mathcomp.boot.fintype]
SubFinite.clone [abbrev, in mathcomp.boot.fintype]
SubFinite.copy [abbrev, in mathcomp.boot.fintype]
SubFinite.eqtype_hasDecEq_mixin [proj, in mathcomp.boot.fintype]
SubFinite.eqtype_isSub_mixin [proj, in mathcomp.boot.fintype]
SubFinite.Exports [mod, in mathcomp.boot.fintype]
SubFinite.Exports.join_fintype_SubFinite_between_fintype_Finite_and_choice_SubChoice [def, in mathcomp.boot.fintype]
SubFinite.Exports.join_fintype_SubFinite_between_fintype_Finite_and_choice_SubCountable [def, in mathcomp.boot.fintype]
SubFinite.Exports.join_fintype_SubFinite_between_fintype_Finite_and_eqtype_SubEquality [def, in mathcomp.boot.fintype]
SubFinite.Exports.join_fintype_SubFinite_between_fintype_Finite_and_eqtype_SubType [def, in mathcomp.boot.fintype]
SubFinite.Exports.subFinType [abbrev, in mathcomp.boot.fintype]
SubFinite.fintype_isFinite_mixin [proj, in mathcomp.boot.fintype]
SubFinite.on [abbrev, in mathcomp.boot.fintype]
SubFinite.on_ [abbrev, in mathcomp.boot.fintype]
SubFinite.pack_ [def, in mathcomp.boot.fintype]
SubFinite.phant_clone [def, in mathcomp.boot.fintype]
SubFinite.phant_on_ [def, in mathcomp.boot.fintype]
SubFinite.sort [proj, in mathcomp.boot.fintype]
SubFinite.type [rec, in mathcomp.boot.fintype]
SubFiniteElpiOperations [mod, in mathcomp.boot.fintype]
subfx_eval [def, in mathcomp.field.fieldext]
subfx_eval_is_additive [def, in mathcomp.field.fieldext]
subfx_eval_is_monoid_morphism [prf, in mathcomp.field.fieldext]
subfx_eval_is_multiplicative [def, in mathcomp.field.fieldext]
subfx_eval_is_zmod_morphism [prf, in mathcomp.field.fieldext]
subfx_eval_morph [def, in mathcomp.field.fieldext]
subfx_evalZ [prf, in mathcomp.field.fieldext]
subfx_fieldAxiom [prf, in mathcomp.field.fieldext]
subfx_inj [def, in mathcomp.field.fieldext]
subfx_inj_base [prf, in mathcomp.field.fieldext]
subfx_inj_eval [prf, in mathcomp.field.fieldext]
subfx_inj_is_additive [def, in mathcomp.field.fieldext]
subfx_inj_is_monoid_morphism [prf, in mathcomp.field.fieldext]
subfx_inj_is_multiplicative [def, in mathcomp.field.fieldext]
subfx_inj_is_zmod_morphism [prf, in mathcomp.field.fieldext]
subfx_inj_root [prf, in mathcomp.field.fieldext]
subfx_injZ [prf, in mathcomp.field.fieldext]
subfx_inv0 [prf, in mathcomp.field.fieldext]
subfx_inv_rep [def, in mathcomp.field.fieldext]
subfx_irreducibleP [prf, in mathcomp.field.fieldext]
subfx_mul_rep [def, in mathcomp.field.fieldext]
subfx_poly_inv [def, in mathcomp.field.fieldext]
subfx_root [def, in mathcomp.field.fieldext]
subfx_scale [def, in mathcomp.field.fieldext]
subfx_scaleAl [prf, in mathcomp.field.fieldext]
subfx_scaler1r [prf, in mathcomp.field.fieldext]
subfx_scalerA [prf, in mathcomp.field.fieldext]
subfx_scalerDl [prf, in mathcomp.field.fieldext]
subfx_scalerDr [prf, in mathcomp.field.fieldext]
subfxE [prf, in mathcomp.field.fieldext]
subfxEroot [prf, in mathcomp.field.fieldext]
SubfxVect [def, in mathcomp.field.fieldext]
subg [def, in mathcomp.finite_group.fingroup]
Subg [constr, in mathcomp.finite_group.fingroup]
subG1 [prf, in mathcomp.finite_group.fingroup]
subG1_contra [prf, in mathcomp.finite_group.fingroup]
subg_default [prf, in mathcomp.finite_group.fingroup]
subg_inj [prf, in mathcomp.finite_group.fingroup]
subg_inv [def, in mathcomp.finite_group.fingroup]
subg_invP [prf, in mathcomp.finite_group.fingroup]
subg_morphism [def, in mathcomp.finite_group.morphism]
subg_mul [def, in mathcomp.finite_group.fingroup]
subg_mulP [prf, in mathcomp.finite_group.fingroup]
subg_mx_abs_irr [prf, in mathcomp.group_representation.mxrepresentation]
subg_mx_faithful [prf, in mathcomp.group_representation.mxrepresentation]
subg_mx_irr [prf, in mathcomp.group_representation.mxrepresentation]
subg_mx_repr [prf, in mathcomp.group_representation.mxrepresentation]
subg_of [ind, in mathcomp.finite_group.fingroup]
subg_of_ind [scheme, in mathcomp.finite_group.fingroup]
subg_of_rec [scheme, in mathcomp.finite_group.fingroup]
subg_of_rect [scheme, in mathcomp.finite_group.fingroup]
subg_of_sind [scheme, in mathcomp.finite_group.fingroup]
subg_of_Sub [def, in mathcomp.finite_group.fingroup]
subg_one [def, in mathcomp.finite_group.fingroup]
subg_oneP [prf, in mathcomp.finite_group.fingroup]
subg_repr [def, in mathcomp.group_representation.mxrepresentation]
subgacent1E [prf, in mathcomp.finite_group.action]
subgacentE [prf, in mathcomp.finite_group.action]
subGcfker [prf, in mathcomp.group_representation.character]
subgK [prf, in mathcomp.finite_group.fingroup]
subgM [prf, in mathcomp.finite_group.fingroup]
subgmK [prf, in mathcomp.finite_group.morphism]
subgP [prf, in mathcomp.finite_group.fingroup]
SubGroup [abbrev, in mathcomp.boot.monoid]
SubGroup [mod, in mathcomp.boot.monoid]
SubGroup.axioms_ [rec, in mathcomp.boot.monoid]
SubGroup.choice_hasChoice_mixin [proj, in mathcomp.boot.monoid]
SubGroup.class [proj, in mathcomp.boot.monoid]
SubGroup.clone [abbrev, in mathcomp.boot.monoid]
SubGroup.copy [abbrev, in mathcomp.boot.monoid]
SubGroup.eqtype_hasDecEq_mixin [proj, in mathcomp.boot.monoid]
SubGroup.eqtype_isSub_mixin [proj, in mathcomp.boot.monoid]
SubGroup.Exports [mod, in mathcomp.boot.monoid]
SubGroup.Exports.join_monoid_SubGroup_between_monoid_BaseGroup_and_choice_SubChoice [def, in mathcomp.boot.monoid]
SubGroup.Exports.join_monoid_SubGroup_between_monoid_BaseGroup_and_eqtype_SubEquality [def, in mathcomp.boot.monoid]
SubGroup.Exports.join_monoid_SubGroup_between_monoid_BaseGroup_and_eqtype_SubType [def, in mathcomp.boot.monoid]
SubGroup.Exports.join_monoid_SubGroup_between_monoid_BaseGroup_and_monoid_SubBaseUMagma [def, in mathcomp.boot.monoid]
SubGroup.Exports.join_monoid_SubGroup_between_monoid_BaseGroup_and_monoid_SubMagma [def, in mathcomp.boot.monoid]
SubGroup.Exports.join_monoid_SubGroup_between_monoid_BaseGroup_and_monoid_SubMonoid [def, in mathcomp.boot.monoid]
SubGroup.Exports.join_monoid_SubGroup_between_monoid_BaseGroup_and_monoid_SubSemigroup [def, in mathcomp.boot.monoid]
SubGroup.Exports.join_monoid_SubGroup_between_monoid_BaseGroup_and_monoid_SubUMagma [def, in mathcomp.boot.monoid]
SubGroup.Exports.join_monoid_SubGroup_between_monoid_Group_and_choice_SubChoice [def, in mathcomp.boot.monoid]
SubGroup.Exports.join_monoid_SubGroup_between_monoid_Group_and_eqtype_SubEquality [def, in mathcomp.boot.monoid]
SubGroup.Exports.join_monoid_SubGroup_between_monoid_Group_and_eqtype_SubType [def, in mathcomp.boot.monoid]
SubGroup.Exports.join_monoid_SubGroup_between_monoid_Group_and_monoid_SubBaseUMagma [def, in mathcomp.boot.monoid]
SubGroup.Exports.join_monoid_SubGroup_between_monoid_Group_and_monoid_SubMagma [def, in mathcomp.boot.monoid]
SubGroup.Exports.join_monoid_SubGroup_between_monoid_Group_and_monoid_SubMonoid [def, in mathcomp.boot.monoid]
SubGroup.Exports.join_monoid_SubGroup_between_monoid_Group_and_monoid_SubSemigroup [def, in mathcomp.boot.monoid]
SubGroup.Exports.join_monoid_SubGroup_between_monoid_Group_and_monoid_SubUMagma [def, in mathcomp.boot.monoid]
SubGroup.Exports.join_monoid_SubGroup_between_monoid_StarMonoid_and_choice_SubChoice [def, in mathcomp.boot.monoid]
SubGroup.Exports.join_monoid_SubGroup_between_monoid_StarMonoid_and_eqtype_SubEquality [def, in mathcomp.boot.monoid]
SubGroup.Exports.join_monoid_SubGroup_between_monoid_StarMonoid_and_eqtype_SubType [def, in mathcomp.boot.monoid]
SubGroup.Exports.join_monoid_SubGroup_between_monoid_StarMonoid_and_monoid_SubBaseUMagma [def, in mathcomp.boot.monoid]
SubGroup.Exports.join_monoid_SubGroup_between_monoid_StarMonoid_and_monoid_SubMagma [def, in mathcomp.boot.monoid]
SubGroup.Exports.join_monoid_SubGroup_between_monoid_StarMonoid_and_monoid_SubMonoid [def, in mathcomp.boot.monoid]
SubGroup.Exports.join_monoid_SubGroup_between_monoid_StarMonoid_and_monoid_SubSemigroup [def, in mathcomp.boot.monoid]
SubGroup.Exports.join_monoid_SubGroup_between_monoid_StarMonoid_and_monoid_SubUMagma [def, in mathcomp.boot.monoid]
SubGroup.Exports.subGroupType [abbrev, in mathcomp.boot.monoid]
SubGroup.monoid_BaseUMagma_isUMagma_mixin [proj, in mathcomp.boot.monoid]
SubGroup.monoid_hasInv_mixin [proj, in mathcomp.boot.monoid]
SubGroup.monoid_hasMul_mixin [proj, in mathcomp.boot.monoid]
SubGroup.monoid_hasOne_mixin [proj, in mathcomp.boot.monoid]
SubGroup.monoid_isSubBaseUMagma_mixin [proj, in mathcomp.boot.monoid]
SubGroup.monoid_isSubMagma_mixin [proj, in mathcomp.boot.monoid]
SubGroup.monoid_Magma_isSemigroup_mixin [proj, in mathcomp.boot.monoid]
SubGroup.monoid_Monoid_isStarMonoid_mixin [proj, in mathcomp.boot.monoid]
SubGroup.monoid_StarMonoid_isGroup_mixin [proj, in mathcomp.boot.monoid]
SubGroup.on [abbrev, in mathcomp.boot.monoid]
SubGroup.on_ [abbrev, in mathcomp.boot.monoid]
SubGroup.pack_ [def, in mathcomp.boot.monoid]
SubGroup.phant_clone [def, in mathcomp.boot.monoid]
SubGroup.phant_on_ [def, in mathcomp.boot.monoid]
SubGroup.sort [proj, in mathcomp.boot.monoid]
SubGroup.type [rec, in mathcomp.boot.monoid]
subgroup_transitiveP [prf, in mathcomp.finite_group.action]
subgroup_transitivePin [prf, in mathcomp.finite_group.action]
SubGroupElpiOperations [mod, in mathcomp.boot.monoid]
subgroups [def, in mathcomp.finite_group.fingroup]
subHall_Hall [prf, in mathcomp.solvable.pgroup]
subHall_Sylow [prf, in mathcomp.solvable.pgroup]
subIset [prf, in mathcomp.boot.finset]
subitv [def, in mathcomp.algebra.interval]
subitv_anti [prf, in mathcomp.algebra.interval]
subitv_refl [prf, in mathcomp.algebra.interval]
subitv_trans [prf, in mathcomp.algebra.interval]
subitvE [prf, in mathcomp.algebra.interval]
subitvP [prf, in mathcomp.algebra.interval]
subitvPl [prf, in mathcomp.algebra.interval]
subitvPr [prf, in mathcomp.algebra.interval]
SubK [prf, in mathcomp.boot.eqtype]
subKn [prf, in mathcomp.boot.ssrnat]
subLalgType [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
subLSemiAlgType [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
SubMagma [abbrev, in mathcomp.boot.monoid]
SubMagma [mod, in mathcomp.boot.monoid]
SubMagma.axioms_ [rec, in mathcomp.boot.monoid]
SubMagma.choice_hasChoice_mixin [proj, in mathcomp.boot.monoid]
SubMagma.class [proj, in mathcomp.boot.monoid]
SubMagma.clone [abbrev, in mathcomp.boot.monoid]
SubMagma.copy [abbrev, in mathcomp.boot.monoid]
SubMagma.eqtype_hasDecEq_mixin [proj, in mathcomp.boot.monoid]
SubMagma.eqtype_isSub_mixin [proj, in mathcomp.boot.monoid]
SubMagma.Exports [mod, in mathcomp.boot.monoid]
SubMagma.Exports.join_monoid_SubMagma_between_monoid_ChoiceMagma_and_choice_SubChoice [def, in mathcomp.boot.monoid]
SubMagma.Exports.join_monoid_SubMagma_between_monoid_ChoiceMagma_and_eqtype_SubEquality [def, in mathcomp.boot.monoid]
SubMagma.Exports.join_monoid_SubMagma_between_monoid_ChoiceMagma_and_eqtype_SubType [def, in mathcomp.boot.monoid]
SubMagma.Exports.join_monoid_SubMagma_between_monoid_Magma_and_choice_SubChoice [def, in mathcomp.boot.monoid]
SubMagma.Exports.join_monoid_SubMagma_between_monoid_Magma_and_eqtype_SubEquality [def, in mathcomp.boot.monoid]
SubMagma.Exports.join_monoid_SubMagma_between_monoid_Magma_and_eqtype_SubType [def, in mathcomp.boot.monoid]
SubMagma.Exports.subMagmaType [abbrev, in mathcomp.boot.monoid]
SubMagma.monoid_hasMul_mixin [proj, in mathcomp.boot.monoid]
SubMagma.monoid_isSubMagma_mixin [proj, in mathcomp.boot.monoid]
SubMagma.on [abbrev, in mathcomp.boot.monoid]
SubMagma.on_ [abbrev, in mathcomp.boot.monoid]
SubMagma.pack_ [def, in mathcomp.boot.monoid]
SubMagma.phant_clone [def, in mathcomp.boot.monoid]
SubMagma.phant_on_ [def, in mathcomp.boot.monoid]
SubMagma.sort [proj, in mathcomp.boot.monoid]
SubMagma.type [rec, in mathcomp.boot.monoid]
SubMagmaElpiOperations [mod, in mathcomp.boot.monoid]
submod_mx [def, in mathcomp.group_representation.mxrepresentation]
submod_mx_faithful [prf, in mathcomp.group_representation.mxrepresentation]
submod_mx_irr [prf, in mathcomp.group_representation.mxrepresentation]
submod_mx_repr [prf, in mathcomp.group_representation.mxrepresentation]
submod_repr [def, in mathcomp.group_representation.mxrepresentation]
SubMonoid [abbrev, in mathcomp.boot.monoid]
SubMonoid [mod, in mathcomp.boot.monoid]
SubMonoid.axioms_ [rec, in mathcomp.boot.monoid]
SubMonoid.choice_hasChoice_mixin [proj, in mathcomp.boot.monoid]
SubMonoid.class [proj, in mathcomp.boot.monoid]
SubMonoid.clone [abbrev, in mathcomp.boot.monoid]
SubMonoid.copy [abbrev, in mathcomp.boot.monoid]
SubMonoid.eqtype_hasDecEq_mixin [proj, in mathcomp.boot.monoid]
SubMonoid.eqtype_isSub_mixin [proj, in mathcomp.boot.monoid]
SubMonoid.Exports [mod, in mathcomp.boot.monoid]
SubMonoid.Exports.join_monoid_SubMonoid_between_monoid_BaseUMagma_and_monoid_SubSemigroup [def, in mathcomp.boot.monoid]
SubMonoid.Exports.join_monoid_SubMonoid_between_monoid_ChoiceBaseUMagma_and_monoid_SubSemigroup [def, in mathcomp.boot.monoid]
SubMonoid.Exports.join_monoid_SubMonoid_between_monoid_Monoid_and_choice_SubChoice [def, in mathcomp.boot.monoid]
SubMonoid.Exports.join_monoid_SubMonoid_between_monoid_Monoid_and_eqtype_SubEquality [def, in mathcomp.boot.monoid]
SubMonoid.Exports.join_monoid_SubMonoid_between_monoid_Monoid_and_eqtype_SubType [def, in mathcomp.boot.monoid]
SubMonoid.Exports.join_monoid_SubMonoid_between_monoid_Monoid_and_monoid_SubBaseUMagma [def, in mathcomp.boot.monoid]
SubMonoid.Exports.join_monoid_SubMonoid_between_monoid_Monoid_and_monoid_SubMagma [def, in mathcomp.boot.monoid]
SubMonoid.Exports.join_monoid_SubMonoid_between_monoid_Monoid_and_monoid_SubSemigroup [def, in mathcomp.boot.monoid]
SubMonoid.Exports.join_monoid_SubMonoid_between_monoid_Monoid_and_monoid_SubUMagma [def, in mathcomp.boot.monoid]
SubMonoid.Exports.join_monoid_SubMonoid_between_monoid_Semigroup_and_monoid_SubBaseUMagma [def, in mathcomp.boot.monoid]
SubMonoid.Exports.join_monoid_SubMonoid_between_monoid_Semigroup_and_monoid_SubUMagma [def, in mathcomp.boot.monoid]
SubMonoid.Exports.join_monoid_SubMonoid_between_monoid_SubBaseUMagma_and_monoid_SubSemigroup [def, in mathcomp.boot.monoid]
SubMonoid.Exports.join_monoid_SubMonoid_between_monoid_SubSemigroup_and_monoid_SubUMagma [def, in mathcomp.boot.monoid]
SubMonoid.Exports.join_monoid_SubMonoid_between_monoid_SubSemigroup_and_monoid_UMagma [def, in mathcomp.boot.monoid]
SubMonoid.Exports.subMonoidType [abbrev, in mathcomp.boot.monoid]
SubMonoid.monoid_BaseUMagma_isUMagma_mixin [proj, in mathcomp.boot.monoid]
SubMonoid.monoid_hasMul_mixin [proj, in mathcomp.boot.monoid]
SubMonoid.monoid_hasOne_mixin [proj, in mathcomp.boot.monoid]
SubMonoid.monoid_isSubBaseUMagma_mixin [proj, in mathcomp.boot.monoid]
SubMonoid.monoid_isSubMagma_mixin [proj, in mathcomp.boot.monoid]
SubMonoid.monoid_Magma_isSemigroup_mixin [proj, in mathcomp.boot.monoid]
SubMonoid.on [abbrev, in mathcomp.boot.monoid]
SubMonoid.on_ [abbrev, in mathcomp.boot.monoid]
SubMonoid.pack_ [def, in mathcomp.boot.monoid]
SubMonoid.phant_clone [def, in mathcomp.boot.monoid]
SubMonoid.phant_on_ [def, in mathcomp.boot.monoid]
SubMonoid.sort [proj, in mathcomp.boot.monoid]
SubMonoid.type [rec, in mathcomp.boot.monoid]
SubMonoidElpiOperations [mod, in mathcomp.boot.monoid]
submx [abbrev, in mathcomp.algebra.mxalgebra]
submx [mod, in mathcomp.algebra.mxalgebra]
submx.body [def, in mathcomp.algebra.mxalgebra]
submx.unlock [def, in mathcomp.algebra.mxalgebra]
submx0 [prf, in mathcomp.algebra.mxalgebra]
submx0null [prf, in mathcomp.algebra.mxalgebra]
submx1 [prf, in mathcomp.algebra.mxalgebra]
submx_full [prf, in mathcomp.algebra.mxalgebra]
submx_Locked [modtype, in mathcomp.algebra.mxalgebra]
submx_Locked.body [ax, in mathcomp.algebra.mxalgebra]
submx_Locked.unlock [ax, in mathcomp.algebra.mxalgebra]
submx_ortho [prf, in mathcomp.algebra.spectral]
submx_refl [prf, in mathcomp.algebra.mxalgebra]
submx_rowsub [prf, in mathcomp.algebra.mxalgebra]
submx_trans [prf, in mathcomp.algebra.mxalgebra]
submx_unlock_subterm [def, in mathcomp.algebra.mxalgebra]
submx_unlockable [def, in mathcomp.algebra.mxalgebra]
submxblock [def, in mathcomp.algebra.matrix]
submxblock0 [prf, in mathcomp.algebra.matrix]
submxblock_diag [prf, in mathcomp.algebra.matrix]
submxblock_sum [prf, in mathcomp.algebra.matrix]
submxblockB [prf, in mathcomp.algebra.matrix]
submxblockD [prf, in mathcomp.algebra.matrix]
submxblockEh [prf, in mathcomp.algebra.matrix]
submxblockEv [prf, in mathcomp.algebra.matrix]
submxblockK [prf, in mathcomp.algebra.matrix]
submxblockN [prf, in mathcomp.algebra.matrix]
submxcol [def, in mathcomp.algebra.matrix]
submxcol0 [prf, in mathcomp.algebra.matrix]
submxcol_matrix [prf, in mathcomp.algebra.matrix]
submxcol_mul [prf, in mathcomp.algebra.matrix]
submxcol_sum [prf, in mathcomp.algebra.matrix]
submxcolB [prf, in mathcomp.algebra.matrix]
submxcolD [prf, in mathcomp.algebra.matrix]
submxcolK [prf, in mathcomp.algebra.matrix]
submxcolN [prf, in mathcomp.algebra.matrix]
submxE [prf, in mathcomp.algebra.mxalgebra]
submxElt [prf, in mathcomp.algebra.mxalgebra]
submxK [prf, in mathcomp.algebra.matrix]
submxMfree [prf, in mathcomp.algebra.mxalgebra]
submxMl [prf, in mathcomp.algebra.mxalgebra]
submxMr [prf, in mathcomp.algebra.mxalgebra]
submxP [prf, in mathcomp.algebra.mxalgebra]
submxrow [def, in mathcomp.algebra.matrix]
submxrow0 [prf, in mathcomp.algebra.matrix]
submxrow_matrix [prf, in mathcomp.algebra.matrix]
submxrow_sum [prf, in mathcomp.algebra.matrix]
submxrowB [prf, in mathcomp.algebra.matrix]
submxrowD [prf, in mathcomp.algebra.matrix]
submxrowK [prf, in mathcomp.algebra.matrix]
submxrowN [prf, in mathcomp.algebra.matrix]
subn [def, in mathcomp.boot.ssrnat]
subn0 [prf, in mathcomp.boot.ssrnat]
subn1 [prf, in mathcomp.boot.ssrnat]
subn2 [prf, in mathcomp.boot.ssrnat]
subn_eq0 [prf, in mathcomp.boot.ssrnat]
subn_exp [prf, in mathcomp.boot.binomial]
subn_gt0 [prf, in mathcomp.boot.ssrnat]
subn_if_gt [prf, in mathcomp.boot.ssrnat]
subn_maxl [prf, in mathcomp.boot.ssrnat]
subn_minl [prf, in mathcomp.boot.ssrnat]
subn_rec [def, in mathcomp.boot.ssrnat]
subn_sqr [prf, in mathcomp.boot.ssrnat]
subnA [prf, in mathcomp.boot.ssrnat]
subnAC [prf, in mathcomp.boot.ssrnat]
subnBA [prf, in mathcomp.boot.ssrnat]
subnBAC [prf, in mathcomp.boot.ssrnat]
subnBl_leq [prf, in mathcomp.boot.ssrnat]
subnBr_leq [prf, in mathcomp.boot.ssrnat]
subnCBA [prf, in mathcomp.boot.ssrnat]
subnDA [prf, in mathcomp.boot.ssrnat]
subnDAC [prf, in mathcomp.boot.ssrnat]
subnDl [prf, in mathcomp.boot.ssrnat]
subnDr [prf, in mathcomp.boot.ssrnat]
subnE [prf, in mathcomp.boot.ssrnat]
subnK [prf, in mathcomp.boot.ssrnat]
subnKC [prf, in mathcomp.boot.ssrnat]
subnn [prf, in mathcomp.boot.ssrnat]
subnormal [def, in mathcomp.solvable.gseries]
subnormal_refl [prf, in mathcomp.solvable.gseries]
subnormal_sub [prf, in mathcomp.solvable.gseries]
subnormal_trans [prf, in mathcomp.solvable.gseries]
subnormalEl [prf, in mathcomp.solvable.gseries]
subnormalEr [prf, in mathcomp.solvable.gseries]
subnormalEsupport [prf, in mathcomp.solvable.gseries]
subnormalP [prf, in mathcomp.solvable.gseries]
subnS [prf, in mathcomp.boot.ssrnat]
subnSK [prf, in mathcomp.boot.ssrnat]
SubP [prf, in mathcomp.boot.eqtype]
subq [def, in mathcomp.algebra.rat]
subq_ge0 [prf, in mathcomp.algebra.rat]
subRingType [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
subSemiAlgType [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
SubSemigroup [abbrev, in mathcomp.boot.monoid]
SubSemigroup [mod, in mathcomp.boot.monoid]
SubSemigroup.axioms_ [rec, in mathcomp.boot.monoid]
SubSemigroup.choice_hasChoice_mixin [proj, in mathcomp.boot.monoid]
SubSemigroup.class [proj, in mathcomp.boot.monoid]
SubSemigroup.clone [abbrev, in mathcomp.boot.monoid]
SubSemigroup.copy [abbrev, in mathcomp.boot.monoid]
SubSemigroup.eqtype_hasDecEq_mixin [proj, in mathcomp.boot.monoid]
SubSemigroup.eqtype_isSub_mixin [proj, in mathcomp.boot.monoid]
SubSemigroup.Exports [mod, in mathcomp.boot.monoid]
SubSemigroup.Exports.join_monoid_SubSemigroup_between_monoid_Semigroup_and_choice_SubChoice [def, in mathcomp.boot.monoid]
SubSemigroup.Exports.join_monoid_SubSemigroup_between_monoid_Semigroup_and_eqtype_SubEquality [def, in mathcomp.boot.monoid]
SubSemigroup.Exports.join_monoid_SubSemigroup_between_monoid_Semigroup_and_eqtype_SubType [def, in mathcomp.boot.monoid]
SubSemigroup.Exports.join_monoid_SubSemigroup_between_monoid_Semigroup_and_monoid_SubMagma [def, in mathcomp.boot.monoid]
SubSemigroup.Exports.subSemigroupType [abbrev, in mathcomp.boot.monoid]
SubSemigroup.monoid_hasMul_mixin [proj, in mathcomp.boot.monoid]
SubSemigroup.monoid_isSubMagma_mixin [proj, in mathcomp.boot.monoid]
SubSemigroup.monoid_Magma_isSemigroup_mixin [proj, in mathcomp.boot.monoid]
SubSemigroup.on [abbrev, in mathcomp.boot.monoid]
SubSemigroup.on_ [abbrev, in mathcomp.boot.monoid]
SubSemigroup.pack_ [def, in mathcomp.boot.monoid]
SubSemigroup.phant_clone [def, in mathcomp.boot.monoid]
SubSemigroup.phant_on_ [def, in mathcomp.boot.monoid]
SubSemigroup.sort [proj, in mathcomp.boot.monoid]
SubSemigroup.type [rec, in mathcomp.boot.monoid]
SubSemigroupElpiOperations [mod, in mathcomp.boot.monoid]
subSemiRingType [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
subseq [def, in mathcomp.boot.seq]
subseq0 [prf, in mathcomp.boot.seq]
subseq_anti [prf, in mathcomp.boot.seq]
subseq_cat2l [prf, in mathcomp.boot.seq]
subseq_cat2r [prf, in mathcomp.boot.seq]
subseq_cons [prf, in mathcomp.boot.seq]
subseq_filter [prf, in mathcomp.boot.seq]
subseq_pairwise [prf, in mathcomp.boot.seq]
subseq_path [prf, in mathcomp.boot.path]
subseq_path_in [prf, in mathcomp.boot.path]
subseq_rcons [prf, in mathcomp.boot.seq]
subseq_refl [prf, in mathcomp.boot.seq]
subseq_rem [prf, in mathcomp.boot.seq]
subseq_rev [prf, in mathcomp.boot.seq]
subseq_rot [prf, in mathcomp.boot.seq]
subseq_sort [prf, in mathcomp.boot.path]
subseq_sort_in [prf, in mathcomp.boot.path]
subseq_sorted [prf, in mathcomp.boot.path]
subseq_sorted_in [prf, in mathcomp.boot.path]
subseq_trans [prf, in mathcomp.boot.seq]
subseq_uniq [prf, in mathcomp.boot.seq]
subseq_uniqP [prf, in mathcomp.boot.seq]
subseqP [prf, in mathcomp.boot.seq]
subseries_repr [def, in mathcomp.group_representation.mxrepresentation]
subset [abbrev, in mathcomp.boot.fintype]
subset [mod, in mathcomp.boot.fintype]
subset.body [def, in mathcomp.boot.fintype]
subset.unlock [def, in mathcomp.boot.fintype]
subset0 [prf, in mathcomp.boot.finset]
subset1 [prf, in mathcomp.boot.finset]
subset_all [prf, in mathcomp.boot.fintype]
subset_cardP [prf, in mathcomp.boot.fintype]
subset_cat2 [prf, in mathcomp.boot.fintype]
subset_catl [prf, in mathcomp.boot.fintype]
subset_catr [prf, in mathcomp.boot.fintype]
subset_closure [prf, in mathcomp.boot.fingraph]
subset_cons [prf, in mathcomp.boot.seq]
subset_cons [prf, in mathcomp.boot.fintype]
subset_cons2 [prf, in mathcomp.boot.seq]
subset_cons2 [prf, in mathcomp.boot.fintype]
subset_cover [prf, in mathcomp.boot.finset]
subset_dfs [prf, in mathcomp.boot.fingraph]
subset_disjoint [prf, in mathcomp.boot.fintype]
subset_eqP [prf, in mathcomp.boot.fintype]
subset_faithful [prf, in mathcomp.finite_group.action]
subset_filter [prf, in mathcomp.boot.fintype]
subset_gen [prf, in mathcomp.finite_group.fingroup]
subset_iter [prf, in mathcomp.boot.finset]
subset_iterS [prf, in mathcomp.boot.finset]
subset_itv [prf, in mathcomp.algebra.interval]
subset_itv_bound [prf, in mathcomp.algebra.interval]
subset_itv_co_cc [prf, in mathcomp.algebra.interval]
subset_itv_oc_cc [prf, in mathcomp.algebra.interval]
subset_itv_oo_cc [prf, in mathcomp.algebra.interval]
subset_itv_oo_co [prf, in mathcomp.algebra.interval]
subset_itv_oo_oc [prf, in mathcomp.algebra.interval]
subset_le_big [prf, in mathcomp.boot.bigop]
subset_le_big_cond [prf, in mathcomp.boot.finset]
subset_leq_card [prf, in mathcomp.boot.fintype]
subset_leqif_card [prf, in mathcomp.boot.fintype]
subset_leqif_cards [prf, in mathcomp.boot.finset]
subset_limgP [prf, in mathcomp.algebra.vector]
subset_Locked [modtype, in mathcomp.boot.fintype]
subset_Locked.body [ax, in mathcomp.boot.fintype]
subset_Locked.unlock [ax, in mathcomp.boot.fintype]
subset_mapP [prf, in mathcomp.boot.seq]
subset_memP [prf, in mathcomp.boot.seq]
subset_neq0 [prf, in mathcomp.boot.finset]
subset_pred1 [prf, in mathcomp.boot.fintype]
subset_predT [prf, in mathcomp.boot.fintype]
subset_trans [prf, in mathcomp.boot.fintype]
subset_unlock [def, in mathcomp.boot.fintype]
subset_unlock_subterm [def, in mathcomp.boot.fintype]
subsetC [prf, in mathcomp.boot.finset]
subsetC_disjoint [prf, in mathcomp.boot.finset]
subsetD [prf, in mathcomp.boot.finset]
subsetD1 [prf, in mathcomp.boot.finset]
subsetD1P [prf, in mathcomp.boot.finset]
subsetDl [prf, in mathcomp.boot.finset]
subsetDP [prf, in mathcomp.boot.finset]
subsetDr [prf, in mathcomp.boot.finset]
subsetE [prf, in mathcomp.boot.fintype]
subsetI [prf, in mathcomp.boot.finset]
subsetIidl [prf, in mathcomp.boot.finset]
subsetIidr [prf, in mathcomp.boot.finset]
subsetIl [prf, in mathcomp.boot.finset]
subsetIP [prf, in mathcomp.boot.finset]
subsetIr [prf, in mathcomp.boot.finset]
subsetP [prf, in mathcomp.boot.fintype]
subsetPn [prf, in mathcomp.boot.fintype]
subsets_disjoint [prf, in mathcomp.boot.finset]
subsetT [prf, in mathcomp.boot.finset]
subsetT_hint [prf, in mathcomp.boot.finset]
subsetU [prf, in mathcomp.boot.finset]
subsetU1 [prf, in mathcomp.boot.finset]
subsetUl [prf, in mathcomp.boot.finset]
subsetUr [prf, in mathcomp.boot.finset]
subsetv [def, in mathcomp.algebra.vector]
subSKn [prf, in mathcomp.boot.ssrnat]
subSn [prf, in mathcomp.boot.ssrnat]
subSnn [prf, in mathcomp.boot.ssrnat]
subSocle_direct [prf, in mathcomp.group_representation.mxrepresentation]
subSocle_iso [prf, in mathcomp.group_representation.mxrepresentation]
subSocle_module [prf, in mathcomp.group_representation.mxrepresentation]
subSocle_semisimple [prf, in mathcomp.group_representation.mxrepresentation]
subSpec [constr, in mathcomp.boot.eqtype]
subSS [prf, in mathcomp.boot.ssrnat]
subTset [prf, in mathcomp.boot.finset]
SubType [abbrev, in mathcomp.boot.eqtype]
SubType [mod, in mathcomp.boot.eqtype]
SubType.axioms_ [rec, in mathcomp.boot.eqtype]
SubType.class [proj, in mathcomp.boot.eqtype]
SubType.clone [abbrev, in mathcomp.boot.eqtype]
SubType.copy [abbrev, in mathcomp.boot.eqtype]
SubType.eqtype_isSub_mixin [proj, in mathcomp.boot.eqtype]
SubType.Exports [mod, in mathcomp.boot.eqtype]
SubType.Exports.subType [abbrev, in mathcomp.boot.eqtype]
SubType.on [abbrev, in mathcomp.boot.eqtype]
SubType.on_ [abbrev, in mathcomp.boot.eqtype]
SubType.pack_ [def, in mathcomp.boot.eqtype]
SubType.phant_clone [def, in mathcomp.boot.eqtype]
SubType.phant_on_ [def, in mathcomp.boot.eqtype]
SubType.sort [proj, in mathcomp.boot.eqtype]
SubType.type [rec, in mathcomp.boot.eqtype]
SubTypeElpiOperations [mod, in mathcomp.boot.eqtype]
SubUMagma [abbrev, in mathcomp.boot.monoid]
SubUMagma [mod, in mathcomp.boot.monoid]
SubUMagma.axioms_ [rec, in mathcomp.boot.monoid]
SubUMagma.choice_hasChoice_mixin [proj, in mathcomp.boot.monoid]
SubUMagma.class [proj, in mathcomp.boot.monoid]
SubUMagma.clone [abbrev, in mathcomp.boot.monoid]
SubUMagma.copy [abbrev, in mathcomp.boot.monoid]
SubUMagma.eqtype_hasDecEq_mixin [proj, in mathcomp.boot.monoid]
SubUMagma.eqtype_isSub_mixin [proj, in mathcomp.boot.monoid]
SubUMagma.Exports [mod, in mathcomp.boot.monoid]
SubUMagma.Exports.join_monoid_SubUMagma_between_choice_SubChoice_and_monoid_UMagma [def, in mathcomp.boot.monoid]
SubUMagma.Exports.join_monoid_SubUMagma_between_eqtype_SubEquality_and_monoid_UMagma [def, in mathcomp.boot.monoid]
SubUMagma.Exports.join_monoid_SubUMagma_between_eqtype_SubType_and_monoid_UMagma [def, in mathcomp.boot.monoid]
SubUMagma.Exports.join_monoid_SubUMagma_between_monoid_SubBaseUMagma_and_monoid_UMagma [def, in mathcomp.boot.monoid]
SubUMagma.Exports.join_monoid_SubUMagma_between_monoid_SubMagma_and_monoid_UMagma [def, in mathcomp.boot.monoid]
SubUMagma.Exports.subUMagmaType [abbrev, in mathcomp.boot.monoid]
SubUMagma.monoid_BaseUMagma_isUMagma_mixin [proj, in mathcomp.boot.monoid]
SubUMagma.monoid_hasMul_mixin [proj, in mathcomp.boot.monoid]
SubUMagma.monoid_hasOne_mixin [proj, in mathcomp.boot.monoid]
SubUMagma.monoid_isSubBaseUMagma_mixin [proj, in mathcomp.boot.monoid]
SubUMagma.monoid_isSubMagma_mixin [proj, in mathcomp.boot.monoid]
SubUMagma.on [abbrev, in mathcomp.boot.monoid]
SubUMagma.on_ [abbrev, in mathcomp.boot.monoid]
SubUMagma.pack_ [def, in mathcomp.boot.monoid]
SubUMagma.phant_clone [def, in mathcomp.boot.monoid]
SubUMagma.phant_on_ [def, in mathcomp.boot.monoid]
SubUMagma.sort [proj, in mathcomp.boot.monoid]
SubUMagma.type [rec, in mathcomp.boot.monoid]
SubUMagmaElpiOperations [mod, in mathcomp.boot.monoid]
subUset [prf, in mathcomp.boot.finset]
subUsetP [prf, in mathcomp.boot.finset]
subV [abbrev, in mathcomp.algebra.vector]
subv0 [prf, in mathcomp.algebra.vector]
subv_add [prf, in mathcomp.algebra.vector]
subv_adjoin [prf, in mathcomp.field.falgebra]
subv_adjoin_seq [prf, in mathcomp.field.falgebra]
subv_anti [prf, in mathcomp.algebra.vector]
subv_bigcapP [prf, in mathcomp.algebra.vector]
subv_cap [prf, in mathcomp.algebra.vector]
subv_cent1 [prf, in mathcomp.field.falgebra]
subv_sumP [prf, in mathcomp.algebra.vector]
subv_trans [prf, in mathcomp.algebra.vector]
SubVectType [def, in mathcomp.field.fieldext]
subvf [prf, in mathcomp.algebra.vector]
subvP [prf, in mathcomp.algebra.vector]
subvP_adjoin [prf, in mathcomp.field.falgebra]
subvPn [prf, in mathcomp.algebra.vector]
Subvs [constr, in mathcomp.algebra.vector]
subvs_fieldMixin [prf, in mathcomp.field.fieldext]
subvs_inj [prf, in mathcomp.algebra.vector]
subvs_mu1l [prf, in mathcomp.field.falgebra]
subvs_mul [def, in mathcomp.field.falgebra]
subvs_mul1 [prf, in mathcomp.field.falgebra]
subvs_mulA [prf, in mathcomp.field.falgebra]
subvs_mulDl [prf, in mathcomp.field.falgebra]
subvs_mulDr [prf, in mathcomp.field.falgebra]
subvs_of [ind, in mathcomp.algebra.vector]
subvs_of_ind [scheme, in mathcomp.algebra.vector]
subvs_of_rec [scheme, in mathcomp.algebra.vector]
subvs_of_rect [scheme, in mathcomp.algebra.vector]
subvs_of_sind [scheme, in mathcomp.algebra.vector]
subvs_one [def, in mathcomp.field.falgebra]
subvs_scaleAl [prf, in mathcomp.field.falgebra]
subvs_scaleAr [prf, in mathcomp.field.falgebra]
subvs_vect_iso [prf, in mathcomp.algebra.vector]
SubvsE [prf, in mathcomp.algebra.vector]
subvsP [prf, in mathcomp.algebra.vector]
subvv [prf, in mathcomp.algebra.vector]
subX_agenv [prf, in mathcomp.field.falgebra]
subxx [prf, in mathcomp.boot.fintype]
subxx_hint [prf, in mathcomp.boot.fintype]
subzn [prf, in mathcomp.algebra.ssrint]
subzSS [prf, in mathcomp.algebra.ssrint]
succn [abbrev, in mathcomp.boot.ssrnat]
succn_inj [prf, in mathcomp.boot.ssrnat]
succnK [prf, in mathcomp.boot.ssrnat]
suffix [def, in mathcomp.boot.seq]
suffix0s [prf, in mathcomp.boot.seq]
suffix1s [prf, in mathcomp.boot.seq]
suffix_catl [prf, in mathcomp.boot.seq]
suffix_catr [prf, in mathcomp.boot.seq]
suffix_cons [prf, in mathcomp.boot.seq]
suffix_drop [prf, in mathcomp.boot.seq]
suffix_infix [prf, in mathcomp.boot.seq]
suffix_infix_trans [prf, in mathcomp.boot.seq]
suffix_prefix_trans [prf, in mathcomp.boot.seq]
suffix_rcons [prf, in mathcomp.boot.seq]
suffix_refl [prf, in mathcomp.boot.seq]
suffix_rev [prf, in mathcomp.boot.seq]
suffix_revLR [prf, in mathcomp.boot.seq]
suffix_sorted [prf, in mathcomp.boot.path]
suffix_subseq [prf, in mathcomp.boot.seq]
suffix_suffix [prf, in mathcomp.boot.seq]
suffix_trans [prf, in mathcomp.boot.seq]
suffix_uniq [prf, in mathcomp.boot.seq]
suffixE [prf, in mathcomp.boot.seq]
suffixP [prf, in mathcomp.boot.seq]
suffixs0 [prf, in mathcomp.boot.seq]
suffixW [prf, in mathcomp.boot.seq]
sum1_card [prf, in mathcomp.boot.bigop]
sum1_count [prf, in mathcomp.boot.bigop]
sum1_size [prf, in mathcomp.boot.bigop]
sum1dep_card [prf, in mathcomp.boot.finset]
sum_by_classes [prf, in mathcomp.group_representation.classfun]
sum_card_class [prf, in mathcomp.finite_group.action]
sum_cfunE [prf, in mathcomp.group_representation.classfun]
sum_drop_poly [prf, in mathcomp.algebra.poly]
sum_enum [def, in mathcomp.boot.fintype]
sum_enum_uniq [prf, in mathcomp.boot.fintype]
sum_eq [def, in mathcomp.boot.eqtype]
sum_eqE [prf, in mathcomp.boot.eqtype]
sum_eqP [prf, in mathcomp.boot.eqtype]
sum_even_poly [prf, in mathcomp.algebra.poly]
sum_ffun [prf, in mathcomp.boot.nmodule]
sum_ffun [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
sum_ffunE [prf, in mathcomp.boot.nmodule]
sum_ffunE [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
sum_index_rcosets_cycle [prf, in mathcomp.solvable.finmodule]
sum_irr_degree [abbrev, in mathcomp.group_representation.mxrepresentation]
sum_irr_degree_pchar [prf, in mathcomp.group_representation.mxrepresentation]
sum_isFinite [def, in mathcomp.boot.fintype]
sum_lfunE [prf, in mathcomp.algebra.vector]
sum_mxsimple_direct_compl [prf, in mathcomp.group_representation.mxrepresentation]
sum_mxsimple_direct_sub [prf, in mathcomp.group_representation.mxrepresentation]
sum_mxsum [def, in mathcomp.algebra.mxalgebra]
sum_nat_cond_const [prf, in mathcomp.boot.finset]
sum_nat_const [prf, in mathcomp.boot.bigop]
sum_nat_const_nat [prf, in mathcomp.boot.bigop]
sum_nat_eq0 [prf, in mathcomp.boot.bigop]
sum_nat_eq1 [prf, in mathcomp.boot.bigop]
sum_nat_seq_eq0 [prf, in mathcomp.boot.bigop]
sum_nat_seq_eq1 [prf, in mathcomp.boot.bigop]
sum_nat_seq_neq0 [prf, in mathcomp.boot.bigop]
sum_ncycle_totient [prf, in mathcomp.solvable.cyclic]
sum_norm2_char_generators [prf, in mathcomp.group_representation.integral_char]
sum_norm_irr_quo [prf, in mathcomp.group_representation.character]
sum_odd_poly [prf, in mathcomp.algebra.poly]
sum_of_opair [def, in mathcomp.boot.choice]
sum_totient_dvd [prf, in mathcomp.solvable.cyclic]
sumfv [prf, in mathcomp.algebra.vector]
sumKx [abbrev, in mathcomp.field.fieldext]
summx_sub [prf, in mathcomp.algebra.mxalgebra]
summx_sub_sums [prf, in mathcomp.algebra.mxalgebra]
summxE [prf, in mathcomp.algebra.matrix]
sumMz [prf, in mathcomp.algebra.ssrint]
sumn [def, in mathcomp.boot.seq]
sumn_cat [prf, in mathcomp.boot.seq]
sumn_count [prf, in mathcomp.boot.seq]
sumn_flatten [prf, in mathcomp.boot.seq]
sumn_ncons [prf, in mathcomp.boot.seq]
sumn_nseq [prf, in mathcomp.boot.seq]
sumn_rcons [prf, in mathcomp.boot.seq]
sumn_rev [prf, in mathcomp.boot.seq]
sumn_rot [prf, in mathcomp.boot.seq]
sumn_set_nth [prf, in mathcomp.boot.seq]
sumn_set_nth0 [prf, in mathcomp.boot.seq]
sumn_set_nth_ltn [prf, in mathcomp.boot.seq]
sumnB [prf, in mathcomp.boot.bigop]
sumnE [prf, in mathcomp.boot.bigop]
sumsmx_module [prf, in mathcomp.group_representation.mxrepresentation]
sumsmx_semisimple [prf, in mathcomp.group_representation.mxrepresentation]
sumsmx_subP [prf, in mathcomp.algebra.mxalgebra]
sumsmx_sup [prf, in mathcomp.algebra.mxalgebra]
sumsmxMr [prf, in mathcomp.algebra.mxalgebra]
sumsmxMr_gen [prf, in mathcomp.algebra.mxalgebra]
sumsmxS [prf, in mathcomp.algebra.mxalgebra]
sumV [abbrev, in mathcomp.algebra.vector]
sumv_pi [abbrev, in mathcomp.algebra.vector]
sumv_pi_for [def, in mathcomp.algebra.vector]
sumv_pi_nat_sum [prf, in mathcomp.algebra.vector]
sumv_pi_sum [prf, in mathcomp.algebra.vector]
sumv_pi_uniq_sum [prf, in mathcomp.algebra.vector]
sumv_sup [prf, in mathcomp.algebra.vector]
sup_field_module [prf, in mathcomp.field.fieldext]
support [abbrev, in mathcomp.boot.nmodule]
support [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
support_cfAut [prf, in mathcomp.group_representation.classfun]
support_cfun [prf, in mathcomp.group_representation.classfun]
support_cfuni [prf, in mathcomp.group_representation.classfun]
support_for [def, in mathcomp.boot.finfun]
support_zchar [prf, in mathcomp.group_representation.vcharacter]
supportE [prf, in mathcomp.boot.finfun]
supportP [prf, in mathcomp.boot.finfun]
sv [def, in mathcomp.solvable.burnside_app]
Sv [def, in mathcomp.solvable.burnside_app]
Sv_inj [prf, in mathcomp.solvable.burnside_app]
sv_inv [prf, in mathcomp.solvable.burnside_app]
swap_pair [def, in mathcomp.boot.ssrfun]
swap_pairK [prf, in mathcomp.boot.ssrfun]
swapXY [def, in mathcomp.algebra.polyXY]
swapXY_comp_poly [prf, in mathcomp.algebra.polyXY]
swapXY_def [def, in mathcomp.algebra.polyXY]
swapXY_eq0 [prf, in mathcomp.algebra.polyXY]
swapXY_is_additive [def, in mathcomp.algebra.polyXY]
swapXY_is_monoid_morphism [prf, in mathcomp.algebra.polyXY]
swapXY_is_multiplicative [def, in mathcomp.algebra.polyXY]
swapXY_is_scalable [prf, in mathcomp.algebra.polyXY]
swapXY_is_zmod_morphism [prf, in mathcomp.algebra.polyXY]
swapXY_key [prf, in mathcomp.algebra.polyXY]
swapXY_map [prf, in mathcomp.algebra.polyXY]
swapXY_map_polyC [prf, in mathcomp.algebra.polyXY]
swapXY_poly_XaY [prf, in mathcomp.algebra.polyXY]
swapXY_poly_XmY [prf, in mathcomp.algebra.polyXY]
swapXY_polyC [prf, in mathcomp.algebra.polyXY]
swapXY_unlockable [def, in mathcomp.algebra.polyXY]
swapXY_X [prf, in mathcomp.algebra.polyXY]
swapXY_Y [prf, in mathcomp.algebra.polyXY]
swapXYK [prf, in mathcomp.algebra.polyXY]
swizzle_mx [def, in mathcomp.algebra.matrix]
swizzle_mx_is_additive [def, in mathcomp.algebra.matrix]
swizzle_mx_is_nmod_morphism [prf, in mathcomp.algebra.matrix]
swizzle_mx_is_scalable [prf, in mathcomp.algebra.matrix]
swizzle_mx_is_semi_additive [def, in mathcomp.algebra.matrix]
swizzle_mx_is_zmod_morphism [prf, in mathcomp.algebra.matrix]
SwizzleAdd [abbrev, in mathcomp.algebra.matrix]
SwizzleLin [abbrev, in mathcomp.algebra.matrix]
Syl [def, in mathcomp.solvable.pgroup]
Syl_trans [prf, in mathcomp.solvable.sylow]
sylow [file, in mathcomp.solvable.sylow]
Sylow [def, in mathcomp.solvable.pgroup]
Sylow's_theorem [prf, in mathcomp.solvable.sylow]
Sylow1 [prf, in mathcomp.solvable.pgroup]
Sylow_exists [prf, in mathcomp.solvable.sylow]
Sylow_gen [prf, in mathcomp.solvable.sylow]
Sylow_Jsub [prf, in mathcomp.solvable.sylow]
Sylow_setI_normal [prf, in mathcomp.solvable.sylow]
Sylow_subJ [prf, in mathcomp.solvable.sylow]
Sylow_subnorm [prf, in mathcomp.solvable.sylow]
Sylow_superset [prf, in mathcomp.solvable.sylow]
Sylow_trans [prf, in mathcomp.solvable.sylow]
Sylow_transversal_gen [prf, in mathcomp.solvable.sylow]
SylowJ [prf, in mathcomp.solvable.pgroup]
SylowP [prf, in mathcomp.solvable.pgroup]
Sylvester_mx [def, in mathcomp.algebra.mxpoly]
Sylvester_mxE [prf, in mathcomp.algebra.mxpoly]
Sym [def, in mathcomp.solvable.alt]
Sym [def, in mathcomp.finite_group.perm]
sym_connect_sym [prf, in mathcomp.boot.fingraph]
Sym_group [def, in mathcomp.solvable.alt]
Sym_group [def, in mathcomp.finite_group.perm]
Sym_group_set [prf, in mathcomp.finite_group.perm]
Sym_trans [prf, in mathcomp.solvable.alt]
SymE [prf, in mathcomp.finite_group.action]
symmetric_form [abbrev, in mathcomp.algebra.sesquilinear]
symmetric_normalmx [prf, in mathcomp.algebra.spectral]
symmetricmx [abbrev, in mathcomp.algebra.sesquilinear]
symplectic_type_group_structure [prf, in mathcomp.solvable.extremal]