Degrees and variables of polynomials #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file establishes many results about the degree and variable sets of a multivariate polynomial.

The variable set of a polynomial $P \in R[X]$ is a finset containing each $x \in X$ that appears in a monomial in $P$.

The degree set of a polynomial $P \in R[X]$ is a multiset containing, for each $x$ in the variable set, $n$ copies of $x$, where $n$ is the maximum number of copies of $x$ appearing in a monomial of $P$.

Main declarations #

• mv_polynomial.degrees p : the multiset of variables representing the union of the multisets corresponding to each non-zero monomial in p. For example if 7 ≠ 0 in R and p = x²y+7y³ then degrees p = {x, x, y, y, y}

• mv_polynomial.vars p : the finset of variables occurring in p. For example if p = x⁴y+yz then vars p = {x, y, z}

• mv_polynomial.degree_of n p : ℕ : the total degree of p with respect to the variable n. For example if p = x⁴y+yz then degree_of y p = 1.

• mv_polynomial.total_degree p : ℕ : the max of the sizes of the multisets s whose monomials X^s occur in p. For example if p = x⁴y+yz then total_degree p = 5.

Notation #

As in other polynomial files, we typically use the notation:

• σ τ : Type* (indexing the variables)

• R : Type* [comm_semiring R] (the coefficients)

• s : σ →₀ ℕ, a function from σ to ℕ which is zero away from a finite set. This will give rise to a monomial in mv_polynomial σ R which mathematicians might call X^s

• r : R

• i : σ, with corresponding monomial X i, often denoted X_i by mathematicians

• p : mv_polynomial σ R

degrees #

vars #

degree_of #

total_degree #

vars and eval #