M (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 |
M (Definitions)
mact [def, in mathcomp.finite_group.action]Magma.pack_ [def, in mathcomp.boot.monoid]
Magma.phant_clone [def, in mathcomp.boot.monoid]
Magma.phant_on_ [def, in mathcomp.boot.monoid]
Magma_isSemigroup.identity_builder [def, in mathcomp.boot.monoid]
Magma_isSemigroup.phant_axioms [def, in mathcomp.boot.monoid]
Magma_isSemigroup.phant_Build [def, in mathcomp.boot.monoid]
Magma_isUMagma.phant_axioms [def, in mathcomp.boot.monoid]
Magma_isUMagma.phant_Build [def, in mathcomp.boot.monoid]
map [def, in mathcomp.boot.seq]
map2_mx [def, in mathcomp.algebra.matrix]
map_bseq [def, in mathcomp.boot.tuple]
map_itv [def, in mathcomp.algebra.interval_inference]
map_itv_bound [def, in mathcomp.algebra.interval_inference]
map_mx [def, in mathcomp.algebra.matrix]
map_mx_is_multiplicative [def, in mathcomp.algebra.matrix]
map_mx_sum [def, in mathcomp.algebra.matrix]
map_pair [def, in mathcomp.classical.unstable]
map_poly [def, in mathcomp.algebra.poly]
map_poly_is_multiplicative [def, in mathcomp.algebra.poly]
map_tuple [def, in mathcomp.boot.tuple]
mask [def, in mathcomp.boot.seq]
mask_nat [def, in mathcomp.algebra.binnums]
MathCompCompatEquality.Equality.phant_mcpack [def, in mathcomp.boot.eqtype]
MathCompCompatSemiVector.SemiVector.phant_mcpack [def, in mathcomp.algebra.vector]
MathCompCompatSplittingField.SplittingField.phant_mcpack [def, in mathcomp.field.galois]
matrix_ind [def, in mathcomp.algebra.matrix]
matrix_of_form [def, in mathcomp.algebra.sesquilinear]
matrix_of_fun.body [def, in mathcomp.algebra.matrix]
matrix_of_fun.unlock [def, in mathcomp.algebra.matrix]
matrix_of_fun_unlock_subterm [def, in mathcomp.algebra.matrix]
matrix_of_tensor [def, in mathcomp.algebra.tensor]
matrix_rec [def, in mathcomp.algebra.matrix]
matrix_rect [def, in mathcomp.algebra.matrix]
matrix_triangle [def, in mathcomp.analysis.normedtype_theory.matrix_normedtype]
matrix_unlockable [def, in mathcomp.algebra.matrix]
MatrixFormula.eval_mx [def, in mathcomp.algebra.mxpoly]
MatrixFormula.Exists_row_form [def, in mathcomp.algebra.mxpoly]
MatrixFormula.mulmx_term [def, in mathcomp.algebra.mxpoly]
MatrixFormula.mx_term [def, in mathcomp.algebra.mxpoly]
MatrixFormula.mxrank_form [def, in mathcomp.algebra.mxpoly]
MatrixFormula.row_env [def, in mathcomp.algebra.mxpoly]
MatrixFormula.row_var [def, in mathcomp.algebra.mxpoly]
MatrixFormula.seq_of_rV [def, in mathcomp.algebra.mxpoly]
MatrixFormula.submx_form [def, in mathcomp.algebra.mxpoly]
max_g2 [def, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_monotone_convergence]
max_g2' [def, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_monotone_convergence]
max_mfun [def, in mathcomp.analysis.measurable_realfun]
max_nnsfun [def, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
max_nonzero_subdef [def, in mathcomp.reals.signed]
max_pdiv [def, in mathcomp.boot.prime]
max_reality_subdef [def, in mathcomp.reals.signed]
max_snum [def, in mathcomp.reals.signed]
maxainv [def, in mathcomp.solvable.jordanholder]
maxgroup [def, in mathcomp.finite_group.fingroup]
maximal [def, in mathcomp.solvable.gseries]
maximal [def, in mathcomp.classical.wochoice]
maximal_disjoint_subcollection [def, in mathcomp.classical.classical_sets]
maximal_eq [def, in mathcomp.solvable.gseries]
maximum_of [def, in mathcomp.classical.wochoice]
maxn [def, in mathcomp.boot.ssrnat]
maxn_snum [def, in mathcomp.reals.signed]
maxnormal [def, in mathcomp.solvable.gseries]
maxrankfun [def, in mathcomp.algebra.mxalgebra]
maxset [def, in mathcomp.boot.finset]
mdisjoint [def, in mathcomp.finmap.multiset]
mdist [def, in mathcomp.analysis.topology_theory.metric_structure]
mdist_ge0 [def, in mathcomp.analysis.topology_theory.metric_structure]
mdist_positivity [def, in mathcomp.analysis.topology_theory.metric_structure]
measurable [def, in mathcomp.analysis.measure_theory.measurable_structure]
Measurable.Exports.join_measurable_structure_Measurable_between_measurable_structure_AlgebraOfSets_and_measurable_structure_SigmaRing [def, in mathcomp.analysis.measure_theory.measurable_structure]
Measurable.pack_ [def, in mathcomp.analysis.measure_theory.measurable_structure]
Measurable.phant_clone [def, in mathcomp.analysis.measure_theory.measurable_structure]
Measurable.phant_on_ [def, in mathcomp.analysis.measure_theory.measurable_structure]
measurable0 [def, in mathcomp.analysis.measure_theory.measurable_structure]
measurable_cover [def, in mathcomp.analysis.measure_theory.measure_extension]
measurable_fun [def, in mathcomp.analysis.measure_theory.measurable_function]
measurable_funPT [def, in mathcomp.analysis.measure_theory.measurable_function]
measurable_kernel [def, in mathcomp.analysis.kernel]
measurable_subset_sigma_subadditive [def, in mathcomp.analysis.measure_theory.measure_function]
MeasurableFun.pack_ [def, in mathcomp.analysis.measure_theory.measurable_function]
MeasurableFun.phant_clone [def, in mathcomp.analysis.measure_theory.measurable_function]
MeasurableFun.phant_on_ [def, in mathcomp.analysis.measure_theory.measurable_function]
MeasurableFun_isDiscrete.identity_builder [def, in mathcomp.analysis.probability_theory.random_variable]
MeasurableFun_isDiscrete.phant_axioms [def, in mathcomp.analysis.probability_theory.random_variable]
MeasurableFun_isDiscrete.phant_Build [def, in mathcomp.analysis.probability_theory.random_variable]
measurableI [def, in mathcomp.analysis.measure_theory.measurable_structure]
measurableR [def, in mathcomp.analysis.lebesgue_stieltjes_measure]
measurableT [def, in mathcomp.analysis.measure_theory.measurable_structure]
measurableTypeR [def, in mathcomp.analysis.lebesgue_stieltjes_measure]
measurableU [def, in mathcomp.analysis.measure_theory.measurable_structure]
Measure.pack_ [def, in mathcomp.analysis.measure_theory.measure_function]
Measure.phant_clone [def, in mathcomp.analysis.measure_theory.measure_function]
Measure.phant_on_ [def, in mathcomp.analysis.measure_theory.measure_function]
measure_add [def, in mathcomp.analysis.measure_theory.measure_function]
measure_eq [def, in mathcomp.analysis.lebesgue_integral_theory.giry]
measure_extension [def, in mathcomp.analysis.measure_theory.measure_extension]
measure_fam_uub [def, in mathcomp.analysis.kernel]
measure_ge0 [def, in mathcomp.analysis.measure_theory.measure_function]
measure_inum [def, in mathcomp.analysis.measure_theory.measure_function]
measure_is_complete [def, in mathcomp.analysis.measure_theory.measure_negligible]
Measure_isFinite.phant_axioms [def, in mathcomp.analysis.measure_theory.measure_function]
Measure_isFinite.phant_Build [def, in mathcomp.analysis.measure_theory.measure_function]
Measure_isProbability.phant_axioms [def, in mathcomp.analysis.measure_theory.probability_measure]
Measure_isProbability.phant_Build [def, in mathcomp.analysis.measure_theory.probability_measure]
Measure_isSFinite.phant_axioms [def, in mathcomp.analysis.measure_theory.measure_function]
Measure_isSFinite.phant_Build [def, in mathcomp.analysis.measure_theory.measure_function]
Measure_isSigmaFinite.phant_axioms [def, in mathcomp.analysis.measure_theory.measure_function]
Measure_isSigmaFinite.phant_Build [def, in mathcomp.analysis.measure_theory.measure_function]
Measure_isSubProbability.phant_axioms [def, in mathcomp.analysis.measure_theory.probability_measure]
Measure_isSubProbability.phant_Build [def, in mathcomp.analysis.measure_theory.probability_measure]
measure_of_charge [def, in mathcomp.analysis.charge]
measure_prod_display [def, in mathcomp.analysis.measure_theory.measurable_structure]
measure_semi_additive [def, in mathcomp.analysis.measure_theory.measure_function]
measure_semi_sigma_additive [def, in mathcomp.analysis.measure_theory.measure_function]
measure_tuple_display [def, in mathcomp.analysis.measure_theory.measurable_structure]
measure_uub [def, in mathcomp.analysis.kernel]
meets [def, in mathcomp.classical.classical_sets]
mem2 [def, in mathcomp.boot.path]
mem_fin [def, in mathcomp.finmap.finmap]
mem_fun [def, in mathcomp.classical.functions]
mem_seq [def, in mathcomp.boot.seq]
mem_seq_predType [def, in mathcomp.boot.seq]
merge [def, in mathcomp.boot.path]
merge_sort_pop [def, in mathcomp.boot.path]
merge_sort_push [def, in mathcomp.boot.path]
merge_sort_rec [def, in mathcomp.boot.path]
metacyclic [def, in mathcomp.solvable.cyclic]
Metric.pack_ [def, in mathcomp.analysis.topology_theory.metric_structure]
Metric.phant_clone [def, in mathcomp.analysis.topology_theory.metric_structure]
Metric.phant_on_ [def, in mathcomp.analysis.topology_theory.metric_structure]
metric_discrete [def, in mathcomp.analysis.topology_theory.discrete_topology]
mfrestr [def, in mathcomp.analysis.measure_theory.measure_function]
mfun [def, in mathcomp.analysis.measure_theory.measurable_function]
mfun_key [def, in mathcomp.analysis.measure_theory.measurable_function]
mfun_keyed [def, in mathcomp.analysis.measure_theory.measurable_function]
mfun_Sub [def, in mathcomp.analysis.measure_theory.measurable_function]
mgFunc_id [def, in mathcomp.solvable.gfunctor]
Mho [def, in mathcomp.solvable.abelian]
Mho_gFun [def, in mathcomp.solvable.abelian]
Mho_group [def, in mathcomp.solvable.abelian]
Mho_igFun [def, in mathcomp.solvable.abelian]
Mho_mgFun [def, in mathcomp.solvable.abelian]
min_mfun [def, in mathcomp.analysis.measurable_realfun]
min_nonzero_subdef [def, in mathcomp.reals.signed]
min_reality_subdef [def, in mathcomp.reals.signed]
min_snum [def, in mathcomp.reals.signed]
mindex [def, in mathcomp.boot.seq]
mindic [def, in mathcomp.analysis.measurable_realfun]
mingroup [def, in mathcomp.finite_group.fingroup]
minimal [def, in mathcomp.classical.wochoice]
minimum_of [def, in mathcomp.classical.wochoice]
minn [def, in mathcomp.boot.ssrnat]
minn_snum [def, in mathcomp.reals.signed]
minnormal [def, in mathcomp.solvable.gseries]
minPoly [def, in mathcomp.field.fieldext]
minset [def, in mathcomp.boot.finset]
misom [def, in mathcomp.finite_group.morphism]
mk_monic [def, in mathcomp.algebra.qpoly]
mk_npoly [def, in mathcomp.algebra.qpoly]
mk_path [def, in mathcomp.analysis.homotopy_theory.continuous_path]
mk_sequence [def, in mathcomp.analysis.sequences]
mkcomp [def, in mathcomp.analysis.kernel]
mkcomp_noparam [def, in mathcomp.analysis.kernel]
mkcts [def, in mathcomp.analysis.topology_theory.topology_structure]
mkfactors [def, in mathcomp.solvable.jordanholder]
mkFcube [def, in mathcomp.solvable.burnside_app]
mkFinPredType_of [def, in mathcomp.finmap.finmap]
mkfun [def, in mathcomp.classical.functions]
mkfun_fun [def, in mathcomp.classical.functions]
mkproduct [def, in mathcomp.analysis.kernel]
mkSec [def, in mathcomp.solvable.jordanholder]
mkseq [def, in mathcomp.boot.seq]
mkset [def, in mathcomp.classical.classical_sets]
mksquare [def, in mathcomp.solvable.burnside_app]
mksrepr [def, in mathcomp.solvable.jordanholder]
mktuple [def, in mathcomp.boot.tuple]
mmt_gen_fun [def, in mathcomp.analysis.probability_theory.random_variable]
mnormalize [def, in mathcomp.analysis.measure_theory.probability_measure]
mod_action [def, in mathcomp.finite_group.action]
mod_groupAction [def, in mathcomp.finite_group.action]
modact [def, in mathcomp.finite_group.action]
modn [def, in mathcomp.boot.div]
modn_rec [def, in mathcomp.boot.div]
modular_group_generators [def, in mathcomp.solvable.extremal]
modular_gtype [def, in mathcomp.solvable.extremal]
modz [def, in mathcomp.algebra.intdiv]
monic [def, in mathcomp.algebra.poly]
monic_irreducible_poly [def, in mathcomp.field.qfpoly]
monic_pred [def, in mathcomp.algebra.poly]
Monoid.AddLaw.pack_ [def, in mathcomp.boot.bigop]
Monoid.AddLaw.phant_clone [def, in mathcomp.boot.bigop]
Monoid.AddLaw.phant_on_ [def, in mathcomp.boot.bigop]
Monoid.ComLaw.Exports.join_Monoid_ComLaw_between_SemiGroup_ComLaw_and_Monoid_Law [def, in mathcomp.boot.bigop]
Monoid.ComLaw.pack_ [def, in mathcomp.boot.bigop]
Monoid.ComLaw.phant_clone [def, in mathcomp.boot.bigop]
Monoid.ComLaw.phant_on_ [def, in mathcomp.boot.bigop]
Monoid.Exports.join_monoid_Monoid_between_monoid_BaseUMagma_and_monoid_Semigroup [def, in mathcomp.boot.monoid]
Monoid.Exports.join_monoid_Monoid_between_monoid_ChoiceBaseUMagma_and_monoid_Semigroup [def, in mathcomp.boot.monoid]
Monoid.Exports.join_monoid_Monoid_between_monoid_Semigroup_and_monoid_UMagma [def, in mathcomp.boot.monoid]
Monoid.isAddLaw.identity_builder [def, in mathcomp.boot.bigop]
Monoid.isAddLaw.phant_axioms [def, in mathcomp.boot.bigop]
Monoid.isAddLaw.phant_Build [def, in mathcomp.boot.bigop]
Monoid.isComLaw.phant_axioms [def, in mathcomp.boot.bigop]
Monoid.isComLaw.phant_Build [def, in mathcomp.boot.bigop]
Monoid.isLaw.phant_axioms [def, in mathcomp.boot.bigop]
Monoid.isLaw.phant_Build [def, in mathcomp.boot.bigop]
Monoid.isMonoidLaw.identity_builder [def, in mathcomp.boot.bigop]
Monoid.isMonoidLaw.phant_axioms [def, in mathcomp.boot.bigop]
Monoid.isMonoidLaw.phant_Build [def, in mathcomp.boot.bigop]
Monoid.isMulLaw.identity_builder [def, in mathcomp.boot.bigop]
Monoid.isMulLaw.phant_axioms [def, in mathcomp.boot.bigop]
Monoid.isMulLaw.phant_Build [def, in mathcomp.boot.bigop]
Monoid.Law.pack_ [def, in mathcomp.boot.bigop]
Monoid.Law.phant_clone [def, in mathcomp.boot.bigop]
Monoid.Law.phant_on_ [def, in mathcomp.boot.bigop]
Monoid.mul_op_Dl [def, in mathcomp.boot.bigop]
Monoid.mul_op_Dr [def, in mathcomp.boot.bigop]
Monoid.mul_zerol [def, in mathcomp.boot.bigop]
Monoid.mul_zeror [def, in mathcomp.boot.bigop]
Monoid.MulLaw.pack_ [def, in mathcomp.boot.bigop]
Monoid.MulLaw.phant_clone [def, in mathcomp.boot.bigop]
Monoid.MulLaw.phant_on_ [def, in mathcomp.boot.bigop]
Monoid.op1m [def, in mathcomp.boot.bigop]
Monoid.opm1 [def, in mathcomp.boot.bigop]
Monoid.pack_ [def, in mathcomp.boot.monoid]
Monoid.phant_clone [def, in mathcomp.boot.monoid]
Monoid.phant_on_ [def, in mathcomp.boot.monoid]
Monoid.Theory.simpm [def, in mathcomp.boot.bigop]
Monoid_isGroup.phant_axioms [def, in mathcomp.boot.monoid]
Monoid_isGroup.phant_Build [def, in mathcomp.boot.monoid]
Monoid_isStarMonoid.identity_builder [def, in mathcomp.boot.monoid]
Monoid_isStarMonoid.phant_axioms [def, in mathcomp.boot.monoid]
Monoid_isStarMonoid.phant_Build [def, in mathcomp.boot.monoid]
monoid_morphism [def, in mathcomp.boot.monoid]
monotone [def, in mathcomp.analysis.measure_theory.measurable_structure]
monotonic [def, in mathcomp.classical.unstable]
morph_act [def, in mathcomp.finite_group.action]
morph_action [def, in mathcomp.finite_group.action]
morph_dom_group [def, in mathcomp.finite_group.morphism]
morph_of_cast_perm [def, in mathcomp.finite_group.perm]
MorPhantom [def, in mathcomp.finite_group.morphism]
morphic [def, in mathcomp.finite_group.morphism]
morphim [def, in mathcomp.finite_group.morphism]
morphim_group [def, in mathcomp.finite_group.morphism]
morphism_for [def, in mathcomp.finite_group.morphism]
morphm [def, in mathcomp.finite_group.morphism]
morphm_morphism [def, in mathcomp.finite_group.morphism]
morphpre [def, in mathcomp.finite_group.morphism]
morphpre_group [def, in mathcomp.finite_group.morphism]
mpi.body [def, in mathcomp.boot.generic_quotient]
mpi.unlock [def, in mathcomp.boot.generic_quotient]
mpi_unlock [def, in mathcomp.boot.generic_quotient]
mpi_unlock_subterm [def, in mathcomp.boot.generic_quotient]
mproper [def, in mathcomp.finmap.multiset]
mrestr [def, in mathcomp.analysis.measure_theory.measure_function]
mscale [def, in mathcomp.analysis.measure_theory.measure_function]
mseries [def, in mathcomp.analysis.measure_theory.measure_function]
mset [def, in mathcomp.analysis.measure_theory.probability_measure]
mset0 [def, in mathcomp.finmap.multiset]
mset_finpredType [def, in mathcomp.finmap.multiset]
msetB [def, in mathcomp.finmap.multiset]
msetD [def, in mathcomp.finmap.multiset]
msetI [def, in mathcomp.finmap.multiset]
msetM [def, in mathcomp.finmap.multiset]
msetn [def, in mathcomp.finmap.multiset]
msetU [def, in mathcomp.finmap.multiset]
msubset [def, in mathcomp.finmap.multiset]
msum [def, in mathcomp.analysis.measure_theory.measure_function]
mu_ext [def, in mathcomp.analysis.measure_theory.measure_extension]
mul [def, in mathcomp.boot.monoid]
mul1g [def, in mathcomp.boot.monoid]
mul_fun [def, in mathcomp.boot.monoid]
mul_nnsfun [def, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
mul_nonzero_subdef [def, in mathcomp.reals.signed]
mul_pair [def, in mathcomp.boot.monoid]
mul_pair [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
mul_poly [def, in mathcomp.algebra.poly]
mul_poly_def [def, in mathcomp.algebra.poly]
mul_poly_unlockable [def, in mathcomp.algebra.poly]
mul_reality_subdef [def, in mathcomp.reals.signed]
mul_snum [def, in mathcomp.reals.signed]
MulClosed.pack_ [def, in mathcomp.boot.monoid]
MulClosed.phant_clone [def, in mathcomp.boot.monoid]
MulClosed.phant_on_ [def, in mathcomp.boot.monoid]
mule [def, in mathcomp.reals.constructive_ereal]
mule_def [def, in mathcomp.reals.constructive_ereal]
mule_defE [def, in mathcomp.reals.constructive_ereal]
mulg1 [def, in mathcomp.boot.monoid]
mulg_closed [def, in mathcomp.boot.monoid]
mulgA [def, in mathcomp.boot.monoid]
mulgm [def, in mathcomp.finite_group.gproduct]
mulgr_action [def, in mathcomp.finite_group.action]
mulmx [def, in mathcomp.algebra.matrix]
mulmxr [def, in mathcomp.algebra.matrix]
muln [def, in mathcomp.boot.ssrnat]
muln_rec [def, in mathcomp.boot.ssrnat]
muln_snum [def, in mathcomp.reals.signed]
mulq [def, in mathcomp.algebra.rat]
mulq_subdef [def, in mathcomp.algebra.rat]
mulr_infty [def, in mathcomp.reals.constructive_ereal]
mulsmx [def, in mathcomp.algebra.mxalgebra]
Multiplicative.pack_ [def, in mathcomp.boot.monoid]
Multiplicative.phant_clone [def, in mathcomp.boot.monoid]
Multiplicative.phant_on_ [def, in mathcomp.boot.monoid]
Multiplicative_isUMagmaMorphism.identity_builder [def, in mathcomp.boot.monoid]
Multiplicative_isUMagmaMorphism.phant_axioms [def, in mathcomp.boot.monoid]
Multiplicative_isUMagmaMorphism.phant_Build [def, in mathcomp.boot.monoid]
multiset [def, in mathcomp.finmap.multiset]
multiset_of [def, in mathcomp.finmap.multiset]
multiset_predType [def, in mathcomp.finmap.multiset]
mults [def, in mathcomp.algebra.tensor]
mulVg [def, in mathcomp.boot.monoid]
mx_ball [def, in mathcomp.analysis.topology_theory.matrix_topology]
mx_ent [def, in mathcomp.analysis.topology_theory.matrix_topology]
mx_ideal [def, in mathcomp.algebra.mxalgebra]
mx_inv_horner [def, in mathcomp.algebra.mxpoly]
mx_norm [def, in mathcomp.analysis.normedtype_theory.matrix_normedtype]
mx_val [def, in mathcomp.algebra.matrix]
mxblock [def, in mathcomp.algebra.matrix]
mxcol [def, in mathcomp.algebra.matrix]
mxdiag [def, in mathcomp.algebra.matrix]
mxdirect_def [def, in mathcomp.algebra.mxalgebra]
mxminpoly [def, in mathcomp.algebra.mxpoly]
mxOver [def, in mathcomp.algebra.matrix]
mxOver_pred [def, in mathcomp.algebra.matrix]
mxrank.body [def, in mathcomp.algebra.mxalgebra]
mxrank.unlock [def, in mathcomp.algebra.mxalgebra]
mxrank_unlock_subterm [def, in mathcomp.algebra.mxalgebra]
mxrank_unlockable [def, in mathcomp.algebra.mxalgebra]
mxring [def, in mathcomp.algebra.mxalgebra]
mxring_id [def, in mathcomp.algebra.mxalgebra]
mxrow [def, in mathcomp.algebra.matrix]
mxsub [def, in mathcomp.algebra.matrix]
mxtrace [def, in mathcomp.algebra.matrix]
mxtrace_is_additive [def, in mathcomp.algebra.matrix]
mxtrace_is_semi_additive [def, in mathcomp.algebra.matrix]
mxvec [def, in mathcomp.algebra.matrix]
mxvec_index [def, in mathcomp.algebra.matrix]
mxvec_is_scalable [def, in mathcomp.algebra.matrix]
mzero [def, in mathcomp.analysis.measure_theory.measure_function]