S (Abbreviations)
| 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 (Abbreviations)
S [abbrev, in mathcomp.analysis.topology_theory.supremum_topology]S [abbrev, in mathcomp.analysis.topology_theory.separation_axioms]
S [abbrev, in mathcomp.analysis.topology_theory.initial_topology]
scale [abbrev, in mathcomp.analysis.measure_theory.measure_function]
sdprod [abbrev, in mathcomp.finite_group.gproduct]
sdprod [abbrev, in mathcomp.finite_group.gproduct]
sdT [abbrev, in mathcomp.finite_group.gproduct]
sdval [abbrev, in mathcomp.finite_group.gproduct]
sedDI_closedP [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
selfFiltered [abbrev, in mathcomp.classical.filter]
selfFiltered.axioms [abbrev, in mathcomp.classical.filter]
selfFiltered.Build [abbrev, in mathcomp.classical.filter]
selfPbij [abbrev, in mathcomp.classical.functions]
semiAlgType [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
Semigroup [abbrev, in mathcomp.boot.monoid]
SemiGroup.Builders_1.opA [abbrev, in mathcomp.boot.bigop]
SemiGroup.Builders_1.opC [abbrev, in mathcomp.boot.bigop]
Semigroup.clone [abbrev, in mathcomp.boot.monoid]
SemiGroup.com_law [abbrev, in mathcomp.boot.bigop]
SemiGroup.ComLaw [abbrev, in mathcomp.boot.bigop]
SemiGroup.ComLaw.clone [abbrev, in mathcomp.boot.bigop]
SemiGroup.ComLaw.copy [abbrev, in mathcomp.boot.bigop]
SemiGroup.ComLaw.on [abbrev, in mathcomp.boot.bigop]
SemiGroup.ComLaw.on_ [abbrev, in mathcomp.boot.bigop]
Semigroup.copy [abbrev, in mathcomp.boot.monoid]
Semigroup.Exports.semigroupType [abbrev, in mathcomp.boot.monoid]
SemiGroup.isComLaw [abbrev, in mathcomp.boot.bigop]
SemiGroup.isComLaw.axioms [abbrev, in mathcomp.boot.bigop]
SemiGroup.isComLaw.Build [abbrev, in mathcomp.boot.bigop]
SemiGroup.isCommutativeLaw [abbrev, in mathcomp.boot.bigop]
SemiGroup.isCommutativeLaw.axioms [abbrev, in mathcomp.boot.bigop]
SemiGroup.isCommutativeLaw.Build [abbrev, in mathcomp.boot.bigop]
SemiGroup.isLaw [abbrev, in mathcomp.boot.bigop]
SemiGroup.isLaw.axioms [abbrev, in mathcomp.boot.bigop]
SemiGroup.isLaw.Build [abbrev, in mathcomp.boot.bigop]
SemiGroup.law [abbrev, in mathcomp.boot.bigop]
SemiGroup.Law [abbrev, in mathcomp.boot.bigop]
SemiGroup.Law.clone [abbrev, in mathcomp.boot.bigop]
SemiGroup.Law.copy [abbrev, in mathcomp.boot.bigop]
SemiGroup.Law.on [abbrev, in mathcomp.boot.bigop]
SemiGroup.Law.on_ [abbrev, in mathcomp.boot.bigop]
Semigroup.on [abbrev, in mathcomp.boot.monoid]
Semigroup.on_ [abbrev, in mathcomp.boot.monoid]
Semigroup_isMonoid [abbrev, in mathcomp.boot.monoid]
Semigroup_isMonoid.axioms [abbrev, in mathcomp.boot.monoid]
Semigroup_isMonoid.Build [abbrev, in mathcomp.boot.monoid]
SemiRingOfSets [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
SemiRingOfSets.clone [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
SemiRingOfSets.copy [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
SemiRingOfSets.Exports.semiRingOfSetsType [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
SemiRingOfSets.on [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
SemiRingOfSets.on_ [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
SemiRingOfSets_isRingOfSets [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
SemiRingOfSets_isRingOfSets.axioms [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
SemiRingOfSets_isRingOfSets.Build [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
semiRingType [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
SemiVector [abbrev, in mathcomp.algebra.vector]
SemiVector.clone [abbrev, in mathcomp.algebra.vector]
SemiVector.copy [abbrev, in mathcomp.algebra.vector]
SemiVector.Exports.semiVectType [abbrev, in mathcomp.algebra.vector]
SemiVector.on [abbrev, in mathcomp.algebra.vector]
SemiVector.on_ [abbrev, in mathcomp.algebra.vector]
SemiVector_isProper [abbrev, in mathcomp.algebra.vector]
SemiVector_isProper.axioms [abbrev, in mathcomp.algebra.vector]
SemiVector_isProper.Build [abbrev, in mathcomp.algebra.vector]
separable [abbrev, in mathcomp.field.separable]
separable_exponent [abbrev, in mathcomp.field.separable]
separable_poly [abbrev, in mathcomp.field.separable]
separablePn [abbrev, in mathcomp.field.separable]
seq [abbrev, in mathcomp.boot.seq]
seq_fset [abbrev, in mathcomp.finmap.finmap]
seq_fset [abbrev, in mathcomp.finmap.finmap]
set1 [abbrev, in mathcomp.boot.finset]
set_itv_bnd_ninfty [abbrev, in mathcomp.classical.set_interval]
set_itv_c_infty [abbrev, in mathcomp.classical.set_interval]
set_itv_infty_c [abbrev, in mathcomp.classical.set_interval]
set_itv_infty_infty [abbrev, in mathcomp.classical.set_interval]
set_itv_infty_o [abbrev, in mathcomp.classical.set_interval]
set_itv_o_infty [abbrev, in mathcomp.classical.set_interval]
set_itv_pinfty_bnd [abbrev, in mathcomp.classical.set_interval]
setDI_closed [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
setDI_semi_setD_closed [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
SetRing.Rmu [abbrev, in mathcomp.analysis.measure_theory.measure_function]
SetRing.rT [abbrev, in mathcomp.analysis.measure_theory.measure_function]
setringDI [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
setT [abbrev, in mathcomp.boot.finset]
setTP [abbrev, in mathcomp.classical.classical_sets]
SFiniteKernel [abbrev, in mathcomp.analysis.kernel]
SFiniteKernel.clone [abbrev, in mathcomp.analysis.kernel]
SFiniteKernel.copy [abbrev, in mathcomp.analysis.kernel]
SFiniteKernel.on [abbrev, in mathcomp.analysis.kernel]
SFiniteKernel.on_ [abbrev, in mathcomp.analysis.kernel]
SFiniteKernel_isFinite [abbrev, in mathcomp.analysis.kernel]
SFiniteKernel_isFinite.Build [abbrev, in mathcomp.analysis.kernel]
SFiniteMeasure [abbrev, in mathcomp.analysis.measure_theory.measure_function]
SFiniteMeasure.clone [abbrev, in mathcomp.analysis.measure_theory.measure_function]
SFiniteMeasure.copy [abbrev, in mathcomp.analysis.measure_theory.measure_function]
SFiniteMeasure.on [abbrev, in mathcomp.analysis.measure_theory.measure_function]
SFiniteMeasure.on_ [abbrev, in mathcomp.analysis.measure_theory.measure_function]
sfun [abbrev, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
sgr [abbrev, in mathcomp.algebra.ssrint]
sgr [abbrev, in mathcomp.algebra.rat]
sigma_algebra_image_class [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
sigma_algebra_preimage_class [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
sigma_algebra_preimage_classE [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
SigmaFiniteContent [abbrev, in mathcomp.analysis.measure_theory.measure_function]
SigmaFiniteContent.clone [abbrev, in mathcomp.analysis.measure_theory.measure_function]
SigmaFiniteContent.copy [abbrev, in mathcomp.analysis.measure_theory.measure_function]
SigmaFiniteContent.Exports.sigma_finite_content [abbrev, in mathcomp.analysis.measure_theory.measure_function]
SigmaFiniteContent.on [abbrev, in mathcomp.analysis.measure_theory.measure_function]
SigmaFiniteContent.on_ [abbrev, in mathcomp.analysis.measure_theory.measure_function]
SigmaFiniteMeasure [abbrev, in mathcomp.analysis.measure_theory.measure_function]
SigmaFiniteMeasure.clone [abbrev, in mathcomp.analysis.measure_theory.measure_function]
SigmaFiniteMeasure.copy [abbrev, in mathcomp.analysis.measure_theory.measure_function]
SigmaFiniteMeasure.Exports.sigma_finite_measure [abbrev, in mathcomp.analysis.measure_theory.measure_function]
SigmaFiniteMeasure.on [abbrev, in mathcomp.analysis.measure_theory.measure_function]
SigmaFiniteMeasure.on_ [abbrev, in mathcomp.analysis.measure_theory.measure_function]
SigmaFiniteTransitionKernel [abbrev, in mathcomp.analysis.kernel]
SigmaFiniteTransitionKernel.clone [abbrev, in mathcomp.analysis.kernel]
SigmaFiniteTransitionKernel.copy [abbrev, in mathcomp.analysis.kernel]
SigmaFiniteTransitionKernel.Exports.sigma_finite_kernel [abbrev, in mathcomp.analysis.kernel]
SigmaFiniteTransitionKernel.on [abbrev, in mathcomp.analysis.kernel]
SigmaFiniteTransitionKernel.on_ [abbrev, in mathcomp.analysis.kernel]
SigmaRing [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
SigmaRing.clone [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
SigmaRing.copy [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
SigmaRing.Exports.sigmaRingType [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
SigmaRing.on [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
SigmaRing.on_ [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
Signed.Exports.num [abbrev, in mathcomp.reals.signed]
Signed.spec [abbrev, in mathcomp.reals.signed]
similar [abbrev, in mathcomp.algebra.mxred]
similar_diag [abbrev, in mathcomp.algebra.mxred]
similar_in [abbrev, in mathcomp.algebra.mxred]
similar_in_to [abbrev, in mathcomp.algebra.mxred]
similar_trig [abbrev, 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]
simp [abbrev, in mathcomp.algebra.polydiv]
simp [abbrev, in mathcomp.algebra.poly]
simp [abbrev, in mathcomp.algebra.mxalgebra]
simp [abbrev, in mathcomp.algebra.matrix]
simplrefl [abbrev, in mathcomp.boot.ssrAC]
sin [abbrev, in mathcomp.analysis.trigo]
size_add [abbrev, in mathcomp.algebra.poly]
size_addl [abbrev, in mathcomp.algebra.poly]
size_exp_leq [abbrev, in mathcomp.algebra.poly]
size_mul_leq [abbrev, in mathcomp.algebra.poly]
size_opp [abbrev, in mathcomp.algebra.poly]
size_prod_leq [abbrev, in mathcomp.algebra.poly]
skew [abbrev, in mathcomp.algebra.sesquilinear]
skewmx [abbrev, in mathcomp.algebra.sesquilinear]
sort_keys [abbrev, in mathcomp.finmap.finmap]
sort_keys_perm [abbrev, in mathcomp.finmap.finmap]
sort_keys_uniq [abbrev, in mathcomp.finmap.finmap]
sort_keysE [abbrev, in mathcomp.finmap.finmap]
sorted [abbrev, in mathcomp.boot.path]
sorted [abbrev, 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]
split [abbrev, in mathcomp.classical.functions]
split [abbrev, in mathcomp.classical.functions]
SplitBij [abbrev, in mathcomp.classical.functions]
SplitBij.clone [abbrev, in mathcomp.classical.functions]
SplitBij.copy [abbrev, in mathcomp.classical.functions]
SplitBij.on [abbrev, in mathcomp.classical.functions]
SplitBij.on_ [abbrev, in mathcomp.classical.functions]
SplitInj [abbrev, in mathcomp.classical.functions]
SplitInj.clone [abbrev, in mathcomp.classical.functions]
SplitInj.copy [abbrev, in mathcomp.classical.functions]
SplitInj.on [abbrev, in mathcomp.classical.functions]
SplitInj.on_ [abbrev, in mathcomp.classical.functions]
SplitInjFun [abbrev, in mathcomp.classical.functions]
SplitInjFun.clone [abbrev, in mathcomp.classical.functions]
SplitInjFun.copy [abbrev, in mathcomp.classical.functions]
SplitInjFun.on [abbrev, in mathcomp.classical.functions]
SplitInjFun.on_ [abbrev, in mathcomp.classical.functions]
SplitInjFun_CanV [abbrev, in mathcomp.classical.functions]
SplitInjFun_CanV.axioms [abbrev, in mathcomp.classical.functions]
SplitInjFun_CanV.Build [abbrev, in mathcomp.classical.functions]
SplitSurj [abbrev, in mathcomp.classical.functions]
SplitSurj.clone [abbrev, in mathcomp.classical.functions]
SplitSurj.copy [abbrev, in mathcomp.classical.functions]
SplitSurj.on [abbrev, in mathcomp.classical.functions]
SplitSurj.on_ [abbrev, in mathcomp.classical.functions]
SplitSurjFun [abbrev, in mathcomp.classical.functions]
SplitSurjFun.clone [abbrev, in mathcomp.classical.functions]
SplitSurjFun.copy [abbrev, in mathcomp.classical.functions]
SplitSurjFun.on [abbrev, in mathcomp.classical.functions]
SplitSurjFun.on_ [abbrev, in mathcomp.classical.functions]
SplitSurjFun_Inj [abbrev, in mathcomp.classical.functions]
SplitSurjFun_Inj.axioms [abbrev, in mathcomp.classical.functions]
SplitSurjFun_Inj.Build [abbrev, in mathcomp.classical.functions]
SplittingField [abbrev, in mathcomp.field.galois]
SplittingField.clone [abbrev, in mathcomp.field.galois]
SplittingField.copy [abbrev, in mathcomp.field.galois]
SplittingField.Exports.splittingFieldType [abbrev, in mathcomp.field.galois]
SplittingField.on [abbrev, in mathcomp.field.galois]
SplittingField.on_ [abbrev, 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]
sT [abbrev, in mathcomp.reals.signed]
sT [abbrev, in mathcomp.reals.signed]
sT [abbrev, in mathcomp.reals.signed]
sT [abbrev, in mathcomp.finite_group.fingroup]
sT [abbrev, in mathcomp.boot.fintype]
sT [abbrev, in mathcomp.boot.finset]
stablemx [abbrev, in mathcomp.algebra.mxalgebra]
stablemx [abbrev, in mathcomp.algebra.mxalgebra]
StarMonoid [abbrev, in mathcomp.boot.monoid]
StarMonoid.clone [abbrev, in mathcomp.boot.monoid]
StarMonoid.copy [abbrev, in mathcomp.boot.monoid]
StarMonoid.Exports.starMonoidType [abbrev, in mathcomp.boot.monoid]
StarMonoid.on [abbrev, in mathcomp.boot.monoid]
StarMonoid.on_ [abbrev, in mathcomp.boot.monoid]
StarMonoid_isGroup [abbrev, in mathcomp.boot.monoid]
StarMonoid_isGroup.axioms [abbrev, in mathcomp.boot.monoid]
StarMonoid_isGroup.Build [abbrev, in mathcomp.boot.monoid]
Sub [abbrev, in mathcomp.boot.eqtype]
subAlgType [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
SubBaseUMagma [abbrev, in mathcomp.boot.monoid]
SubBaseUMagma.clone [abbrev, in mathcomp.boot.monoid]
SubBaseUMagma.copy [abbrev, in mathcomp.boot.monoid]
SubBaseUMagma.Exports.subBaseUMagmaType [abbrev, in mathcomp.boot.monoid]
SubBaseUMagma.on [abbrev, in mathcomp.boot.monoid]
SubBaseUMagma.on_ [abbrev, in mathcomp.boot.monoid]
SubChoice [abbrev, in mathcomp.boot.choice]
SubChoice.clone [abbrev, in mathcomp.boot.choice]
SubChoice.copy [abbrev, 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_isSubGroup [abbrev, in mathcomp.boot.monoid]
SubChoice_isSubGroup.axioms [abbrev, in mathcomp.boot.monoid]
SubChoice_isSubGroup.Build [abbrev, in mathcomp.boot.monoid]
SubChoice_isSubMagma [abbrev, in mathcomp.boot.monoid]
SubChoice_isSubMagma.axioms [abbrev, in mathcomp.boot.monoid]
SubChoice_isSubMagma.Build [abbrev, in mathcomp.boot.monoid]
SubChoice_isSubMonoid [abbrev, in mathcomp.boot.monoid]
SubChoice_isSubMonoid.axioms [abbrev, in mathcomp.boot.monoid]
SubChoice_isSubMonoid.Build [abbrev, in mathcomp.boot.monoid]
SubChoice_isSubSemigroup [abbrev, in mathcomp.boot.monoid]
SubChoice_isSubSemigroup.axioms [abbrev, in mathcomp.boot.monoid]
SubChoice_isSubSemigroup.Build [abbrev, in mathcomp.boot.monoid]
SubChoice_isSubUMagma [abbrev, in mathcomp.boot.monoid]
SubChoice_isSubUMagma.axioms [abbrev, in mathcomp.boot.monoid]
SubChoice_isSubUMagma.Build [abbrev, in mathcomp.boot.monoid]
subComRingType [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
subComSemiRingType [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
SubCountable [abbrev, in mathcomp.boot.choice]
SubCountable.clone [abbrev, in mathcomp.boot.choice]
SubCountable.copy [abbrev, 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_isFinite [abbrev, in mathcomp.boot.fintype]
SubCountable_isFinite.axioms [abbrev, in mathcomp.boot.fintype]
SubCountable_isFinite.Build [abbrev, in mathcomp.boot.fintype]
subdom [abbrev, in mathcomp.finite_group.action]
SubEquality [abbrev, in mathcomp.boot.eqtype]
SubEquality.clone [abbrev, in mathcomp.boot.eqtype]
SubEquality.copy [abbrev, 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]
SubFinite [abbrev, in mathcomp.boot.fintype]
SubFinite.clone [abbrev, in mathcomp.boot.fintype]
SubFinite.copy [abbrev, in mathcomp.boot.fintype]
SubFinite.Exports.subFinType [abbrev, in mathcomp.boot.fintype]
SubFinite.on [abbrev, in mathcomp.boot.fintype]
SubFinite.on_ [abbrev, in mathcomp.boot.fintype]
SubGroup [abbrev, in mathcomp.boot.monoid]
SubGroup.clone [abbrev, in mathcomp.boot.monoid]
SubGroup.copy [abbrev, in mathcomp.boot.monoid]
SubGroup.Exports.subGroupType [abbrev, in mathcomp.boot.monoid]
SubGroup.on [abbrev, in mathcomp.boot.monoid]
SubGroup.on_ [abbrev, in mathcomp.boot.monoid]
subLalgType [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
subLSemiAlgType [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
SubMagma [abbrev, in mathcomp.boot.monoid]
SubMagma.clone [abbrev, in mathcomp.boot.monoid]
SubMagma.copy [abbrev, in mathcomp.boot.monoid]
SubMagma.Exports.subMagmaType [abbrev, in mathcomp.boot.monoid]
SubMagma.on [abbrev, in mathcomp.boot.monoid]
SubMagma.on_ [abbrev, in mathcomp.boot.monoid]
SubMonoid [abbrev, in mathcomp.boot.monoid]
SubMonoid.clone [abbrev, in mathcomp.boot.monoid]
SubMonoid.copy [abbrev, in mathcomp.boot.monoid]
SubMonoid.Exports.subMonoidType [abbrev, in mathcomp.boot.monoid]
SubMonoid.on [abbrev, in mathcomp.boot.monoid]
SubMonoid.on_ [abbrev, in mathcomp.boot.monoid]
submx [abbrev, in mathcomp.algebra.mxalgebra]
SubProbability [abbrev, in mathcomp.analysis.measure_theory.probability_measure]
SubProbability.clone [abbrev, in mathcomp.analysis.measure_theory.probability_measure]
SubProbability.copy [abbrev, in mathcomp.analysis.measure_theory.probability_measure]
SubProbability.Exports.subprobability [abbrev, in mathcomp.analysis.measure_theory.probability_measure]
SubProbability.on [abbrev, in mathcomp.analysis.measure_theory.probability_measure]
SubProbability.on_ [abbrev, in mathcomp.analysis.measure_theory.probability_measure]
SubProbability_isProbability [abbrev, in mathcomp.analysis.kernel]
SubProbability_isProbability.Build [abbrev, in mathcomp.analysis.kernel]
SubProbabilityKernel [abbrev, in mathcomp.analysis.kernel]
SubProbabilityKernel.clone [abbrev, in mathcomp.analysis.kernel]
SubProbabilityKernel.copy [abbrev, in mathcomp.analysis.kernel]
SubProbabilityKernel.Exports.sprobability_kernel [abbrev, in mathcomp.analysis.kernel]
SubProbabilityKernel.on [abbrev, in mathcomp.analysis.kernel]
SubProbabilityKernel.on_ [abbrev, in mathcomp.analysis.kernel]
subRingType [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
subSemiAlgType [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
SubSemigroup [abbrev, in mathcomp.boot.monoid]
SubSemigroup.clone [abbrev, in mathcomp.boot.monoid]
SubSemigroup.copy [abbrev, in mathcomp.boot.monoid]
SubSemigroup.Exports.subSemigroupType [abbrev, in mathcomp.boot.monoid]
SubSemigroup.on [abbrev, in mathcomp.boot.monoid]
SubSemigroup.on_ [abbrev, in mathcomp.boot.monoid]
subSemiRingType [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
subset [abbrev, in mathcomp.boot.fintype]
SubType [abbrev, in mathcomp.boot.eqtype]
SubType.clone [abbrev, in mathcomp.boot.eqtype]
SubType.copy [abbrev, 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]
SubUMagma [abbrev, in mathcomp.boot.monoid]
SubUMagma.clone [abbrev, in mathcomp.boot.monoid]
SubUMagma.copy [abbrev, in mathcomp.boot.monoid]
SubUMagma.Exports.subUMagmaType [abbrev, in mathcomp.boot.monoid]
SubUMagma.on [abbrev, in mathcomp.boot.monoid]
SubUMagma.on_ [abbrev, in mathcomp.boot.monoid]
subV [abbrev, in mathcomp.algebra.vector]
succn [abbrev, in mathcomp.boot.ssrnat]
sumKx [abbrev, in mathcomp.field.fieldext]
sumV [abbrev, in mathcomp.algebra.vector]
sumv_pi [abbrev, in mathcomp.algebra.vector]
sup_le_ub [abbrev, in mathcomp.reals.reals]
sup_open [abbrev, in mathcomp.analysis.topology_theory.function_spaces]
sup_ubound [abbrev, in mathcomp.reals.reals]
support [abbrev, in mathcomp.boot.nmodule]
support [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
Surject [abbrev, in mathcomp.classical.functions]
Surject.clone [abbrev, in mathcomp.classical.functions]
Surject.copy [abbrev, in mathcomp.classical.functions]
Surject.on [abbrev, in mathcomp.classical.functions]
Surject.on_ [abbrev, in mathcomp.classical.functions]
SurjFun [abbrev, in mathcomp.classical.functions]
SurjFun.clone [abbrev, in mathcomp.classical.functions]
SurjFun.copy [abbrev, in mathcomp.classical.functions]
SurjFun.on [abbrev, in mathcomp.classical.functions]
SurjFun.on_ [abbrev, in mathcomp.classical.functions]
SurjFun_Inj [abbrev, in mathcomp.classical.functions]
SurjFun_Inj.axioms [abbrev, in mathcomp.classical.functions]
SurjFun_Inj.Build [abbrev, in mathcomp.classical.functions]
SwizzleAdd [abbrev, in mathcomp.algebra.matrix]
SwizzleLin [abbrev, in mathcomp.algebra.matrix]
symmetric_form [abbrev, in mathcomp.algebra.sesquilinear]
symmetricmx [abbrev, in mathcomp.algebra.sesquilinear]