Glossary: M

Definitions in this project whose names start with M. The whole glossary has the other sections.

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 · Other

M def

$M(n)$ is the number of monotone Boolean functions on $n$ variables. · DedekindNumber.M

M def

Let $M_n = \max_{|z| = 1} |p_n(z)|$. · Erdos119.M

M def

Let $A$ and $B$ be two complementary subsets, a splitting of the numbers $\{1, 2, \dots, 2n\}$, such that both have the same cardinality $n$. Define $M(n)$ to be the minimum MaxOverlap that can be achieved, ranging over all such … · Erdos36.M

M def

The maximum of $\sum_{n\in A}\frac{1}{n}$ over all admissible $A\subseteq \{1,\ldots,N\}$. · Erdos858.M

M def

For $f = a_0 + \cdots + a_dx^d$, the quantity $M=\frac{\lvert a_0\rvert+\cdots +\lvert a_d\rvert}{(\lvert a_0\rvert\lvert a_d\rvert)^{1/2}}$. · Erdos990.M

m def

m N = ⌊∑_{n ≤ N} 1/n⌋. · Erdos308.m

m def

Let $m_n$ be the smallest integer such that $n\mid \phi(m_n)$. · Erdos456.m

m def

$m(f)=\min_{|z|=1}|f(z)|$. · Erdos525.m

m def

m(n, k): minimal sunflower-forcing family size in the non-uniform [n] model. · Erdos857.m

m def

This is $m(p)$ in [Be23]: the size of the smallest set $A \subset \mathbb{Z} / p\mathbb{Z}$ (with at least two elements) for which no element in the sumset $A + A$ has a unique representation. · Green27.m

m def

The minimum size of a subset of ℕ that contains, for each d = 1, …, N, an arithmetic progression of length k with common difference d. · Green37.m

m def

The matrix for the specific case $a=5, b=2$. $$M = \begin{pmatrix} 1 & 5 \cr 1 & 2 \end{pmatrix}$$ · OeisA108306.m

M' def

$M'(n)$ is the number of antichains (Sperner families) of subsets of Fin n. · DedekindNumber.M'

Machine def

A Post-Turing machine with symbol type Γ and label type Λ is a function which, given the current state q : Λ and the tape head a : Γ, either halts (returns none) or returns a new state q' : Option Λ and a Stmt describing what … · Turing.BusyBeaver.Machine

Magma class

class Magma (α : Type) · EquationalTheories_677_255.Magma

mahlerMeasure def

The Mahler measure of f(X) is defined as ‖a‖ ∏ᵢ max(1,‖αᵢ‖), where f(X)=a(X-α₁)(X-α₂)...(X-αₙ). · LehmerMahlerMeasureProblem.mahlerMeasure

mahlerMeasureZ def

def mahlerMeasureZ (f : ℤ[X]) : ℝ · LehmerMahlerMeasureProblem.mahlerMeasureZ

mandelbrotSet abbrev

The Mandelbrot set is the special case of the multibrot set for n = 2. In other words, it is the set of all parameters c : ℂ for which 0 does not escape to infinity under repeated application of z ↦ z ^ 2 + c. · Mandelbrot.mandelbrotSet

map def

An embedding of fields induces a continuous homomorphism of absolute Galois groups. Note that this depends on an arbitrary choice of embedding of the algebraic closures. · Field.absoluteGaloisGroup.map

mapOfAlgebra def

A commuting square of two fields and their algebraic closures induces a continuous homomorphism of their absolute Galois groups. · Field.absoluteGaloisGroup.mapOfAlgebra

marks def

A ruler is described by its list of segment lengths (gaps) g, so that its marks are the partial sums $0 = m_0 < m_1 < \cdots < m_n = L$, where $n$ (g.length) is the number of segments and $L$ (g.sum) is the length. · SparseRuler.marks

matchingNumber def

matchingNumber G is the size of a maximum matching of G. · SimpleGraph.matchingNumber

matchingProbability def

Probability of a matching in a uniformly chosen fixed-size edge family. This is the cardinality of the event divided by that of the finite sample space; it is zero when m exceeds the number of possible edges. · Hypergraph.matchingProbability

matrixHattoriStallingsTraceAt def

