16.5. Multivariate polynomials🔗

For polynomials in several variables, use MvPolynomial, parametrised by a type σ of variables and a coefficient ring R:

MvPolynomial σ R : Type (max u_2 u_1)#check (MvPolynomial σ R : Type _)

The variable indexed by an element i of σ is (MvPolynomial.X i : MvPolynomial σ R), and the constant embedding is MvPolynomial.C.

Unlike the univariate case, where R[X] is a scoped notation in the Polynomial namespace, Mathlib does not have notation for MvPolynomial σ R, scoped or otherwise: you write MvPolynomial σ R directly, even though docstrings and mathematical commentary throughout Mathlib often use R[σ] or R[X₁, …, Xₙ] informally. This notation is borrowed from the related types AddMonoidAlgebra and MonoidAlgebra, which do have scoped R[M] notation. When a particular file uses the same multivariate polynomial ring repeatedly, the usual workaround is a local notation. For example, the Witt-vector files use 𝕄 to denote MvPolynomial (Fin 2 × ℕ) ℤ.

The type of variables σ can be chosen freely to fit the situation at hand, and is unconstrained at the level of the definition itself. When "finitely many variables" needs to be stated abstractly, the usual idiom is to keep σ generic and add a Finite or Fintype instance assumption on it as a separate hypothesis, as is done for example in MvPolynomial.ringKrullDim_of_isNoetherianRing. The most common concrete choice in Mathlib is Fin n: this is what is used, for example, to state results about finitely generated algebras in Algebra.FiniteType and Algebra.FinitePresentation. Other choices appear too: Bool is used internally in the construction of the bernsteinPolynomial, and Bool × ℕ shows up in the structure polynomials behind WittVector.

16.5.1. Coefficients, degree and evaluation🔗

The core operations from the univariate setting have multivariate counterparts, with the main difference that a "degree" is now a multidegree, a function σ →₀ ℕ recording the exponent of each variable.

The coefficient of p at multidegree m is MvPolynomial.coeff, which takes a σ →₀ ℕ rather than a single natural number:

example : R := p.coeff m

Two multivariate polynomials are equal if and only if all coefficients agree (see MvPolynomial.ext).

One notion of degree taking values in ℕ is the MvPolynomial.totalDegree. The degree/natDegree distinction from the univariate case has no analogue here.

p.totalDegree : ℕ#check (p.totalDegree : ℕ)

Per-variable degrees are also available via MvPolynomial.degreeOf.

Evaluating a multivariate polynomial requires specifying a value for each variable, given as a function indexed by σ. The three flavours mirror the univariate case:

MvPolynomial.eval: MvPolynomial.eval f p when f : σ → R;
MvPolynomial.eval₂: like eval, but first pushing the coefficients through a ring homomorphism R →+* A;
MvPolynomial.aeval: MvPolynomial.aeval g p when A is an R-algebra and g : σ → A, the algebra homomorphism sending each variable X i to g i.

(MvPolynomial.eval f) p : R#check (MvPolynomial.eval f p : R)
MvPolynomial.aeval g : MvPolynomial σ R →ₐ[R] A#check (MvPolynomial.aeval g : MvPolynomial σ R →ₐ[R] A)