M (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 |
M (Abbreviations)
m [abbrev, in mathcomp.classical.functions]m [abbrev, in mathcomp.algebra.vector]
Magma [abbrev, in mathcomp.boot.monoid]
Magma.clone [abbrev, in mathcomp.boot.monoid]
Magma.copy [abbrev, in mathcomp.boot.monoid]
Magma.Exports.magmaType [abbrev, in mathcomp.boot.monoid]
Magma.on [abbrev, in mathcomp.boot.monoid]
Magma.on_ [abbrev, in mathcomp.boot.monoid]
Magma_isSemigroup [abbrev, in mathcomp.boot.monoid]
Magma_isSemigroup.axioms [abbrev, in mathcomp.boot.monoid]
Magma_isSemigroup.Build [abbrev, in mathcomp.boot.monoid]
Magma_isUMagma [abbrev, in mathcomp.boot.monoid]
Magma_isUMagma.axioms [abbrev, in mathcomp.boot.monoid]
Magma_isUMagma.Build [abbrev, in mathcomp.boot.monoid]
MathCompCompatEquality.Equality.axiom [abbrev, in mathcomp.boot.eqtype]
MathCompCompatEquality.Equality.axioms [abbrev, in mathcomp.boot.eqtype]
MathCompCompatEquality.Equality.class_of [abbrev, in mathcomp.boot.eqtype]
MathCompCompatEquality.Equality.mcpack [abbrev, in mathcomp.boot.eqtype]
MathCompCompatEquality.Equality.Mixin [abbrev, in mathcomp.boot.eqtype]
MathCompCompatEquality.Equality.mixin_of [abbrev, in mathcomp.boot.eqtype]
MathCompCompatSemiVector.SemiVector.axiom [abbrev, in mathcomp.algebra.vector]
MathCompCompatSemiVector.SemiVector.axioms [abbrev, in mathcomp.algebra.vector]
MathCompCompatSemiVector.SemiVector.class_of [abbrev, in mathcomp.algebra.vector]
MathCompCompatSemiVector.SemiVector.mcpack [abbrev, in mathcomp.algebra.vector]
MathCompCompatSemiVector.SemiVector.Mixin [abbrev, in mathcomp.algebra.vector]
MathCompCompatSemiVector.SemiVector.mixin_of [abbrev, in mathcomp.algebra.vector]
MathCompCompatSplittingField.SplittingField.axiom [abbrev, in mathcomp.field.galois]
MathCompCompatSplittingField.SplittingField.axioms [abbrev, in mathcomp.field.galois]
MathCompCompatSplittingField.SplittingField.class_of [abbrev, in mathcomp.field.galois]
MathCompCompatSplittingField.SplittingField.mcpack [abbrev, in mathcomp.field.galois]
MathCompCompatSplittingField.SplittingField.Mixin [abbrev, in mathcomp.field.galois]
MathCompCompatSplittingField.SplittingField.mixin_of [abbrev, in mathcomp.field.galois]
MathCompCompatVector.Vector.axiom [abbrev, in mathcomp.algebra.vector]
MathCompCompatVector.Vector.class_of [abbrev, in mathcomp.algebra.vector]
matrix_of_fun [abbrev, in mathcomp.algebra.matrix]
MatrixFormula.Add [abbrev, in mathcomp.algebra.mxpoly]
MatrixFormula.And [abbrev, in mathcomp.algebra.mxpoly]
MatrixFormula.Bool [abbrev, in mathcomp.algebra.mxpoly]
MatrixFormula.eval [abbrev, in mathcomp.algebra.mxpoly]
MatrixFormula.False [abbrev, in mathcomp.algebra.mxpoly]
MatrixFormula.form [abbrev, in mathcomp.algebra.mxpoly]
MatrixFormula.holds [abbrev, in mathcomp.algebra.mxpoly]
MatrixFormula.morphAnd [abbrev, in mathcomp.algebra.mxpoly]
MatrixFormula.qf_eval [abbrev, in mathcomp.algebra.mxpoly]
MatrixFormula.qf_form [abbrev, in mathcomp.algebra.mxpoly]
MatrixFormula.term [abbrev, in mathcomp.algebra.mxpoly]
MatrixFormula.True [abbrev, in mathcomp.algebra.mxpoly]
max [abbrev, in mathcomp.classical.boolp]
maxe [abbrev, in mathcomp.reals.constructive_ereal]
maxeMl [abbrev, in mathcomp.reals.constructive_ereal]
maxeMr [abbrev, in mathcomp.reals.constructive_ereal]
Measurable [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
Measurable.clone [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
Measurable.copy [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
Measurable.Exports.measurableType [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
Measurable.on [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
Measurable.on_ [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
measurable_fun_prod [abbrev, in mathcomp.analysis.measure_theory.measurable_function]
measurable_pair1 [abbrev, in mathcomp.analysis.measure_theory.measurable_function]
measurable_pair2 [abbrev, in mathcomp.analysis.measure_theory.measurable_function]
measurable_sfun_inP [abbrev, in mathcomp.analysis.lebesgue_stieltjes_measure]
measurable_sfunP [abbrev, in mathcomp.analysis.measure_theory.measurable_function]
MeasurableFun [abbrev, in mathcomp.analysis.measure_theory.measurable_function]
MeasurableFun.clone [abbrev, in mathcomp.analysis.measure_theory.measurable_function]
MeasurableFun.copy [abbrev, in mathcomp.analysis.measure_theory.measurable_function]
MeasurableFun.on [abbrev, in mathcomp.analysis.measure_theory.measurable_function]
MeasurableFun.on_ [abbrev, in mathcomp.analysis.measure_theory.measurable_function]
MeasurableFun_isDiscrete [abbrev, in mathcomp.analysis.probability_theory.random_variable]
MeasurableFun_isDiscrete.axioms [abbrev, in mathcomp.analysis.probability_theory.random_variable]
MeasurableFun_isDiscrete.Build [abbrev, in mathcomp.analysis.probability_theory.random_variable]
Measure [abbrev, in mathcomp.analysis.measure_theory.measure_function]
Measure.clone [abbrev, in mathcomp.analysis.measure_theory.measure_function]
Measure.copy [abbrev, in mathcomp.analysis.measure_theory.measure_function]
Measure.Exports.measure [abbrev, in mathcomp.analysis.measure_theory.measure_function]
Measure.on [abbrev, in mathcomp.analysis.measure_theory.measure_function]
Measure.on_ [abbrev, in mathcomp.analysis.measure_theory.measure_function]
measure_dominates_ae_eq [abbrev, in mathcomp.analysis.measure_theory.measure_negligible]
Measure_isFinite [abbrev, in mathcomp.analysis.measure_theory.measure_function]
Measure_isFinite.axioms [abbrev, in mathcomp.analysis.measure_theory.measure_function]
Measure_isFinite.Build [abbrev, in mathcomp.analysis.measure_theory.measure_function]
Measure_isProbability [abbrev, in mathcomp.analysis.measure_theory.probability_measure]
Measure_isProbability.axioms [abbrev, in mathcomp.analysis.measure_theory.probability_measure]
Measure_isProbability.Build [abbrev, in mathcomp.analysis.measure_theory.probability_measure]
Measure_isSFinite [abbrev, in mathcomp.analysis.measure_theory.measure_function]
Measure_isSFinite.axioms [abbrev, in mathcomp.analysis.measure_theory.measure_function]
Measure_isSFinite.Build [abbrev, in mathcomp.analysis.measure_theory.measure_function]
Measure_isSigmaFinite [abbrev, in mathcomp.analysis.measure_theory.measure_function]
Measure_isSigmaFinite.axioms [abbrev, in mathcomp.analysis.measure_theory.measure_function]
Measure_isSigmaFinite.Build [abbrev, in mathcomp.analysis.measure_theory.measure_function]
Measure_isSubProbability [abbrev, in mathcomp.analysis.measure_theory.probability_measure]
Measure_isSubProbability.axioms [abbrev, in mathcomp.analysis.measure_theory.probability_measure]
Measure_isSubProbability.Build [abbrev, in mathcomp.analysis.measure_theory.probability_measure]
mem_1B_itvcc [abbrev, in mathcomp.classical.set_interval]
Metric [abbrev, in mathcomp.analysis.topology_theory.metric_structure]
Metric.clone [abbrev, in mathcomp.analysis.topology_theory.metric_structure]
Metric.copy [abbrev, in mathcomp.analysis.topology_theory.metric_structure]
Metric.Exports.metricType [abbrev, in mathcomp.analysis.topology_theory.metric_structure]
Metric.on [abbrev, in mathcomp.analysis.topology_theory.metric_structure]
Metric.on_ [abbrev, in mathcomp.analysis.topology_theory.metric_structure]
metricType_numDomainType.ball_mdist [abbrev, in mathcomp.analysis.topology_theory.metric_structure]
metricType_numDomainType.nbhs_mdist [abbrev, in mathcomp.analysis.topology_theory.metric_structure]
mfun [abbrev, in mathcomp.analysis.measure_theory.measurable_function]
min [abbrev, in mathcomp.classical.boolp]
mine [abbrev, in mathcomp.reals.constructive_ereal]
mineMl [abbrev, in mathcomp.reals.constructive_ereal]
mineMr [abbrev, in mathcomp.reals.constructive_ereal]
minkowski [abbrev, in mathcomp.analysis.hoelder]
mk [abbrev, in mathcomp.boot.bigop]
mk_mon [abbrev, in mathcomp.algebra.mxpoly]
mkbigO [abbrev, in mathcomp.analysis.landau]
mkbigO [abbrev, in mathcomp.analysis.landau]
mkbigOmega [abbrev, in mathcomp.analysis.landau]
mkbigOmega [abbrev, in mathcomp.analysis.landau]
mkbigTheta [abbrev, in mathcomp.analysis.landau]
mkbigTheta [abbrev, in mathcomp.analysis.landau]
mkFinPredType [abbrev, in mathcomp.finmap.finmap]
mklittleo [abbrev, in mathcomp.analysis.landau]
mklittleo [abbrev, in mathcomp.analysis.landau]
mklittleo [abbrev, in mathcomp.analysis.landau]
Monoid [abbrev, in mathcomp.boot.monoid]
Monoid.add_law [abbrev, in mathcomp.boot.bigop]
Monoid.AddLaw [abbrev, in mathcomp.boot.bigop]
Monoid.AddLaw.clone [abbrev, in mathcomp.boot.bigop]
Monoid.AddLaw.copy [abbrev, in mathcomp.boot.bigop]
Monoid.AddLaw.on [abbrev, in mathcomp.boot.bigop]
Monoid.AddLaw.on_ [abbrev, in mathcomp.boot.bigop]
Monoid.Builders_15.op1m [abbrev, in mathcomp.boot.bigop]
Monoid.Builders_15.opA [abbrev, in mathcomp.boot.bigop]
Monoid.Builders_15.opC [abbrev, in mathcomp.boot.bigop]
Monoid.Builders_8.op1m [abbrev, in mathcomp.boot.bigop]
Monoid.Builders_8.opA [abbrev, in mathcomp.boot.bigop]
Monoid.Builders_8.opm1 [abbrev, in mathcomp.boot.bigop]
Monoid.clone [abbrev, in mathcomp.boot.monoid]
Monoid.com_law [abbrev, in mathcomp.boot.bigop]
Monoid.ComLaw [abbrev, in mathcomp.boot.bigop]
Monoid.ComLaw.clone [abbrev, in mathcomp.boot.bigop]
Monoid.ComLaw.copy [abbrev, in mathcomp.boot.bigop]
Monoid.ComLaw.on [abbrev, in mathcomp.boot.bigop]
Monoid.ComLaw.on_ [abbrev, in mathcomp.boot.bigop]
Monoid.copy [abbrev, in mathcomp.boot.monoid]
Monoid.Exports.monoidType [abbrev, in mathcomp.boot.monoid]
Monoid.isAddLaw [abbrev, in mathcomp.boot.bigop]
Monoid.isAddLaw.axioms [abbrev, in mathcomp.boot.bigop]
Monoid.isAddLaw.Build [abbrev, in mathcomp.boot.bigop]
Monoid.isComLaw [abbrev, in mathcomp.boot.bigop]
Monoid.isComLaw.axioms [abbrev, in mathcomp.boot.bigop]
Monoid.isComLaw.Build [abbrev, in mathcomp.boot.bigop]
Monoid.isLaw [abbrev, in mathcomp.boot.bigop]
Monoid.isLaw.axioms [abbrev, in mathcomp.boot.bigop]
Monoid.isLaw.Build [abbrev, in mathcomp.boot.bigop]
Monoid.isMonoidLaw [abbrev, in mathcomp.boot.bigop]
Monoid.isMonoidLaw.axioms [abbrev, in mathcomp.boot.bigop]
Monoid.isMonoidLaw.Build [abbrev, in mathcomp.boot.bigop]
Monoid.isMulLaw [abbrev, in mathcomp.boot.bigop]
Monoid.isMulLaw.axioms [abbrev, in mathcomp.boot.bigop]
Monoid.isMulLaw.Build [abbrev, in mathcomp.boot.bigop]
Monoid.law [abbrev, in mathcomp.boot.bigop]
Monoid.Law [abbrev, in mathcomp.boot.bigop]
Monoid.Law.clone [abbrev, in mathcomp.boot.bigop]
Monoid.Law.copy [abbrev, in mathcomp.boot.bigop]
Monoid.Law.on [abbrev, in mathcomp.boot.bigop]
Monoid.Law.on_ [abbrev, in mathcomp.boot.bigop]
Monoid.mul_law [abbrev, in mathcomp.boot.bigop]
Monoid.MulLaw [abbrev, in mathcomp.boot.bigop]
Monoid.MulLaw.clone [abbrev, in mathcomp.boot.bigop]
Monoid.MulLaw.copy [abbrev, in mathcomp.boot.bigop]
Monoid.MulLaw.on [abbrev, in mathcomp.boot.bigop]
Monoid.MulLaw.on_ [abbrev, in mathcomp.boot.bigop]
Monoid.on [abbrev, in mathcomp.boot.monoid]
Monoid.on_ [abbrev, in mathcomp.boot.monoid]
monoid_closed [abbrev, in mathcomp.boot.monoid]
Monoid_isGroup [abbrev, in mathcomp.boot.monoid]
Monoid_isGroup.axioms [abbrev, in mathcomp.boot.monoid]
Monoid_isGroup.Build [abbrev, in mathcomp.boot.monoid]
Monoid_isStarMonoid [abbrev, in mathcomp.boot.monoid]
Monoid_isStarMonoid.axioms [abbrev, in mathcomp.boot.monoid]
Monoid_isStarMonoid.Build [abbrev, in mathcomp.boot.monoid]
morPhantom [abbrev, in mathcomp.finite_group.morphism]
mpi [abbrev, in mathcomp.boot.generic_quotient]
mu [abbrev, in mathcomp.analysis.probability_theory.uniform_distribution]
mu [abbrev, in mathcomp.analysis.probability_theory.random_variable]
mu [abbrev, in mathcomp.analysis.probability_theory.normal_distribution]
mu [abbrev, in mathcomp.analysis.probability_theory.exponential_distribution]
mu [abbrev, in mathcomp.analysis.probability_theory.exponential_distribution]
mu [abbrev, in mathcomp.analysis.probability_theory.beta_distribution]
mu [abbrev, in mathcomp.analysis.probability_theory.beta_distribution]
mu [abbrev, in mathcomp.analysis.probability_theory.beta_distribution]
mu [abbrev, in mathcomp.analysis.probability_theory.beta_distribution]
mu [abbrev, in mathcomp.analysis.probability_theory.beta_distribution]
mu [abbrev, in mathcomp.analysis.probability_theory.beta_distribution]
mu [abbrev, in mathcomp.analysis.lebesgue_measure]
mu [abbrev, in mathcomp.analysis.lebesgue_measure]
mu [abbrev, in mathcomp.analysis.lebesgue_measure]
mu [abbrev, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_nonneg]
mu [abbrev, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_nonneg]
mu [abbrev, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation]
mu [abbrev, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation]
mu [abbrev, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation]
mu [abbrev, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation]
mu [abbrev, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation]
mu [abbrev, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation]
mu [abbrev, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation]
mu [abbrev, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation]
mu [abbrev, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation]
mu [abbrev, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_Rintegral]
mu [abbrev, in mathcomp.analysis.ftc]
mu [abbrev, in mathcomp.analysis.ftc]
mu [abbrev, in mathcomp.analysis.ftc]
mu [abbrev, in mathcomp.analysis.ftc]
mu [abbrev, in mathcomp.analysis.ftc]
mu [abbrev, in mathcomp.analysis.ftc]
mu [abbrev, in mathcomp.analysis.ftc]
mu [abbrev, in mathcomp.analysis.charge]
mu [abbrev, in mathcomp.analysis.charge]
mu_int [abbrev, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integrable]
mul1g [abbrev, in mathcomp.finite_group.fingroup]
MulClosed [abbrev, in mathcomp.boot.monoid]
MulClosed.clone [abbrev, in mathcomp.boot.monoid]
MulClosed.copy [abbrev, in mathcomp.boot.monoid]
MulClosed.Exports.mulgClosed [abbrev, in mathcomp.boot.monoid]
MulClosed.on [abbrev, in mathcomp.boot.monoid]
MulClosed.on_ [abbrev, in mathcomp.boot.monoid]
mulg [abbrev, in mathcomp.finite_group.fingroup]
mulg1 [abbrev, in mathcomp.finite_group.fingroup]
mulgA [abbrev, in mathcomp.finite_group.fingroup]
mulgI [abbrev, in mathcomp.finite_group.fingroup]
mulgK [abbrev, in mathcomp.finite_group.fingroup]
mulgKV [abbrev, in mathcomp.finite_group.fingroup]
mulgV [abbrev, in mathcomp.finite_group.fingroup]
mulKg [abbrev, in mathcomp.finite_group.fingroup]
mulKVg [abbrev, in mathcomp.finite_group.fingroup]
mulrzDl_tmp [abbrev, in mathcomp.algebra.ssrint]
mulrzDr_tmp [abbrev, in mathcomp.algebra.ssrint]
Multiplicative [abbrev, in mathcomp.boot.monoid]
Multiplicative.clone [abbrev, in mathcomp.boot.monoid]
Multiplicative.copy [abbrev, in mathcomp.boot.monoid]
Multiplicative.on [abbrev, in mathcomp.boot.monoid]
Multiplicative.on_ [abbrev, in mathcomp.boot.monoid]
Multiplicative_isUMagmaMorphism [abbrev, in mathcomp.boot.monoid]
Multiplicative_isUMagmaMorphism.axioms [abbrev, in mathcomp.boot.monoid]
Multiplicative_isUMagmaMorphism.Build [abbrev, in mathcomp.boot.monoid]
mulVg [abbrev, in mathcomp.finite_group.fingroup]
mxdirect [abbrev, in mathcomp.algebra.mxalgebra]
mxdirect [abbrev, in mathcomp.algebra.mxalgebra]
mxf [abbrev, in mathcomp.algebra.mxalgebra]
mxrank [abbrev, in mathcomp.algebra.mxalgebra]
mxrank [abbrev, in mathcomp.algebra.mxalgebra]