The value at the conjugacy class of g of the universal trace of a matrix over R[G]. · Arxiv.«math.0703548».matrixHattoriStallingsTraceAt

max013AffineTranslates def

The maximum number of $\lbrace 0,1,3 \rbrace$ affine translates that a set of size $n$ can contain. · Green24.max013AffineTranslates

max_gap def

The maximum gap between consecutive terms of a finite sequence s : Fin k → ℕ, i.e., $\max_{0 \le i < k-1} (s(i+1) - s(i))$. · Erdos287.max_gap

maxAPFreeCard def

Define the largest possible size of a subset of a finset s that does not contain any non-trivial k-term arithmetic progression. · Finset.maxAPFreeCard

maxArithInterCard def

For each $N > 0$, let $t$ be the largest size of an arithmetic intersection set. · Erdos272.maxArithInterCard

maxBoundaryLength def

$\Lambda(f)$, the maximum of the lengths of the boundaries of the connected components of $\{ z: \lvert f(z)\rvert<1\}$, where the length of a subset of $\mathbb{C}$ is its $1$-dimensional Hausdorff measure. · Erdos1044.maxBoundaryLength

maxCard def

The largest size of an admissible subset of {1, …, N}. · Erdos534.maxCard

maxCard def

Define the largest possible size of a subset of $\{1, \dots, N\}$ that does not contain any non-trivial $k$-term arithmetic progression. · Set.IsAPOfLengthFree.maxCard

maxChromaticCliqueRatio def

maxChromaticCliqueRatio n is $f(n)$, the maximum of $\chi(G)/\omega(G)$ over all graphs $G$ on $n$ vertices. · Erdos627.maxChromaticCliqueRatio

maxCollinear def

The largest number of points of P on a single line. · Erdos102.maxCollinear

maxConvexUnitDistances def

The maximum number of unit distances determined by the vertices of a convex $n$-gon. This function is often denoted as $U_c(n)$ in combinatorics. · Erdos96.maxConvexUnitDistances

maxCosetDim def

