S (Definitions)

Files

K

U

W

X

Y

_

Definitions

Y

_

Lemmas

Y

_

Abbreviations

Y

_

Global Index

Y

_

S (Definitions)

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]
S05f [def, 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]
S14f [def, 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]
S23f [def, 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]
S3f [def, in mathcomp.solvable.burnside_app]
s4 [def, in mathcomp.solvable.burnside_app]
S4 [def, 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]
S5f [def, in mathcomp.solvable.burnside_app]
s6 [def, in mathcomp.solvable.burnside_app]
S6 [def, in mathcomp.solvable.burnside_app]
S6f [def, in mathcomp.solvable.burnside_app]
scalar_mx [def, in mathcomp.algebra.matrix]
scalar_mx_is_additive [def, in mathcomp.algebra.matrix]
scalar_mx_is_multiplicative [def, in mathcomp.algebra.matrix]
scalar_mx_is_semi_additive [def, in mathcomp.algebra.matrix]
scale_act [def, in mathcomp.group_representation.mxabelem]
scale_action [def, in mathcomp.group_representation.mxabelem]
scale_groupAction [def, in mathcomp.group_representation.mxabelem]
scale_lfun [def, 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_unlockable [def, in mathcomp.algebra.poly]
scalemx [def, in mathcomp.algebra.matrix]
scalq [def, in mathcomp.algebra.rat]
scanl [def, in mathcomp.boot.seq]
scanl_bseq [def, in mathcomp.boot.tuple]
scanl_tuple [def, in mathcomp.boot.tuple]
schmidt [def, in mathcomp.algebra.spectral]
schmidt_complete [def, in mathcomp.algebra.spectral]
SCN [def, in mathcomp.solvable.maximal]
SCN_at [def, in mathcomp.solvable.maximal]
sd1 [def, in mathcomp.solvable.burnside_app]
Sd1 [def, in mathcomp.solvable.burnside_app]
sd2 [def, in mathcomp.solvable.burnside_app]
Sd2 [def, in mathcomp.solvable.burnside_app]
sdpair1 [def, in mathcomp.finite_group.gproduct]
sdpair1_morphism [def, in mathcomp.finite_group.gproduct]
sdpair2 [def, in mathcomp.finite_group.gproduct]
sdpair2_morphism [def, in mathcomp.finite_group.gproduct]
sdprod_groupType [def, in mathcomp.finite_group.gproduct]
sdprod_Iirr [def, in mathcomp.group_representation.character]
sdprod_inv [def, in mathcomp.finite_group.gproduct]
sdprod_mul [def, in mathcomp.finite_group.gproduct]
sdprod_one [def, in mathcomp.finite_group.gproduct]
sdprodm [def, in mathcomp.finite_group.gproduct]
sdprodm_morphism [def, in mathcomp.finite_group.gproduct]
section_group [def, in mathcomp.solvable.jordanholder]
section_isog [def, in mathcomp.solvable.jordanholder]
section_repr [def, in mathcomp.solvable.jordanholder]
section_repr [def, in mathcomp.group_representation.mxrepresentation]
semidihedral_gtype [def, in mathcomp.solvable.extremal]
semidirect_product [def, in mathcomp.finite_group.gproduct]
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.isComLaw.phant_axioms [def, in mathcomp.boot.bigop]
SemiGroup.isComLaw.phant_Build [def, in mathcomp.boot.bigop]
SemiGroup.isCommutativeLaw.identity_builder [def, in mathcomp.boot.bigop]
SemiGroup.isCommutativeLaw.phant_axioms [def, in mathcomp.boot.bigop]
SemiGroup.isCommutativeLaw.phant_Build [def, in mathcomp.boot.bigop]
SemiGroup.isLaw.identity_builder [def, in mathcomp.boot.bigop]
SemiGroup.isLaw.phant_axioms [def, in mathcomp.boot.bigop]
SemiGroup.isLaw.phant_Build [def, 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.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_isMonoid.phant_axioms [def, in mathcomp.boot.monoid]
Semigroup_isMonoid.phant_Build [def, in mathcomp.boot.monoid]
semiprime [def, in mathcomp.solvable.frobenius]
semiregular [def, in mathcomp.solvable.frobenius]
SemiVector.pack_ [def, in mathcomp.algebra.vector]
SemiVector.phant_clone [def, in mathcomp.algebra.vector]
SemiVector.phant_on_ [def, 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]
separable [def, in mathcomp.field.separable]
separable_element [def, in mathcomp.field.separable]
separable_generator [def, in mathcomp.field.separable]
separable_poly.body [def, in mathcomp.field.separable]
separable_poly.unlock [def, in mathcomp.field.separable]
separable_poly_unlock_subterm [def, in mathcomp.field.separable]
separable_poly_unlockable [def, in mathcomp.field.separable]
seq_eqclass [def, 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_predType [def, in mathcomp.boot.seq]
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_unpickle [def, in mathcomp.boot.fintype]
seqn [def, in mathcomp.boot.seq]
seqn_rec [def, in mathcomp.boot.seq]
seqn_type [def, in mathcomp.boot.seq]
series_repr [def, in mathcomp.group_representation.mxrepresentation]
sesqui [def, in mathcomp.algebra.sesquilinear]
sesqui_keyed [def, in mathcomp.algebra.sesquilinear]
set0 [def, in mathcomp.boot.finset]
set1.body [def, in mathcomp.boot.finset]
set1.unlock [def, in mathcomp.boot.finset]
set1_group [def, in mathcomp.finite_group.fingroup]
set1_unlock_subterm [def, in mathcomp.boot.finset]
set1gXn [def, in mathcomp.finite_group.gproduct]
set_action [def, in mathcomp.finite_group.action]
set_base_group [def, in mathcomp.finite_group.fingroup]
set_invg [def, in mathcomp.finite_group.fingroup]
set_isSub [def, in mathcomp.boot.finset]
set_mulg [def, in mathcomp.finite_group.fingroup]
set_nth [def, in mathcomp.boot.seq]
set_of [def, in mathcomp.boot.finset]
set_predType [def, in mathcomp.boot.finset]
setact [def, in mathcomp.finite_group.action]
setC [def, in mathcomp.boot.finset]
setD [def, in mathcomp.boot.finset]
setI [def, in mathcomp.boot.finset]
setI_group [def, in mathcomp.finite_group.fingroup]
setT_group [def, in mathcomp.finite_group.fingroup]
setTfor [def, in mathcomp.boot.finset]
setU [def, in mathcomp.boot.finset]
setX [def, in mathcomp.boot.finset]
setX_group [def, in mathcomp.finite_group.gproduct]
setXn [def, in mathcomp.boot.finset]
setXn_group [def, in mathcomp.finite_group.gproduct]
sgval [def, in mathcomp.finite_group.fingroup]
sgval_morphism [def, in mathcomp.finite_group.morphism]
sgz [def, in mathcomp.algebra.ssrint]
sgzE [def, in mathcomp.algebra.ssrint]
sh [def, in mathcomp.solvable.burnside_app]
Sh [def, in mathcomp.solvable.burnside_app]
shape [def, in mathcomp.boot.seq]
shorten [def, in mathcomp.boot.path]
sign_morph [def, in mathcomp.solvable.alt]
similar_to [def, in mathcomp.algebra.mxred]
simmx_to_for [def, in mathcomp.algebra.mxpoly]
simple [def, in mathcomp.solvable.gseries]
size [def, in mathcomp.boot.seq]
sizeY [def, in mathcomp.algebra.polyXY]
snd_morphism [def, in mathcomp.finite_group.gproduct]
Socle [def, in mathcomp.group_representation.mxrepresentation]
socle_base [def, in mathcomp.group_representation.mxrepresentation]
socle_enum [def, 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_repr [def, in mathcomp.group_representation.mxrepresentation]
socle_val [def, in mathcomp.group_representation.mxrepresentation]
solvable [def, in mathcomp.solvable.nilpotent]
sop [def, in mathcomp.solvable.burnside_app]
sort [def, in mathcomp.boot.path]
sort_bseq [def, in mathcomp.boot.tuple]
sort_rec1 [def, in mathcomp.boot.path]
sort_tuple [def, in mathcomp.boot.tuple]
sorted [def, in mathcomp.boot.path]
span [def, in mathcomp.algebra.vector]
span_expanded_def [def, in mathcomp.algebra.vector]
span_unlockable [def, in mathcomp.algebra.vector]
special [def, in mathcomp.solvable.maximal]
spectral_diag [def, in mathcomp.algebra.spectral]
spectralmx [def, in mathcomp.algebra.spectral]
split [def, in mathcomp.boot.fintype]
splits_over [def, in mathcomp.finite_group.gproduct]
splitting_field_axiom [def, 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]
splittingFieldFor [def, in mathcomp.field.galois]
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]
ssetI [def, in mathcomp.boot.finset]
stable_factor [def, in mathcomp.solvable.gseries]
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.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.pack_ [def, in mathcomp.boot.monoid]
StarMonoid.phant_clone [def, in mathcomp.boot.monoid]
StarMonoid.phant_on_ [def, in mathcomp.boot.monoid]
StarMonoid_isGroup.identity_builder [def, in mathcomp.boot.monoid]
StarMonoid_isGroup.phant_axioms [def, in mathcomp.boot.monoid]
StarMonoid_isGroup.phant_Build [def, in mathcomp.boot.monoid]
Sub [def, in mathcomp.boot.eqtype]
sub_annihilant [def, in mathcomp.algebra.polyXY]
sub_ord [def, in mathcomp.boot.fintype]
Sub_rect [def, in mathcomp.boot.eqtype]
sub_type [def, in mathcomp.boot.eqtype]
subact [def, in mathcomp.finite_group.action]
subact_dom [def, in mathcomp.finite_group.action]
subact_dom_group [def, in mathcomp.finite_group.action]
subaction [def, in mathcomp.finite_group.action]
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.pack_ [def, in mathcomp.boot.monoid]
SubBaseUMagma.phant_clone [def, in mathcomp.boot.monoid]
SubBaseUMagma.phant_on_ [def, in mathcomp.boot.monoid]
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.pack_ [def, in mathcomp.boot.choice]
SubChoice.phant_clone [def, in mathcomp.boot.choice]
SubChoice.phant_on_ [def, in mathcomp.boot.choice]
SubChoice_isSubGroup.phant_axioms [def, in mathcomp.boot.monoid]
SubChoice_isSubGroup.phant_Build [def, in mathcomp.boot.monoid]
SubChoice_isSubMagma.phant_axioms [def, in mathcomp.boot.monoid]
SubChoice_isSubMagma.phant_Build [def, in mathcomp.boot.monoid]
SubChoice_isSubMonoid.phant_axioms [def, in mathcomp.boot.monoid]
SubChoice_isSubMonoid.phant_Build [def, in mathcomp.boot.monoid]
SubChoice_isSubSemigroup.phant_axioms [def, in mathcomp.boot.monoid]
SubChoice_isSubSemigroup.phant_Build [def, in mathcomp.boot.monoid]
SubChoice_isSubUMagma.phant_axioms [def, in mathcomp.boot.monoid]
SubChoice_isSubUMagma.phant_Build [def, in mathcomp.boot.monoid]
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.pack_ [def, in mathcomp.boot.choice]
SubCountable.phant_clone [def, in mathcomp.boot.choice]
SubCountable.phant_on_ [def, in mathcomp.boot.choice]
SubCountable_isFinite.phant_axioms [def, in mathcomp.boot.fintype]
SubCountable_isFinite.phant_Build [def, in mathcomp.boot.fintype]
SubEquality.Exports.join_eqtype_SubEquality_between_eqtype_Equality_and_eqtype_SubType [def, 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]
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]
SubFieldExtType [def, in mathcomp.field.fieldext]
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.pack_ [def, in mathcomp.boot.fintype]
SubFinite.phant_clone [def, in mathcomp.boot.fintype]
SubFinite.phant_on_ [def, in mathcomp.boot.fintype]
subfx_eval [def, in mathcomp.field.fieldext]
subfx_eval_is_additive [def, in mathcomp.field.fieldext]
subfx_eval_is_multiplicative [def, in mathcomp.field.fieldext]
subfx_eval_morph [def, in mathcomp.field.fieldext]
subfx_inj [def, in mathcomp.field.fieldext]
subfx_inj_is_additive [def, in mathcomp.field.fieldext]
subfx_inj_is_multiplicative [def, in mathcomp.field.fieldext]
subfx_inv_rep [def, 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]
SubfxVect [def, in mathcomp.field.fieldext]
subg [def, in mathcomp.finite_group.fingroup]
subg_inv [def, in mathcomp.finite_group.fingroup]
subg_morphism [def, in mathcomp.finite_group.morphism]
subg_mul [def, in mathcomp.finite_group.fingroup]
subg_of_Sub [def, in mathcomp.finite_group.fingroup]
subg_one [def, in mathcomp.finite_group.fingroup]
subg_repr [def, in mathcomp.group_representation.mxrepresentation]
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.pack_ [def, in mathcomp.boot.monoid]
SubGroup.phant_clone [def, in mathcomp.boot.monoid]
SubGroup.phant_on_ [def, in mathcomp.boot.monoid]
subgroups [def, in mathcomp.finite_group.fingroup]
subitv [def, in mathcomp.algebra.interval]
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.pack_ [def, in mathcomp.boot.monoid]
SubMagma.phant_clone [def, in mathcomp.boot.monoid]
SubMagma.phant_on_ [def, in mathcomp.boot.monoid]
submod_mx [def, in mathcomp.group_representation.mxrepresentation]
submod_repr [def, in mathcomp.group_representation.mxrepresentation]
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.pack_ [def, in mathcomp.boot.monoid]
SubMonoid.phant_clone [def, in mathcomp.boot.monoid]
SubMonoid.phant_on_ [def, in mathcomp.boot.monoid]
submx.body [def, in mathcomp.algebra.mxalgebra]
submx.unlock [def, 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]
submxcol [def, in mathcomp.algebra.matrix]
submxrow [def, in mathcomp.algebra.matrix]
subn [def, in mathcomp.boot.ssrnat]
subn_rec [def, in mathcomp.boot.ssrnat]
subnormal [def, in mathcomp.solvable.gseries]
subq [def, in mathcomp.algebra.rat]
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.pack_ [def, in mathcomp.boot.monoid]
SubSemigroup.phant_clone [def, in mathcomp.boot.monoid]
SubSemigroup.phant_on_ [def, in mathcomp.boot.monoid]
subseq [def, in mathcomp.boot.seq]
subseries_repr [def, in mathcomp.group_representation.mxrepresentation]
subset.body [def, in mathcomp.boot.fintype]
subset.unlock [def, in mathcomp.boot.fintype]
subset_unlock [def, in mathcomp.boot.fintype]
subset_unlock_subterm [def, in mathcomp.boot.fintype]
subsetv [def, in mathcomp.algebra.vector]
SubType.pack_ [def, in mathcomp.boot.eqtype]
SubType.phant_clone [def, in mathcomp.boot.eqtype]
SubType.phant_on_ [def, in mathcomp.boot.eqtype]
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.pack_ [def, in mathcomp.boot.monoid]
SubUMagma.phant_clone [def, in mathcomp.boot.monoid]
SubUMagma.phant_on_ [def, in mathcomp.boot.monoid]
SubVectType [def, in mathcomp.field.fieldext]
subvs_mul [def, in mathcomp.field.falgebra]
subvs_one [def, in mathcomp.field.falgebra]
suffix [def, in mathcomp.boot.seq]
sum_enum [def, in mathcomp.boot.fintype]
sum_eq [def, in mathcomp.boot.eqtype]
sum_isFinite [def, in mathcomp.boot.fintype]
sum_mxsum [def, in mathcomp.algebra.mxalgebra]
sum_of_opair [def, in mathcomp.boot.choice]
sumn [def, in mathcomp.boot.seq]
sumv_pi_for [def, in mathcomp.algebra.vector]
support_for [def, in mathcomp.boot.finfun]
sv [def, in mathcomp.solvable.burnside_app]
Sv [def, in mathcomp.solvable.burnside_app]
swap_pair [def, in mathcomp.boot.ssrfun]
swapXY [def, in mathcomp.algebra.polyXY]
swapXY_def [def, in mathcomp.algebra.polyXY]
swapXY_is_additive [def, in mathcomp.algebra.polyXY]
swapXY_is_multiplicative [def, in mathcomp.algebra.polyXY]
swapXY_unlockable [def, in mathcomp.algebra.polyXY]
swizzle_mx [def, in mathcomp.algebra.matrix]
swizzle_mx_is_additive [def, in mathcomp.algebra.matrix]
swizzle_mx_is_semi_additive [def, in mathcomp.algebra.matrix]
Syl [def, in mathcomp.solvable.pgroup]
Sylow [def, in mathcomp.solvable.pgroup]
Sylvester_mx [def, in mathcomp.algebra.mxpoly]
Sym [def, in mathcomp.solvable.alt]
Sym [def, in mathcomp.finite_group.perm]
Sym_group [def, in mathcomp.solvable.alt]
Sym_group [def, in mathcomp.finite_group.perm]