S (Definitions)
| 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 (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]
s_finite [def, in mathcomp.analysis.measure_theory.measure_function]
same_prefix [def, in mathcomp.classical.classical_orders]
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_ball [def, in mathcomp.analysis.normedtype_theory.vitali_lemma]
scale_continuous [def, in mathcomp.analysis.normedtype_theory.tvs]
scale_fimfun [def, in mathcomp.analysis.numfun]
scale_lfun [def, in mathcomp.algebra.vector]
scale_littleo [def, in mathcomp.analysis.landau]
scale_mfun [def, in mathcomp.analysis.measurable_realfun]
scale_nnsfun [def, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
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]
scale_sfun [def, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
scale_unif_continuous [def, in mathcomp.analysis.normedtype_theory.tvs]
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_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]
sdrop [def, in mathcomp.analysis.sequences]
second_countable [def, in mathcomp.analysis.topology_theory.topology_structure]
section_group [def, in mathcomp.solvable.jordanholder]
section_isog [def, in mathcomp.solvable.jordanholder]
section_repr [def, in mathcomp.solvable.jordanholder]
self_sub [def, in mathcomp.analysis.normedtype_theory.normed_module]
selfFiltered.identity_builder [def, in mathcomp.classical.filter]
selfFiltered.phant_axioms [def, in mathcomp.classical.filter]
selfFiltered.phant_Build [def, in mathcomp.classical.filter]
semi_additive [def, in mathcomp.analysis.measure_theory.measure_function]
semi_additive2 [def, in mathcomp.analysis.measure_theory.measure_function]
semi_measurableD [def, in mathcomp.analysis.measure_theory.measurable_structure]
semi_setD_closed [def, in mathcomp.analysis.measure_theory.measurable_structure]
semi_sigma_additive [def, in mathcomp.analysis.measure_theory.measure_function]
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]
SemiRingOfSets.pack_ [def, in mathcomp.analysis.measure_theory.measurable_structure]
SemiRingOfSets.phant_clone [def, in mathcomp.analysis.measure_theory.measurable_structure]
SemiRingOfSets.phant_on_ [def, in mathcomp.analysis.measure_theory.measurable_structure]
SemiRingOfSets_isRingOfSets.identity_builder [def, in mathcomp.analysis.measure_theory.measurable_structure]
SemiRingOfSets_isRingOfSets.phant_axioms [def, in mathcomp.analysis.measure_theory.measurable_structure]
SemiRingOfSets_isRingOfSets.phant_Build [def, in mathcomp.analysis.measure_theory.measurable_structure]
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]
separate_points_from_closed [def, in mathcomp.analysis.topology_theory.function_spaces]
separated [def, in mathcomp.analysis.topology_theory.connected]
seq_eqclass [def, in mathcomp.boot.seq]
seq_finpredType [def, in mathcomp.finmap.finmap]
seq_fset.body [def, in mathcomp.finmap.finmap]
seq_fset.unlock [def, in mathcomp.finmap.finmap]
seq_fset_unlock_subterm [def, in mathcomp.finmap.finmap]
seq_iso3_L [def, in mathcomp.solvable.burnside_app]
seq_iso_L [def, in mathcomp.solvable.burnside_app]
seq_mset [def, in mathcomp.finmap.multiset]
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]
seqD [def, in mathcomp.analysis.sequences]
seqDU [def, in mathcomp.analysis.sequences]
seqn [def, in mathcomp.boot.seq]
seqn_rec [def, in mathcomp.boot.seq]
seqn_type [def, in mathcomp.boot.seq]
sequence [def, in mathcomp.analysis.sequences]
series [def, in mathcomp.analysis.sequences]
sesqui [def, in mathcomp.algebra.sesquilinear]
sesqui_keyed [def, in mathcomp.algebra.sesquilinear]
set [def, in mathcomp.classical.classical_sets]
set0 [def, in mathcomp.classical.classical_sets]
set0 [def, in mathcomp.boot.finset]
set1 [def, in mathcomp.classical.classical_sets]
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_bij [def, in mathcomp.classical.functions]
set_bij_bijfun [def, in mathcomp.classical.functions]
set_fun [def, in mathcomp.classical.functions]
set_inj [def, in mathcomp.classical.functions]
set_invg [def, in mathcomp.finite_group.fingroup]
set_isSub [def, in mathcomp.boot.finset]
set_itv_infty_set0 [def, in mathcomp.classical.set_interval]
set_itvE [def, in mathcomp.classical.set_interval]
set_mulg [def, in mathcomp.finite_group.fingroup]
set_nbhs [def, in mathcomp.analysis.topology_theory.separation_axioms]
set_nth [def, in mathcomp.boot.seq]
set_of [def, in mathcomp.boot.finset]
set_of_fset [def, in mathcomp.finmap.finmap]
set_predType [def, in mathcomp.classical.classical_sets]
set_predType [def, in mathcomp.boot.finset]
set_surj [def, in mathcomp.classical.functions]
set_system [def, in mathcomp.classical.classical_sets]
set_type [def, in mathcomp.classical.classical_sets]
set_val [def, in mathcomp.classical.functions]
setact [def, in mathcomp.finite_group.action]
setC [def, in mathcomp.classical.classical_sets]
setC [def, in mathcomp.boot.finset]
setC_closed [def, in mathcomp.analysis.measure_theory.measurable_structure]
setC_inj [def, in mathcomp.classical.classical_sets]
setD [def, in mathcomp.classical.classical_sets]
setD [def, in mathcomp.boot.finset]
setD_closed [def, in mathcomp.analysis.measure_theory.measurable_structure]
seteqfun [def, in mathcomp.classical.functions]
setf [def, in mathcomp.finmap.finmap]
setI [def, in mathcomp.classical.classical_sets]
setI [def, in mathcomp.boot.finset]
setI_closed [def, in mathcomp.classical.classical_sets]
setI_group [def, in mathcomp.finite_group.fingroup]
setring [def, in mathcomp.analysis.measure_theory.measurable_structure]
SetRing.decomp [def, in mathcomp.analysis.measure_theory.measure_function]
SetRing.display [def, in mathcomp.analysis.measure_theory.measure_function]
SetRing.measurable_fin_trivIset [def, in mathcomp.analysis.measure_theory.measure_function]
SetRing.measure [def, in mathcomp.analysis.measure_theory.measure_function]
SetRing.type [def, in mathcomp.analysis.measure_theory.measure_function]
setSD_closed [def, in mathcomp.analysis.measure_theory.measurable_structure]
setT [def, in mathcomp.classical.classical_sets]
setT_group [def, in mathcomp.finite_group.fingroup]
setTbij [def, in mathcomp.classical.functions]
setTfor [def, in mathcomp.boot.finset]
setU [def, in mathcomp.classical.classical_sets]
setU [def, in mathcomp.boot.finset]
setU_closed [def, in mathcomp.classical.classical_sets]
setX [def, in mathcomp.classical.classical_sets]
setX [def, in mathcomp.boot.finset]
setX_group [def, in mathcomp.finite_group.gproduct]
setX_of_sigT [def, in mathcomp.analysis.topology_theory.subtype_topology]
setXL [def, in mathcomp.classical.classical_sets]
setXn [def, in mathcomp.boot.finset]
setXn_group [def, in mathcomp.finite_group.gproduct]
setXR [def, in mathcomp.classical.classical_sets]
setY [def, in mathcomp.classical.classical_sets]
setY_closed [def, in mathcomp.analysis.measure_theory.measurable_structure]
sfinite_kernel_subdef [def, in mathcomp.analysis.kernel]
sfinite_measure [def, in mathcomp.analysis.measure_theory.measure_function]
sfinite_measure_seq [def, in mathcomp.analysis.measure_theory.measure_function]
SFiniteKernel.pack_ [def, in mathcomp.analysis.kernel]
SFiniteKernel.phant_clone [def, in mathcomp.analysis.kernel]
SFiniteKernel.phant_on_ [def, in mathcomp.analysis.kernel]
SFiniteMeasure.pack_ [def, in mathcomp.analysis.measure_theory.measure_function]
SFiniteMeasure.phant_clone [def, in mathcomp.analysis.measure_theory.measure_function]
SFiniteMeasure.phant_on_ [def, in mathcomp.analysis.measure_theory.measure_function]
sfun [def, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
sfun_key [def, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
sfun_keyed [def, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
sfun_Sub [def, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
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]
shift [def, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
shorten [def, in mathcomp.boot.path]
sigL [def, in mathcomp.classical.functions]
sigL_arrow [def, in mathcomp.analysis.topology_theory.function_spaces]
sigLfun [def, in mathcomp.classical.functions]
sigLR [def, in mathcomp.classical.functions]
sigma_additive [def, in mathcomp.analysis.measure_theory.measure_function]
sigma_algebra [def, in mathcomp.analysis.measure_theory.measurable_structure]
sigma_display [def, in mathcomp.analysis.measure_theory.measurable_structure]
sigma_finite [def, in mathcomp.analysis.measure_theory.measure_function]
sigma_finiteT [def, in mathcomp.analysis.measure_theory.measure_function]
sigma_ring [def, in mathcomp.analysis.measure_theory.measurable_structure]
sigma_subadditive [def, in mathcomp.analysis.measure_theory.measure_extension]
SigmaFiniteContent.pack_ [def, in mathcomp.analysis.measure_theory.measure_function]
SigmaFiniteContent.phant_clone [def, in mathcomp.analysis.measure_theory.measure_function]
SigmaFiniteContent.phant_on_ [def, in mathcomp.analysis.measure_theory.measure_function]
SigmaFiniteMeasure.Exports.join_measure_function_SigmaFiniteMeasure_between_measure_function_Measure_and_measure_function_SigmaFiniteContent [def, in mathcomp.analysis.measure_theory.measure_function]
SigmaFiniteMeasure.Exports.join_measure_function_SigmaFiniteMeasure_between_measure_function_SFiniteMeasure_and_measure_function_SigmaFiniteContent [def, in mathcomp.analysis.measure_theory.measure_function]
SigmaFiniteMeasure.pack_ [def, in mathcomp.analysis.measure_theory.measure_function]
SigmaFiniteMeasure.phant_clone [def, in mathcomp.analysis.measure_theory.measure_function]
SigmaFiniteMeasure.phant_on_ [def, in mathcomp.analysis.measure_theory.measure_function]
SigmaFiniteTransitionKernel.pack_ [def, in mathcomp.analysis.kernel]
SigmaFiniteTransitionKernel.phant_clone [def, in mathcomp.analysis.kernel]
SigmaFiniteTransitionKernel.phant_on_ [def, in mathcomp.analysis.kernel]
SigmaRing.pack_ [def, in mathcomp.analysis.measure_theory.measurable_structure]
SigmaRing.phant_clone [def, in mathcomp.analysis.measure_theory.measurable_structure]
SigmaRing.phant_on_ [def, in mathcomp.analysis.measure_theory.measurable_structure]
sign_morph [def, in mathcomp.solvable.alt]
Signed.Exports.nonneg [def, in mathcomp.reals.signed]
Signed.Exports.posnum [def, in mathcomp.reals.signed]
Signed.from [def, in mathcomp.reals.signed]
Signed.fromP [def, in mathcomp.reals.signed]
Signed.is_real [def, in mathcomp.reals.signed]
Signed.mk [def, in mathcomp.reals.signed]
Signed.reality_cond [def, in mathcomp.reals.signed]
sigR [def, in mathcomp.classical.functions]
SigSub [def, in mathcomp.classical.classical_sets]
sigT_fun [def, in mathcomp.classical.unstable]
sigT_nbhs [def, in mathcomp.analysis.topology_theory.sigT_topology]
sigT_of_setX [def, in mathcomp.analysis.topology_theory.subtype_topology]
similar_to [def, in mathcomp.algebra.mxred]
simmx_to_for [def, in mathcomp.algebra.mxpoly]
simpl_pred_finpredType [def, in mathcomp.finmap.finmap]
simple [def, in mathcomp.solvable.gseries]
sin.body [def, in mathcomp.analysis.trigo]
sin.unlock [def, in mathcomp.analysis.trigo]
sin_coeff [def, in mathcomp.analysis.trigo]
sin_coeff' [def, in mathcomp.analysis.trigo]
sin_inum [def, in mathcomp.analysis.trigo]
sin_unlock_subterm [def, in mathcomp.analysis.trigo]
singletons [def, in mathcomp.analysis.topology_theory.function_spaces]
sintegral [def, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_definition]
size [def, in mathcomp.boot.seq]
size_mset [def, in mathcomp.finmap.multiset]
sizeY [def, in mathcomp.algebra.polyXY]
small_ent_sub [def, in mathcomp.analysis.topology_theory.function_spaces]
smallest [def, in mathcomp.classical.classical_sets]
snd_fset [def, in mathcomp.classical.cardinality]
snd_morphism [def, in mathcomp.finite_group.gproduct]
snd_set [def, in mathcomp.classical.classical_sets]
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]
SortKeys.f [def, in mathcomp.finmap.finmap]
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]
split_ [def, in mathcomp.classical.functions]
split_ent [def, in mathcomp.analysis.topology_theory.uniform_structure]
SplitBij.Exports.join_functions_SplitBij_between_functions_Bij_and_functions_Inversible [def, in mathcomp.classical.functions]
SplitBij.Exports.join_functions_SplitBij_between_functions_Bij_and_functions_InvFun [def, in mathcomp.classical.functions]
SplitBij.Exports.join_functions_SplitBij_between_functions_Bij_and_functions_SplitInj [def, in mathcomp.classical.functions]
SplitBij.Exports.join_functions_SplitBij_between_functions_Bij_and_functions_SplitInjFun [def, in mathcomp.classical.functions]
SplitBij.Exports.join_functions_SplitBij_between_functions_Bij_and_functions_SplitSurj [def, in mathcomp.classical.functions]
SplitBij.Exports.join_functions_SplitBij_between_functions_Bij_and_functions_SplitSurjFun [def, in mathcomp.classical.functions]
SplitBij.Exports.join_functions_SplitBij_between_functions_Inject_and_functions_SplitSurj [def, in mathcomp.classical.functions]
SplitBij.Exports.join_functions_SplitBij_between_functions_Inject_and_functions_SplitSurjFun [def, in mathcomp.classical.functions]
SplitBij.Exports.join_functions_SplitBij_between_functions_InjFun_and_functions_SplitSurj [def, in mathcomp.classical.functions]
SplitBij.Exports.join_functions_SplitBij_between_functions_InjFun_and_functions_SplitSurjFun [def, in mathcomp.classical.functions]
SplitBij.Exports.join_functions_SplitBij_between_functions_SplitInj_and_functions_SplitSurj [def, in mathcomp.classical.functions]
SplitBij.Exports.join_functions_SplitBij_between_functions_SplitInj_and_functions_SplitSurjFun [def, in mathcomp.classical.functions]
SplitBij.Exports.join_functions_SplitBij_between_functions_SplitInj_and_functions_Surject [def, in mathcomp.classical.functions]
SplitBij.Exports.join_functions_SplitBij_between_functions_SplitInj_and_functions_SurjFun [def, in mathcomp.classical.functions]
SplitBij.Exports.join_functions_SplitBij_between_functions_SplitInjFun_and_functions_SplitSurj [def, in mathcomp.classical.functions]
SplitBij.Exports.join_functions_SplitBij_between_functions_SplitInjFun_and_functions_SplitSurjFun [def, in mathcomp.classical.functions]
SplitBij.Exports.join_functions_SplitBij_between_functions_SplitInjFun_and_functions_Surject [def, in mathcomp.classical.functions]
SplitBij.Exports.join_functions_SplitBij_between_functions_SplitInjFun_and_functions_SurjFun [def, in mathcomp.classical.functions]
SplitBij.pack_ [def, in mathcomp.classical.functions]
SplitBij.phant_clone [def, in mathcomp.classical.functions]
SplitBij.phant_on_ [def, in mathcomp.classical.functions]
SplitInj.Exports.join_functions_SplitInj_between_functions_Inject_and_functions_Inversible [def, in mathcomp.classical.functions]
SplitInj.pack_ [def, in mathcomp.classical.functions]
SplitInj.phant_clone [def, in mathcomp.classical.functions]
SplitInj.phant_on_ [def, in mathcomp.classical.functions]
SplitInjFun.Exports.join_functions_SplitInjFun_between_functions_Fun_and_functions_SplitInj [def, in mathcomp.classical.functions]
SplitInjFun.Exports.join_functions_SplitInjFun_between_functions_Inject_and_functions_InvFun [def, in mathcomp.classical.functions]
SplitInjFun.Exports.join_functions_SplitInjFun_between_functions_InjFun_and_functions_Inversible [def, in mathcomp.classical.functions]
SplitInjFun.Exports.join_functions_SplitInjFun_between_functions_InjFun_and_functions_InvFun [def, in mathcomp.classical.functions]
SplitInjFun.Exports.join_functions_SplitInjFun_between_functions_InjFun_and_functions_SplitInj [def, in mathcomp.classical.functions]
SplitInjFun.Exports.join_functions_SplitInjFun_between_functions_InvFun_and_functions_SplitInj [def, in mathcomp.classical.functions]
SplitInjFun.Exports.join_functions_SplitInjFun_between_functions_OInvFun_and_functions_SplitInj [def, in mathcomp.classical.functions]
SplitInjFun.pack_ [def, in mathcomp.classical.functions]
SplitInjFun.phant_clone [def, in mathcomp.classical.functions]
SplitInjFun.phant_on_ [def, in mathcomp.classical.functions]
SplitInjFun_CanV.phant_axioms [def, in mathcomp.classical.functions]
SplitInjFun_CanV.phant_Build [def, in mathcomp.classical.functions]
splits_over [def, in mathcomp.finite_group.gproduct]
SplitSurj.Exports.join_functions_SplitSurj_between_functions_Inversible_and_functions_Surject [def, in mathcomp.classical.functions]
SplitSurj.pack_ [def, in mathcomp.classical.functions]
SplitSurj.phant_clone [def, in mathcomp.classical.functions]
SplitSurj.phant_on_ [def, in mathcomp.classical.functions]
SplitSurjFun.Exports.join_functions_SplitSurjFun_between_functions_Fun_and_functions_SplitSurj [def, in mathcomp.classical.functions]
SplitSurjFun.Exports.join_functions_SplitSurjFun_between_functions_Inversible_and_functions_SurjFun [def, in mathcomp.classical.functions]
SplitSurjFun.Exports.join_functions_SplitSurjFun_between_functions_InvFun_and_functions_SplitSurj [def, in mathcomp.classical.functions]
SplitSurjFun.Exports.join_functions_SplitSurjFun_between_functions_InvFun_and_functions_Surject [def, in mathcomp.classical.functions]
SplitSurjFun.Exports.join_functions_SplitSurjFun_between_functions_InvFun_and_functions_SurjFun [def, in mathcomp.classical.functions]
SplitSurjFun.Exports.join_functions_SplitSurjFun_between_functions_OInvFun_and_functions_SplitSurj [def, in mathcomp.classical.functions]
SplitSurjFun.Exports.join_functions_SplitSurjFun_between_functions_SplitSurj_and_functions_SurjFun [def, in mathcomp.classical.functions]
SplitSurjFun.pack_ [def, in mathcomp.classical.functions]
SplitSurjFun.phant_clone [def, in mathcomp.classical.functions]
SplitSurjFun.phant_on_ [def, in mathcomp.classical.functions]
SplitSurjFun_Inj.phant_axioms [def, in mathcomp.classical.functions]
SplitSurjFun_Inj.phant_Build [def, in mathcomp.classical.functions]
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]
sprob_kernel [def, in mathcomp.analysis.kernel]
sprobability_setT [def, in mathcomp.analysis.measure_theory.probability_measure]
sqrt_nonzero_subdef [def, in mathcomp.reals.signed]
sqrt_snum [def, in mathcomp.reals.signed]
sqrtC_reality_subdef [def, in mathcomp.reals.signed]
sqrtC_snum [def, in mathcomp.reals.signed]
sqrte [def, in mathcomp.reals.constructive_ereal]
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]
ssquash [def, in mathcomp.classical.functions]
stable_factor [def, in mathcomp.solvable.gseries]
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]
start_with [def, in mathcomp.classical.classical_orders]
strace [def, in mathcomp.analysis.measure_theory.measurable_structure]
Streicher_K_ [def, in mathcomp.classical.internal_Eqdep_dec]
Streicher_K_on_ [def, in mathcomp.classical.internal_Eqdep_dec]
strict_monotonic [def, in mathcomp.classical.unstable]
strictly_dominated_by [def, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
Sub [def, in mathcomp.boot.eqtype]
sub_annihilant [def, in mathcomp.algebra.polyXY]
sub_fun [def, in mathcomp.finmap.finmap]
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]
subadditive [def, in mathcomp.analysis.measure_theory.measure_function]
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]
subfinset_finpred [def, in mathcomp.finmap.finmap]
subfun [def, in mathcomp.classical.functions]
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]
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]
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]
SubProbability.pack_ [def, in mathcomp.analysis.measure_theory.probability_measure]
SubProbability.phant_clone [def, in mathcomp.analysis.measure_theory.probability_measure]
SubProbability.phant_on_ [def, in mathcomp.analysis.measure_theory.probability_measure]
SubProbabilityKernel.pack_ [def, in mathcomp.analysis.kernel]
SubProbabilityKernel.phant_clone [def, in mathcomp.analysis.kernel]
SubProbabilityKernel.phant_on_ [def, in mathcomp.analysis.kernel]
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]
subset [def, in mathcomp.classical.classical_sets]
subset.body [def, in mathcomp.boot.fintype]
subset.unlock [def, in mathcomp.boot.fintype]
subset_filter [def, in mathcomp.classical.filter]
subset_sigma_subadditive [def, in mathcomp.analysis.measure_theory.measurable_structure]
subset_unlock [def, in mathcomp.boot.fintype]
subset_unlock_subterm [def, in mathcomp.boot.fintype]
subsetCW [def, in mathcomp.classical.classical_sets]
subsetv [def, in mathcomp.algebra.vector]
subspace [def, in mathcomp.analysis.topology_theory.subspace_topology]
subspace_ball [def, in mathcomp.analysis.topology_theory.subspace_topology]
subspace_ent [def, in mathcomp.analysis.topology_theory.subspace_topology]
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]
succn_snum [def, in mathcomp.reals.signed]
suffix [def, in mathcomp.boot.seq]
sum [def, in mathcomp.analysis.showcase.summability]
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_nnsfun [def, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
sum_of_opair [def, in mathcomp.boot.choice]
summable [def, in mathcomp.analysis.showcase.summability]
summable [def, in mathcomp.analysis.esum]
sumn [def, in mathcomp.boot.seq]
sumv_pi_for [def, in mathcomp.algebra.vector]
sup [def, in mathcomp.reals.reals]
sup_adherent_subdef [def, in mathcomp.reals.reals]
sup_ent [def, in mathcomp.analysis.topology_theory.supremum_topology]
sup_pseudometric [def, in mathcomp.analysis.topology_theory.separation_axioms]
sup_subbase [def, in mathcomp.analysis.topology_theory.supremum_topology]
sup_topology [def, in mathcomp.analysis.topology_theory.supremum_topology]
sup_upper_bound_subdef [def, in mathcomp.reals.reals]
support_for [def, in mathcomp.boot.finfun]
supremum [def, in mathcomp.classical.classical_sets]
supremums [def, in mathcomp.classical.classical_sets]
sups [def, in mathcomp.analysis.sequences]
Surject.pack_ [def, in mathcomp.classical.functions]
Surject.phant_clone [def, in mathcomp.classical.functions]
Surject.phant_on_ [def, in mathcomp.classical.functions]
surjection_of_surj [def, in mathcomp.classical.functions]
surjective_ocanV [def, in mathcomp.classical.functions]
SurjFun.Exports.join_functions_SurjFun_between_functions_Fun_and_functions_Surject [def, in mathcomp.classical.functions]
SurjFun.Exports.join_functions_SurjFun_between_functions_OInvFun_and_functions_Surject [def, in mathcomp.classical.functions]
SurjFun.pack_ [def, in mathcomp.classical.functions]
SurjFun.phant_clone [def, in mathcomp.classical.functions]
SurjFun.phant_on_ [def, in mathcomp.classical.functions]
SurjFun_Inj.phant_axioms [def, in mathcomp.classical.functions]
SurjFun_Inj.phant_Build [def, in mathcomp.classical.functions]
sv [def, in mathcomp.solvable.burnside_app]
Sv [def, in mathcomp.solvable.burnside_app]
swap [def, in mathcomp.classical.unstable]
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]