def maxCosetDim (K V : Type*) [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (A : Set V) : ℕ · maxCosetDim

maxDepth def

The largest $d \leq r$ such that $\sum_{i \in I} a_i \equiv 0 \pmod{2^d}$ for some non-empty subset $I \subseteq [k]$, where $a_1, \dots, a_k \in \mathbb{Z}/2^r\mathbb{Z}$. · Green21.maxDepth

maxEccentricityVertices def

The set of vertices of maximum eccentricity. · SimpleGraph.maxEccentricityVertices

maxEigenvalue def

def Matrix.IsHermitian.maxEigenvalue {𝕜 : Type*} [RCLike 𝕜] {n : Type*} [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.IsHermitian) : ℝ · Matrix.IsHermitian.maxEigenvalue

maxEquidistantPointsAt def

For a given point x and a set of other points, this function finds the maximum number of points that lie on a single circle centered at x. It does this by grouping the other points by their distance to x and finding the size of the … · Erdos92.maxEquidistantPointsAt

maxEvenCorrection def

The maximum of $\operatorname{distEven}(v)-\operatorname{evenHorizontal}(v)$. · WrittenOnTheWallII.GraphConjecture309.maxEvenCorrection

maxEvenDistance def

Maximum even distance between distinct vertices in G. Only positive even distances are considered. Returns 0 if no such distance exists. · SimpleGraph.maxEvenDistance

maximalDistinctDistancesFrom def

Let $x_1,\ldots,x_n\in \mathbb{R}^2$ and let $R(x_i)=\#\{ \lvert x_j-x_i\rvert : j\neq i\}$, where the points are ordered such that $$R(x_1)\leq \cdots \leq R(x_n).$$ Let $g(n)$ be the maximum number of distinct values the $R(x_i)$ can … · EuclideanGeometry.maximalDistinctDistancesFrom

maximalLength def

Let $F(n)$ be the maximal length of a $2$-increasing sequence of triples with each coordinate belong to $[n]$ ($= \{1, 2, ..., n\}$). · Arxiv.«1609.08688».maximalLength

maximallyMixed def

The maximally mixed state on $m$ parties. · OpenQuantumProblem35.maximallyMixed

maxLocalIndependence def

Maximum local independence number over all vertices. For each vertex, we compute the independence number of the subgraph induced by its neighbors, and take the maximum over all vertices. · SimpleGraph.maxLocalIndependence

maxLogOne def

The function $\operatorname{Log} x := \max\{log x, 1\}$. · Erdos442.Real.maxLogOne

maxMass def

The largest reciprocal sum ∑_{n ∈ A} 1/n over admissible A ⊆ {1, …, N}. · Erdos538.maxMass

maxMinimalCuts def

The maximum number $c(n)$ of minimal cuts a graph on $n$ vertices can have. · Erdos150.maxMinimalCuts

MaxNotSqSum def

MaxNotSqSum N is the size of the largest subset A of {1,...,N} such that for all non-empty S ⊆ A, the sum ∑ n ∈ S, n is not a square. · Erdos587.MaxNotSqSum

MaxOverlap def

The maximum overlap for a given pair of sets $A$ and $B$, taken over all possible integer differences $k$. · Erdos36.MaxOverlap

maxOverlapC def

A computable stand-in for MaxOverlap. Overlap is already computable; the only obstacle is the iSup, and maxOverlap_eq_sup says it agrees with this Finset.sup. · Erdos36.maxOverlapC

maxPrimeFac def

The greatest prime divisor of a natural number n > 1. · Nat.maxPrimeFac

maxRestrictedSumAvoidingSubsetSize def

We define the construction from [Sa21, p1] as $M(A) := \max \{|S| : S \subseteq A \text{ and } (S \hat{+} S) \cap A = \varnothing \}$. · Green2.maxRestrictedSumAvoidingSubsetSize

maxRichDistances def

The largest number of distinct distances that a set of n points in $\mathbb{R}^2$ can determine, each of which occurs for more than n many pairs of points of the set. · Erdos756.maxRichDistances

maxSidonSubsetCard def

The maximum size of a Sidon set in the supplied Finset. · Finset.maxSidonSubsetCard

maxSubgraphEdgeDistToBipartite def

For a given graph $G$ and size $n$, this defines the smallest number $k$ such that any subgraph of $G$ on $n$ vertices can be made bipartite by deleting at most $k$ edges. · Erdos74.SimpleGraph.maxSubgraphEdgeDistToBipartite

maxSubsetSumAvoidingCard def

The largest cardinality of a set $A \subseteq \{1, \ldots, N\}$ such that no subset of $A$ sums to $n$. · Erdos361.maxSubsetSumAvoidingCard

MaxTemp def

Maximum of temp_v over all vertices. · SimpleGraph.MaxTemp

maxTrianglesAtVertex def

The maximum number of triangles incident to any vertex in $G$. · WrittenOnTheWallII.GraphConjecture160.maxTrianglesAtVertex

maxUnionFree def

The largest size of a union-free collection $\mathcal{F}$ of subsets of $[n]$. · Erdos447.maxUnionFree

maxUnitCircleCount def

The maximum number of qualifying unit circles attained by a configuration of n points. · Erdos104.maxUnitCircleCount

maxUnitDistances def

The maximum number of unit distances determined by any set of $n$ points in the plane. This function is often denoted as $u(n)$ in combinatorics. · Erdos90.maxUnitDistances

MaxWeaklyDivisible def

MaxWeaklyDivisible N k is the size of the largest k-weakly divisible subset of {1,..., N} · Erdos56.MaxWeaklyDivisible

maxY def

The maximum $y$ for a given $x$, cast to a real number for asymptotics. · Green46.maxY

Mem def

Membership in the half-open cube ∏ j, [lower j, lower j + side). · Erdos769.Cube.Mem

menageDenomTerm def

The denominator term $k! (n-1)_k$ represented as a Real number. · OeisA258667.menageDenomTerm

middleColumnBit def

The sequence of bits forming the middle column of the CA pattern, $C_{t, 0}$. · OeisA267581.middleColumnBit

MilnorK abbrev

The Milnor K-ring K^M_*(F)/ℓ of the field F with coefficients in ℤ/ℓ. For ℓ = 0 this is the Milnor K-ring K^M_*(F). · MilnorK

MinAsymptoticAddBasisOfOrder def

An asymptotic additive basis of order h is minimal when one cannot obtain an asymptotic additive basis by removing any element from it. · Erdos330.MinAsymptoticAddBasisOfOrder

minChromaticEdges def

Minimum edge count for chromatic number k, with infinity when no such graph exists. · Hypergraph.minChromaticEdges

minColours def

$c(a_1, \dots, a_k)$, the least number of colours required in order to colour $\mathbb{N}$ so that there is no monochromatic solution to $a_1x_1 + \cdots + a_kx_k = 0$. · Green21.minColours

minComplementEdgeNeighborhood def

The minimum complement-edge neighborhood-union order, when a complement edge exists. · WrittenOnTheWallII.GraphConjecture309.minComplementEdgeNeighborhood

minCopies def

The minimal number of rotated copies of the pyjama set of width ε needed to cover the plane. · Green41.minCopies

minDensity def

The minimal covering density over all covering subspaces for a given n and r. We compute in ℝ≥0∞ (ENNReal) to gracefully handle any potential divergence. · Green40.minDensity

minDensityFinset def

def minDensityFinset (n r : ℕ) : ℝ≥0∞ · Green40.minDensityFinset

minEdgeDistToBipartite def

The minimum number of edges that must be deleted from a subgraph A to make it bipartite. · Erdos74.SimpleGraph.minEdgeDistToBipartite

minEvenDistance def

Minimum even distance between distinct vertices in G. Only positive even distances are considered. Returns 0 if no such distance exists. · SimpleGraph.minEvenDistance

minimalCrossDistances def

The minimal number of distinct distances $d(x_i, y_j)$ over all choices of $2n$ distinct points $x_1, \ldots, x_n, y_1, \ldots, y_n$ in X. · Erdos661.minimalCrossDistances

minimalDiscriminant def

The minimal discriminant ideal of an elliptic curve over a number field is the product of the local minimal discriminant ideals v.asIdeal ^ W.minimalDiscriminantExponent v over all nonzero prime ideals v of its ring of integers. Only … · WeierstrassCurve.minimalDiscriminant

minimalDiscriminantExponent def

The exponent of v in the minimal discriminant ideal of W: the natural number n such that the discriminant of a minimal model over the v-adic completion has valuation exp (-n). A vanishing discriminant has valuation 0, whose … · WeierstrassCurve.minimalDiscriminantExponent

minimalDistinctDistances def

The minimum number of distinct distances determined by a set of n points in X. · minimalDistinctDistances

minIntersectingEdges def

Least number of edges in an intersecting r-uniform family with transversal size r. Infinity records a missing witness. · Hypergraph.minIntersectingEdges

minLocalIndependence def

Minimum local independence number over all vertices. For each vertex, we compute the independence number of the subgraph induced by its neighbors, and take the minimum over all vertices. · SimpleGraph.minLocalIndependence

minMaximalSidonSet def

The size of the smallest maximal Sidon set in $\{1, \dots, N\}$. · Erdos156.minMaximalSidonSet

minModulus def

The candidate least modulus admitting a valid set of n residues, conjecturally $2^n - 2^{\lfloor\log_2 n\rfloor}$. · Arxiv.«2607.08366».minModulus

minNewEdges def

For a graph $G$, minNewEdges r G is the smallest number of edges that need to be added to $G$ so that it has diameter at most $r$, while preserving the property of being triangle-free. Erdős, Gyárfás and Ruszinkó denote this quantity by … · Erdos619.minNewEdges

MinOverlapQuotient def

The quotient of the minimum maximum overlap $M(N)$ by $N$. The central question of the minimum overlap problem is to determine the asymptotic behavior of this quotient as $N \to \infty$. · Erdos36.MinOverlapQuotient

minTriangleArea def

The minimum (unsigned) area of a triangle determined by three distinct points in a set S. Collinear triples count with area 0. EuclideanGeometry.triangle_area is a signed area, so the absolute value is taken before the infimum. · Erdos507.minTriangleArea

minTrianglesAtVertex def

The minimum number of triangles incident to any vertex, over all vertices of $G$. · WrittenOnTheWallII.GraphConjecture291.minTrianglesAtVertex

minZeros def

The minimum number of zeros in $[0,1)$ of $\sum_{a \in A} \cos(2\pi a\theta)$ over all sets $A \subset \mathbb{Z}$ of size $n$. · Green82.minZeros

mixedMonoAPGuaranteeSet def

The set of natural numbers $N$ such that any 2-coloring of ${1, ..., N}$ contains a monochromatic arithmetic progression of length $k$ (color 0) or length $r$ (color 1). · Green14.mixedMonoAPGuaranteeSet

mkAMSSyntax def

def mkAMSSyntax (nums : TSyntaxArray `num) : CommandElabM <| TSyntax ``attrInstance · AMSLinter.mkAMSSyntax

mkAnswerAnnotation def

def mkAnswerAnnotation (e : Expr) : Expr · Google.mkAnswerAnnotation

mkCanonicalSorryAnnotation def

Construct a canonical sorryAx application with a stable, module-independent tag. Unlike Lean's built-in sorry macro, this does not embed the current module name via hygiene, so the resulting expression is identical regardless of … · Google.mkCanonicalSorryAnnotation

mkEdge def

Helper: build an EdgeN from endpoints and endpoint indices. · MonochromaticQuantumGraph.mkEdge

mkMachineMatchAltExpr def

Take as input a list of strings and return an array of matchAltExpr syntaxes mapping (state, symbol) pairs to actions of a Turing Machine, given by a term of type Option (State n). · mkMachineMatchAltExpr

mkStateType def

mkStateType n adds to the environment an inductive type with n states names State{n} with constructors the symbols A, B, ..., together with the instance Inhabited (State{n}). · mkStateType

mkStateVector abbrev

Build a state vector from its coordinates in the computational basis. · OpenQuantumProblem23.mkStateVector

mkStateVector abbrev

Build a state vector from its computational-basis amplitudes. · OpenQuantumProblem35.mkStateVector

mMin def

mMin n is the minimal m such that $\sum_{n\leq k\leq m}\frac{1}{k}\geq 1$; such an m exists for n ≥ 1 since the harmonic series diverges. · Erdos314.mMin

modularFormAn def

The n-th Fourier coefficient of a modular form (around the cusp at infinity). · ModularityConjecture.modularFormAn

modularityConjecture def

See theorem 8.8.1 of [diamondshurman2005]. · ModularityConjecture.modularityConjecture

moduleDocstringLinter def

The module docstring linter checks two things: - A file that has no /-! ... -/ block gets a warning on its first non-moduleDoc command. - A file that has more than one /-! ... -/ block gets a warning on each extra block. · ModuleDocstringLinter.moduleDocstringLinter

moment def

The $k$th moment of the Riemann zeta function is the integral $$ \frac{1}{T}\int_0^T |\zeta(1/2 + it)|^{2k}dt. $$ · RiemannZetaMoments.moment

monoAP_guarantee_set def

The set of natural numbers that guarantee a monochromatic arithmetic progression. · Erdos138.monoAP_guarantee_set

monoAPNumber def

The van der Waerden number, is the smallest integer N such that any r-coloring of {1, ..., N} is guaranteed to contain a monochromatic arithmetic progression of length k. It is defined as the infimum of the (non-empty) set of … · Erdos138.monoAPNumber

monochromaticGraph def

The monochromatic subgraph of color i under edge coloring c : Sym2 V → Fin n. · Erdos609.monochromaticGraph

MonochromaticHasOddCycleLe def

A coloring c has a monochromatic odd cycle of length at most m. · Erdos609.MonochromaticHasOddCycleLe

MonolithicSpace class

A topological space is monolithic (see [Ar1987]; [Ar2013] uses the term without defining it) if every subspace has network weight at most its density. · Homogeneous.MonolithicSpace

monotonicSubsequenceSums def

The set of sums $\sum x_{i_r}$, where $x_{i_1},\ldots,x_{i_r}$ ranges over the monotonic subsequences of the sequence $x_1,\ldots,x_n$. · Erdos1026.monotonicSubsequenceSums

morphism def

The morphism σ on {a, b} defined by a ↦ aab, b ↦ b, represented on Bool where false = a and true = b. · OeisA6697.morphism

Move inductive

The elementary Andrews-Curtis moves: inversion or multiplication of relators, interchange of two relators, and conjugation of one relator by an arbitrary word. · AndrewsCurtis.Move

mSeq def

The sequence defined by $m_0 = 2$ and $m_{n+1} = \lceil m_n (1 + 1/\log n) \rceil$. · Bugeaud06.mSeq

muellerSet def

The set of all integers congruent to $3\cdot 2^i\pmod{2^{i+2}}$ for some $i\geq 0$. · Erdos1136.muellerSet

mulRightL def

Right multiplication by X, as a continuous linear map. · AutomorphicForm.LieDerivAux.mulRightL

multibrotSet def

The Multibrot set of power n is the set of all parameters c : ℂ for which 0 does not escape to infinity under repeated application of z ↦ z ^ n + c. · Mandelbrot.multibrotSet

multicolourTriangleRamsey def

$R(3;k)$, the minimal n such that every k-colouring of the edges of K_n contains a monochromatic triangle. · Erdos183.multicolourTriangleRamsey

MultiplesOf def

The set of multiples of a sequence $(a_i)$ is $\{na_i | n \in \mathbb{N}, i\}$. · Erdos26.MultiplesOf

MultiplicativelyIndependent def

Two integers $p, q \ge 2$ are multiplicatively independent if $\log p / \log q$ is irrational, equivalently if $p^m = q^n$ holds only for $m = n = 0$. · Nat.MultiplicativelyIndependent

MultiplicativelyIndependentFamily def

A family of integers is multiplicatively independent if there is no nonzero tuple of integers $(n_i)$ with $\prod_i b_i^{n_i} = 1$; equivalently, the numbers $\log b_i$ are linearly independent over $\mathbb{Q}$, which is the form used … · Nat.MultiplicativelyIndependentFamily

multiplicityGap def

$f(d_1) - f(d_2)$: the gap between the largest and second-largest distance multiplicities. The supremum over $d$ handles both a unique winner and a tie: non-winners contribute $0$ by truncated subtraction, and tied winners also contribute … · Erdos959.multiplicityGap

multiStep def

def multiStep (M : Machine Γ Λ) (config : Cfg Γ Λ) (n : ℕ) : Option (Cfg Γ Λ) · Turing.BusyBeaver.Machine.multiStep

multiZeta def

The multiple zeta value $\zeta(s_1, s_2, \ldots, s_k)$, defined as $$\zeta(s_1, \ldots, s_k) = \sum_{n_1 > n_2 > \cdots > n_k > 0} \frac{1}{n_1^{s_1} n_2^{s_2} \cdots n_k^{s_k}}.$$ The argument is a list of positive natural numbers. The … · ZagierMZV.multiZeta

MutuallyOrthogonal def

A family of latin squares is mutually orthogonal if any two distinct members are orthogonal. · LatinSquare.MutuallyOrthogonal

MvRatFunc abbrev

The field of multivariate rational functions in variables indexed by σ over a commutative ring K, defined as the fraction field of the multivariate polynomial ring MvPolynomial σ K. · MvRatFunc

MyAbbrevSorry abbrev

abbrev MyAbbrevSorry : Nat · MyAbbrevSorry

MycAdj def

Adjacency of the generalised Mycielskian, before SimpleGraph.fromRel packages it as a graph. · Erdos750.MycAdj

MycVerts abbrev

Vertices of the generalised Mycielskian $M_s(G)$: $s$ copies of the vertices of $G$, one per level, and a single apex. · Erdos750.MycVerts

MyDefByAdmit def

def MyDefByAdmit : Nat · MyDefByAdmit

MyDefBySorry def

def MyDefBySorry : Nat · MyDefBySorry

MyDefPattern def

def MyDefPattern : Nat → Nat | 0 => sorry | _ => 1 /-- warning: Placeholder definitions (e.g., `def foo : Type · MyDefPattern

MyDefSorry def

def MyDefSorry : Nat · MyDefSorry

MyNormalType def

def MyNormalType : Type · MyNormalType

MyOpaqueType opaque

opaque MyOpaqueType : Type /-- warning: New axioms (e.g., `axiom foo : ...`) are not allowed. Note: This linter can be disabled with `set_option linter.style.stubs false` -/ #guard_msgs(warning) in · MyOpaqueType

mzvSetOfWeight def

The set of all MZV values of weight $n$. · ZagierMZV.mzvSetOfWeight

mzvSpanOfWeight def

The $\mathbb{Q}$-submodule of $\mathbb{R}$ spanned by all MZVs of weight $n$. · ZagierMZV.mzvSpanOfWeight