doc-next-gen

Mathlib.Algebra.MvPolynomial.Degrees

Module docstring

{"# Degrees of polynomials

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

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

  • MvPolynomial.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}

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

  • MvPolynomial.totalDegree 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 totalDegree p = 5.

Notation

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

  • σ τ : Type* (indexing the variables)

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

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

  • r : R

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

  • p : MvPolynomial σ R

","### degrees ","### degreeOf ","### totalDegree "}

MvPolynomial.degrees definition
(p : MvPolynomial σ R) : Multiset σ
Full source 
/-- The maximal degrees of each variable in a multi-variable polynomial, expressed as a multiset.

(For example, `degrees (x^2 * y + y^3)` would be `{x, x, y, y, y}`.)
-/
def degrees (p : MvPolynomial σ R) : Multiset σ :=
  letI := Classical.decEq σ
  p.support.sup fun s : σ →₀ ℕ => toMultiset s
Multiset of maximal variable degrees in a multivariate polynomial
Informal description
The function `degrees` maps a multivariate polynomial $p \in R[\sigma]$ to a multiset of variables, where each variable appears with multiplicity equal to its highest exponent in any monomial of $p$. For example, if $p = x^2y + y^3$ (with $7 \neq 0$ in $R$), then $\text{degrees}(p) = \{x, x, y, y, y\}$.
MvPolynomial.degrees_def theorem
[DecidableEq σ] (p : MvPolynomial σ R) : p.degrees = p.support.sup fun s : σ →₀ ℕ => Finsupp.toMultiset s
Full source 
theorem degrees_def [DecidableEq σ] (p : MvPolynomial σ R) :
    p.degrees = p.support.sup fun s : σ →₀ ℕ => Finsupp.toMultiset s := by rw [degrees]; convert rfl
Characterization of Polynomial Degrees via Support Supremum
Informal description
For a multivariate polynomial $p \in R[\sigma]$ with decidable equality on the variables $\sigma$, the multiset of maximal variable degrees $\text{degrees}(p)$ is equal to the supremum (join) over the support of $p$ of the multiset representations of its monomial exponents. More precisely, if we write $p = \sum_{s} a_s X^s$ where $s : \sigma \to_{\text{f}} \mathbb{N}$ are finitely supported exponent functions, then: $$\text{degrees}(p) = \sup_{s \in \text{support}(p)} \text{toMultiset}(s)$$ where $\text{toMultiset}(s)$ converts the exponent function $s$ into a multiset of variables (e.g., $s = (x \mapsto 2, y \mapsto 1)$ becomes $\{x,x,y\}$).
MvPolynomial.degrees_monomial theorem
(s : σ →₀ ℕ) (a : R) : degrees (monomial s a) ≤ toMultiset s
Full source 
theorem degrees_monomial (s : σ →₀ ℕ) (a : R) : degrees (monomial s a) ≤ toMultiset s := by
  classical
    refine (supDegree_single s a).trans_le ?_
    split_ifs
    exacts [bot_le, le_rfl]
Degree Bound for Monomial in Multivariate Polynomial
Informal description
For any finitely supported function $s : \sigma \to_{\text{f}} \mathbb{N}$ and any coefficient $a \in R$, the multiset of maximal variable degrees of the monomial $s$ with coefficient $a$ is bounded above by the multiset representation of $s$. In other words, $\text{degrees}(\text{monomial}(s, a)) \leq \text{toMultiset}(s)$.
MvPolynomial.degrees_monomial_eq theorem
(s : σ →₀ ℕ) (a : R) (ha : a ≠ 0) : degrees (monomial s a) = toMultiset s
Full source 
theorem degrees_monomial_eq (s : σ →₀ ℕ) (a : R) (ha : a ≠ 0) :
    degrees (monomial s a) = toMultiset s := by
  classical
    exact (supDegree_single s a).trans (if_neg ha)
Degrees of Monomial Equal Multiset Representation for Nonzero Coefficients
Informal description
For any finitely supported function $s : \sigma \to_{\text{f}} \mathbb{N}$ and any nonzero coefficient $a \in R$ (where $a \neq 0$), the degrees multiset of the monomial $\text{monomial}(s, a)$ in the multivariate polynomial ring $R[\sigma]$ is equal to the multiset representation of $s$, i.e., \[ \text{degrees}(\text{monomial}(s, a)) = \text{toMultiset}(s). \]
MvPolynomial.degrees_C theorem
(a : R) : degrees (C a : MvPolynomial σ R) = 0
Full source 
theorem degrees_C (a : R) : degrees (C a : MvPolynomial σ R) = 0 :=
  Multiset.le_zero.1 <| degrees_monomial _ _
Degrees of Constant Polynomial is Zero Multiset
Informal description
For any coefficient $a \in R$, the degrees multiset of the constant polynomial $C(a)$ in the multivariate polynomial ring $R[\sigma]$ is the empty multiset, i.e., $\text{degrees}(C(a)) = 0$.
MvPolynomial.degrees_X' theorem
(n : σ) : degrees (X n : MvPolynomial σ R) ≤ { n }
Full source 
theorem degrees_X' (n : σ) : degrees (X n : MvPolynomial σ R) ≤ {n} :=
  le_trans (degrees_monomial _ _) <| le_of_eq <| toMultiset_single _ _
Degree Bound for Monomial $X_n$: $\text{degrees}(X_n) \leq \{n\}$
Informal description
For any variable $n$ in the index set $\sigma$, the multiset of maximal variable degrees of the monomial $X_n$ in the multivariate polynomial ring $R[\sigma]$ is bounded above by the singleton multiset $\{n\}$. In other words, $\text{degrees}(X_n) \leq \{n\}$.
MvPolynomial.degrees_X theorem
[Nontrivial R] (n : σ) : degrees (X n : MvPolynomial σ R) = { n }
Full source 
@[simp]
theorem degrees_X [Nontrivial R] (n : σ) : degrees (X n : MvPolynomial σ R) = {n} :=
  (degrees_monomial_eq _ (1 : R) one_ne_zero).trans (toMultiset_single _ _)
Degrees of Variable Monomial: $\text{degrees}(X_n) = \{n\}$
Informal description
For a nontrivial commutative semiring $R$ and a variable $n \in \sigma$, the degrees multiset of the monomial $X_n$ in the multivariate polynomial ring $R[\sigma]$ is the singleton multiset $\{n\}$. That is, \[ \text{degrees}(X_n) = \{n\}. \]
MvPolynomial.degrees_zero theorem
: degrees (0 : MvPolynomial σ R) = 0
Full source 
@[simp]
theorem degrees_zero : degrees (0 : MvPolynomial σ R) = 0 := by
  rw [← C_0]
  exact degrees_C 0
Degrees of Zero Polynomial is Zero Multiset
Informal description
The degrees multiset of the zero polynomial in the multivariate polynomial ring $R[\sigma]$ is the empty multiset, i.e., $\text{degrees}(0) = 0$.
MvPolynomial.degrees_one theorem
: degrees (1 : MvPolynomial σ R) = 0
Full source 
@[simp]
theorem degrees_one : degrees (1 : MvPolynomial σ R) = 0 :=
  degrees_C 1
Degrees of the Constant One Polynomial is Zero Multiset
Informal description
The degrees multiset of the constant polynomial $1$ in the multivariate polynomial ring $R[\sigma]$ is the empty multiset, i.e., $\text{degrees}(1) = 0$.
MvPolynomial.degrees_add_le theorem
[DecidableEq σ] {p q : MvPolynomial σ R} : (p + q).degrees ≤ p.degrees ⊔ q.degrees
Full source 
theorem degrees_add_le [DecidableEq σ] {p q : MvPolynomial σ R} :
    (p + q).degrees ≤ p.degrees ⊔ q.degrees := by
  simp_rw [degrees_def]; exact supDegree_add_le
Subadditivity of Polynomial Degrees under Addition
Informal description
Let $\sigma$ be a type with decidable equality, and let $R$ be a commutative semiring. For any two multivariate polynomials $p, q \in R[\sigma]$, the multiset of maximal variable degrees of their sum satisfies: $$\text{degrees}(p + q) \leq \text{degrees}(p) \sqcup \text{degrees}(q)$$ where $\sqcup$ denotes the join (supremum) in the lattice of multisets over $\sigma$.
MvPolynomial.degrees_sum_le theorem
{ι : Type*} [DecidableEq σ] (s : Finset ι) (f : ι → MvPolynomial σ R) : (∑ i ∈ s, f i).degrees ≤ s.sup fun i => (f i).degrees
Full source 
theorem degrees_sum_le {ι : Type*} [DecidableEq σ] (s : Finset ι) (f : ι → MvPolynomial σ R) :
    (∑ i ∈ s, f i).degrees ≤ s.sup fun i => (f i).degrees := by
  simp_rw [degrees_def]; exact supDegree_sum_le
Subadditivity of Degrees for Sum of Multivariate Polynomials
Informal description
Let $\sigma$ be a type with decidable equality, $R$ be a commutative semiring, and $s$ be a finite set of indices. For any family of multivariate polynomials $(f_i)_{i \in s}$ in $R[\sigma]$, the multiset of maximal variable degrees of their sum satisfies: \[ \text{degrees}\left(\sum_{i \in s} f_i\right) \leq \sup_{i \in s} \text{degrees}(f_i) \] where $\text{degrees}(f_i)$ denotes the multiset of maximal exponents for each variable in $f_i$, and $\sup$ is the join operation in the lattice of multisets over $\sigma$.
MvPolynomial.degrees_mul_le theorem
{p q : MvPolynomial σ R} : (p * q).degrees ≤ p.degrees + q.degrees
Full source 
theorem degrees_mul_le {p q : MvPolynomial σ R} : (p * q).degrees ≤ p.degrees + q.degrees := by
  classical
  simp_rw [degrees_def]
  exact supDegree_mul_le (map_add _)
Degree Multiset Subadditivity under Polynomial Multiplication
Informal description
For any two multivariate polynomials $p$ and $q$ in $R[\sigma]$, the multiset of maximal variable degrees of their product $p \cdot q$ is componentwise bounded above by the sum of the multisets of maximal variable degrees of $p$ and $q$. In other words: \[ \text{degrees}(p \cdot q) \leq \text{degrees}(p) + \text{degrees}(q) \] where $\text{degrees}(p)$ denotes the multiset where each variable appears with multiplicity equal to its highest exponent in any monomial of $p$.
MvPolynomial.degrees_prod_le theorem
{ι : Type*} {s : Finset ι} {f : ι → MvPolynomial σ R} : (∏ i ∈ s, f i).degrees ≤ ∑ i ∈ s, (f i).degrees
Full source 
theorem degrees_prod_le {ι : Type*} {s : Finset ι} {f : ι → MvPolynomial σ R} :
    (∏ i ∈ s, f i).degrees ≤ ∑ i ∈ s, (f i).degrees := by
  classical exact supDegree_prod_le (map_zero _) (map_add _)
Degree Multiset Bound for Product of Multivariate Polynomials
Informal description
For any finite set $s$ of indices and any family of multivariate polynomials $f_i \in R[\sigma]$ indexed by $i \in s$, the multiset of maximal variable degrees of the product $\prod_{i \in s} f_i$ is componentwise bounded above by the sum of the multisets of maximal variable degrees of each $f_i$. In other words, we have: \[ \text{degrees}\left(\prod_{i \in s} f_i\right) \leq \sum_{i \in s} \text{degrees}(f_i) \] where $\text{degrees}(p)$ denotes the multiset of maximal exponents for each variable in polynomial $p$.
MvPolynomial.degrees_pow_le theorem
{p : MvPolynomial σ R} {n : ℕ} : (p ^ n).degrees ≤ n • p.degrees
Full source 
theorem degrees_pow_le {p : MvPolynomial σ R} {n : ℕ} : (p ^ n).degrees ≤ n • p.degrees := by
  simpa using degrees_prod_le (s := .range n) (f := fun _ ↦ p)
Degree Multiset Bound for Powers of Multivariate Polynomials: $\text{degrees}(p^n) \leq n \cdot \text{degrees}(p)$
Informal description
For any multivariate polynomial $p \in R[\sigma]$ and any natural number $n$, the multiset of maximal variable degrees of $p^n$ is componentwise bounded above by $n$ times the multiset of maximal variable degrees of $p$. In other words: \[ \text{degrees}(p^n) \leq n \cdot \text{degrees}(p) \] where $\text{degrees}(p)$ denotes the multiset where each variable appears with multiplicity equal to its highest exponent in any monomial of $p$.
MvPolynomial.mem_degrees theorem
{p : MvPolynomial σ R} {i : σ} : i ∈ p.degrees ↔ ∃ d, p.coeff d ≠ 0 ∧ i ∈ d.support
Full source 
theorem mem_degrees {p : MvPolynomial σ R} {i : σ} :
    i ∈ p.degreesi ∈ p.degrees ↔ ∃ d, p.coeff d ≠ 0 ∧ i ∈ d.support := by
  classical
  simp only [degrees_def, Multiset.mem_sup, ← mem_support_iff, Finsupp.mem_toMultiset, exists_prop]
Characterization of Variable Membership in Polynomial Degree Multiset
Informal description
For a multivariate polynomial $p \in R[\sigma]$ and a variable $i \in \sigma$, the variable $i$ appears in the multiset of maximal degrees $\text{degrees}(p)$ if and only if there exists a monomial $X^d$ in $p$ with nonzero coefficient such that $i$ appears in the support of $d$ (i.e., the exponent of $i$ in $d$ is nonzero).
MvPolynomial.le_degrees_add_left theorem
(h : Disjoint p.degrees q.degrees) : p.degrees ≤ (p + q).degrees
Full source 
theorem le_degrees_add_left (h : Disjoint p.degrees q.degrees) : p.degrees ≤ (p + q).degrees := by
  classical
  apply Finset.sup_le
  intro d hd
  rw [Multiset.disjoint_iff_ne] at h
  obtain rfl | h0 := eq_or_ne d 0
  · rw [toMultiset_zero]; apply Multiset.zero_le
  · refine Finset.le_sup_of_le (b := d) ?_ le_rfl
    rw [mem_support_iff, coeff_add]
    suffices q.coeff d = 0 by rwa [this, add_zero, coeff, ← Finsupp.mem_support_iff]
    rw [Ne, ← Finsupp.support_eq_empty, ← Ne, ← Finset.nonempty_iff_ne_empty] at h0
    obtain ⟨j, hj⟩ := h0
    contrapose! h
    rw [mem_support_iff] at hd
    refine ⟨j, ?_, j, ?_, rfl⟩
    all_goals rw [mem_degrees]; refine ⟨d, ?_, hj⟩; assumption
Degree Multiset Monotonicity Under Addition with Disjoint Degrees
Informal description
Let $p$ and $q$ be multivariate polynomials in $R[\sigma]$ such that their degree multisets are disjoint. Then the degree multiset of $p$ is componentwise less than or equal to the degree multiset of $p + q$. In other words: \[ \text{degrees}(p) \leq \text{degrees}(p + q) \] where $\text{degrees}(p)$ denotes the multiset where each variable appears with multiplicity equal to its highest exponent in any monomial of $p$.
MvPolynomial.le_degrees_add_right theorem
(h : Disjoint p.degrees q.degrees) : q.degrees ≤ (p + q).degrees
Full source 
lemma le_degrees_add_right (h : Disjoint p.degrees q.degrees) : q.degrees ≤ (p + q).degrees := by
  simpa [add_comm] using le_degrees_add_left h.symm
Degree Multiset Monotonicity Under Addition with Disjoint Degrees (Right Version)
Informal description
Let $p$ and $q$ be multivariate polynomials in $R[\sigma]$ such that their degree multisets are disjoint. Then the degree multiset of $q$ is componentwise less than or equal to the degree multiset of $p + q$. In other words: \[ \text{degrees}(q) \leq \text{degrees}(p + q) \] where $\text{degrees}(q)$ denotes the multiset where each variable appears with multiplicity equal to its highest exponent in any monomial of $q$.
MvPolynomial.degrees_add_of_disjoint theorem
[DecidableEq σ] (h : Disjoint p.degrees q.degrees) : (p + q).degrees = p.degrees ∪ q.degrees
Full source 
theorem degrees_add_of_disjoint [DecidableEq σ] (h : Disjoint p.degrees q.degrees) :
    (p + q).degrees = p.degrees ∪ q.degrees :=
  degrees_add_le.antisymm <| Multiset.union_le (le_degrees_add_left h) (le_degrees_add_right h)
Additivity of Degree Multisets for Disjoint Polynomials
Informal description
Let $\sigma$ be a type with decidable equality, and let $R$ be a commutative semiring. For any two multivariate polynomials $p, q \in R[\sigma]$ with disjoint degree multisets (i.e., $\text{degrees}(p) \cap \text{degrees}(q) = \emptyset$), the degree multiset of their sum is the union of their individual degree multisets: $$\text{degrees}(p + q) = \text{degrees}(p) \cup \text{degrees}(q).$$ Here, $\text{degrees}(p)$ denotes the multiset where each variable appears with multiplicity equal to its highest exponent in any monomial of $p$.
MvPolynomial.degrees_map_le theorem
[CommSemiring S] {f : R →+* S} : (map f p).degrees ≤ p.degrees
Full source 
lemma degrees_map_le [CommSemiring S] {f : R →+* S} : (map f p).degrees ≤ p.degrees := by
  classical exact Finset.sup_mono <| support_map_subset ..
Degree Multiset Non-Increasing Under Polynomial Map
Informal description
Let $R$ and $S$ be commutative semirings, and let $f: R \to S$ be a ring homomorphism. For any multivariate polynomial $p \in R[\sigma]$, the degree multiset of the polynomial $\text{map}\, f\, p \in S[\sigma]$ is a submultiset of the degree multiset of $p$. Here, the degree multiset of a polynomial records, for each variable $\sigma$, its maximal exponent appearing in any monomial of the polynomial.
MvPolynomial.degrees_rename theorem
(f : σ → τ) (φ : MvPolynomial σ R) : (rename f φ).degrees ⊆ φ.degrees.map f
Full source 
theorem degrees_rename (f : σ → τ) (φ : MvPolynomial σ R) :
    (rename f φ).degrees ⊆ φ.degrees.map f := by
  classical
  intro i
  rw [mem_degrees, Multiset.mem_map]
  rintro ⟨d, hd, hi⟩
  obtain ⟨x, rfl, hx⟩ := coeff_rename_ne_zero _ _ _ hd
  simp only [Finsupp.mapDomain, Finsupp.mem_support_iff] at hi
  rw [sum_apply, Finsupp.sum] at hi
  contrapose! hi
  rw [Finset.sum_eq_zero]
  intro j hj
  simp only [exists_prop, mem_degrees] at hi
  specialize hi j ⟨x, hx, hj⟩
  rw [Finsupp.single_apply, if_neg hi]
Degree Multiset Subset Property under Variable Renaming
Informal description
Let $f : \sigma \to \tau$ be a function between index types, and let $\varphi \in R[\sigma]$ be a multivariate polynomial. Then the degree multiset of the renamed polynomial $\text{rename}\, f\, \varphi \in R[\tau]$ is a submultiset of the image of the degree multiset of $\varphi$ under $f$. Here, the degree multiset of a polynomial records, for each variable, its maximal exponent appearing in any monomial of the polynomial.
MvPolynomial.degrees_map_of_injective theorem
[CommSemiring S] (p : MvPolynomial σ R) {f : R →+* S} (hf : Injective f) : (map f p).degrees = p.degrees
Full source 
theorem degrees_map_of_injective [CommSemiring S] (p : MvPolynomial σ R) {f : R →+* S}
    (hf : Injective f) : (map f p).degrees = p.degrees := by
  simp only [degrees, MvPolynomial.support_map_of_injective _ hf]
Preservation of Degree Multiset under Injective Polynomial Map
Informal description
Let $R$ and $S$ be commutative semirings, and let $f: R \to S$ be an injective ring homomorphism. For any multivariate polynomial $p \in R[\sigma]$, the degree multiset of the polynomial $\text{map}\, f\, p \in S[\sigma]$ is equal to the degree multiset of $p$. Here, the degree multiset of a polynomial records, for each variable, its maximal exponent appearing in any monomial of the polynomial.
MvPolynomial.degrees_rename_of_injective theorem
{p : MvPolynomial σ R} {f : σ → τ} (h : Function.Injective f) : degrees (rename f p) = (degrees p).map f
Full source 
theorem degrees_rename_of_injective {p : MvPolynomial σ R} {f : σ → τ} (h : Function.Injective f) :
    degrees (rename f p) = (degrees p).map f := by
  classical
  simp only [degrees, Multiset.map_finset_sup p.support Finsupp.toMultiset f h,
    support_rename_of_injective h, Finset.sup_image]
  refine Finset.sup_congr rfl fun x _ => ?_
  exact (Finsupp.toMultiset_map _ _).symm
Degree Multiset Preservation under Injective Variable Renaming
Informal description
Let $p \in R[\sigma]$ be a multivariate polynomial and $f : \sigma \to \tau$ be an injective function. Then the degree multiset of the polynomial $\text{rename}\, f\, p \in R[\tau]$ is equal to the image of the degree multiset of $p$ under $f$. That is, \[ \text{degrees}(\text{rename}\, f\, p) = \text{map}\, f\, (\text{degrees}(p)). \]
MvPolynomial.degreeOf definition
(n : σ) (p : MvPolynomial σ R) : ℕ
Full source 
/-- `degreeOf n p` gives the highest power of X_n that appears in `p` -/
def degreeOf (n : σ) (p : MvPolynomial σ R) : ℕ :=
  letI := Classical.decEq σ
  p.degrees.count n
Degree of a variable in a multivariate polynomial
Informal description
For a multivariate polynomial $p \in R[\sigma]$ and a variable $n \in \sigma$, the function $\text{degreeOf}$ returns the highest exponent of the variable $n$ appearing in any monomial of $p$. More formally, $\text{degreeOf}\, n\, p$ is equal to the multiplicity of $n$ in the multiset $\text{degrees}\, p$, where $\text{degrees}\, p$ contains each variable with multiplicity equal to its maximal exponent in $p$.
MvPolynomial.degreeOf_def theorem
[DecidableEq σ] (n : σ) (p : MvPolynomial σ R) : p.degreeOf n = p.degrees.count n
Full source 
theorem degreeOf_def [DecidableEq σ] (n : σ) (p : MvPolynomial σ R) :
    p.degreeOf n = p.degrees.count n := by rw [degreeOf]; convert rfl
Degree of Variable Equals Multiplicity in Degrees Multiset
Informal description
For a multivariate polynomial $p \in R[\sigma]$ and a variable $n \in \sigma$, the degree of $n$ in $p$ is equal to the multiplicity of $n$ in the multiset $\text{degrees}(p)$, where $\text{degrees}(p)$ records the maximal exponents of each variable in $p$'s monomials. That is, \[ \text{degreeOf}(n, p) = \text{count}(n, \text{degrees}(p)). \]
MvPolynomial.degreeOf_eq_sup theorem
(n : σ) (f : MvPolynomial σ R) : degreeOf n f = f.support.sup fun m => m n
Full source 
theorem degreeOf_eq_sup (n : σ) (f : MvPolynomial σ R) :
    degreeOf n f = f.support.sup fun m => m n := by
  classical
  rw [degreeOf_def, degrees, Multiset.count_finset_sup]
  congr
  ext
  simp only [count_toMultiset]
Degree of Variable as Supremum of Exponents in Support
Informal description
For a multivariate polynomial $f \in R[\sigma]$ and a variable $n \in \sigma$, the degree of $n$ in $f$ is equal to the supremum of the exponents of $n$ across all monomials in the support of $f$. That is, \[ \text{degreeOf}(n, f) = \sup_{m \in \text{supp}(f)} m(n). \]
MvPolynomial.degreeOf_lt_iff theorem
{n : σ} {f : MvPolynomial σ R} {d : ℕ} (h : 0 < d) : degreeOf n f < d ↔ ∀ m : σ →₀ ℕ, m ∈ f.support → m n < d
Full source 
theorem degreeOf_lt_iff {n : σ} {f : MvPolynomial σ R} {d : ℕ} (h : 0 < d) :
    degreeOfdegreeOf n f < d ↔ ∀ m : σ →₀ ℕ, m ∈ f.support → m n < d := by
  rwa [degreeOf_eq_sup, Finset.sup_lt_iff]
Degree of Variable Strictly Less Than Criterion: $\text{degreeOf}(n, f) < d \leftrightarrow \forall m \in \text{supp}(f), m(n) < d$
Informal description
For a multivariate polynomial $f \in R[\sigma]$, a variable $n \in \sigma$, and a natural number $d > 0$, the degree of $n$ in $f$ is strictly less than $d$ if and only if for every monomial $m$ in the support of $f$, the exponent of $n$ in $m$ is strictly less than $d$. That is, \[ \text{degreeOf}(n, f) < d \leftrightarrow \forall m \in \text{supp}(f), m(n) < d. \]
MvPolynomial.degreeOf_le_iff theorem
{n : σ} {f : MvPolynomial σ R} {d : ℕ} : degreeOf n f ≤ d ↔ ∀ m ∈ support f, m n ≤ d
Full source 
lemma degreeOf_le_iff {n : σ} {f : MvPolynomial σ R} {d : ℕ} :
    degreeOfdegreeOf n f ≤ d ↔ ∀ m ∈ support f, m n ≤ d := by
  rw [degreeOf_eq_sup, Finset.sup_le_iff]
Characterization of Variable Degree Bound in Multivariate Polynomial: $\text{degreeOf}(n, f) \leq d \leftrightarrow \forall m \in \text{supp}(f), m(n) \leq d$
Informal description
For a multivariate polynomial $f \in R[\sigma]$, a variable $n \in \sigma$, and a natural number $d$, the degree of $n$ in $f$ is at most $d$ if and only if for every monomial $m$ in the support of $f$, the exponent of $n$ in $m$ is at most $d$. That is, \[ \text{degreeOf}(n, f) \leq d \leftrightarrow \forall m \in \text{supp}(f), m(n) \leq d. \]
MvPolynomial.degreeOf_zero theorem
(n : σ) : degreeOf n (0 : MvPolynomial σ R) = 0
Full source 
@[simp]
theorem degreeOf_zero (n : σ) : degreeOf n (0 : MvPolynomial σ R) = 0 := by
  classical simp only [degreeOf_def, degrees_zero, Multiset.count_zero]
Degree of Variable in Zero Polynomial is Zero
Informal description
For any variable $n \in \sigma$, the degree of $n$ in the zero polynomial $0 \in R[\sigma]$ is zero, i.e., $\text{degreeOf}(n, 0) = 0$.
MvPolynomial.degreeOf_C theorem
(a : R) (x : σ) : degreeOf x (C a : MvPolynomial σ R) = 0
Full source 
@[simp]
theorem degreeOf_C (a : R) (x : σ) : degreeOf x (C a : MvPolynomial σ R) = 0 := by
  classical simp [degreeOf_def, degrees_C]
Degree of Variable in Constant Polynomial is Zero: $\text{degreeOf}(x, C(a)) = 0$
Informal description
For any coefficient $a \in R$ and any variable $x \in \sigma$, the degree of $x$ in the constant polynomial $C(a) \in R[\sigma]$ is zero, i.e., $\text{degreeOf}(x, C(a)) = 0$.
MvPolynomial.degreeOf_X theorem
[DecidableEq σ] (i j : σ) [Nontrivial R] : degreeOf i (X j : MvPolynomial σ R) = if i = j then 1 else 0
Full source 
theorem degreeOf_X [DecidableEq σ] (i j : σ) [Nontrivial R] :
    degreeOf i (X j : MvPolynomial σ R) = if i = j then 1 else 0 := by
  classical
  by_cases c : i = j
  · simp only [c, if_true, eq_self_iff_true, degreeOf_def, degrees_X, Multiset.count_singleton]
  simp [c, if_false, degreeOf_def, degrees_X]
Degree of Variable in Monomial: $\text{degreeOf}(i, X_j) = \mathbb{1}_{i = j}$
Informal description
For a nontrivial commutative semiring $R$ and variables $i, j \in \sigma$, the degree of the variable $i$ in the monomial $X_j$ is $1$ if $i = j$ and $0$ otherwise. That is, \[ \text{degreeOf}(i, X_j) = \begin{cases} 1 & \text{if } i = j \\ 0 & \text{otherwise} \end{cases} \]
MvPolynomial.degreeOf_add_le theorem
(n : σ) (f g : MvPolynomial σ R) : degreeOf n (f + g) ≤ max (degreeOf n f) (degreeOf n g)
Full source 
theorem degreeOf_add_le (n : σ) (f g : MvPolynomial σ R) :
    degreeOf n (f + g) ≤ max (degreeOf n f) (degreeOf n g) := by
  simp_rw [degreeOf_eq_sup]; exact supDegree_add_le
Degree of Variable in Sum is Bounded by Maximum Degree
Informal description
For any variable $n \in \sigma$ and any two multivariate polynomials $f, g \in R[\sigma]$, the degree of $n$ in the sum $f + g$ is at most the maximum of the degrees of $n$ in $f$ and $g$ individually. That is, \[ \text{degreeOf}(n, f + g) \leq \max(\text{degreeOf}(n, f), \text{degreeOf}(n, g)). \]
MvPolynomial.monomial_le_degreeOf theorem
(i : σ) {f : MvPolynomial σ R} {m : σ →₀ ℕ} (h_m : m ∈ f.support) : m i ≤ degreeOf i f
Full source 
theorem monomial_le_degreeOf (i : σ) {f : MvPolynomial σ R} {m : σ →₀ ℕ} (h_m : m ∈ f.support) :
    m i ≤ degreeOf i f := by
  rw [degreeOf_eq_sup i]
  apply Finset.le_sup h_m
Exponent in Monomial Bounded by Variable Degree: $m(i) \leq \text{degreeOf}(i, f)$
Informal description
For any multivariate polynomial $f \in R[\sigma]$, any variable $i \in \sigma$, and any monomial $m$ in the support of $f$, the exponent of $i$ in $m$ is at most the degree of $i$ in $f$. That is, \[ m(i) \leq \text{degreeOf}(i, f). \]
MvPolynomial.degreeOf_monomial_eq theorem
(s : σ →₀ ℕ) (i : σ) {a : R} (ha : a ≠ 0) : (monomial s a).degreeOf i = s i
Full source 
lemma degreeOf_monomial_eq (s : σ →₀ ℕ) (i : σ) {a : R} (ha : a ≠ 0) :
    (monomial s a).degreeOf i = s i := by
  classical rw [degreeOf_def, degrees_monomial_eq _ _ ha, Finsupp.count_toMultiset]
Degree of Variable in Monomial Equals Exponent
Informal description
For any finitely supported function $s \colon \sigma \to \mathbb{N}$, any variable $i \in \sigma$, and any nonzero coefficient $a \in R$, the degree of the variable $i$ in the monomial $\text{monomial}(s, a)$ is equal to $s(i)$. That is, \[ \text{degreeOf}(i, \text{monomial}(s, a)) = s(i). \]
MvPolynomial.degreeOf_mul_le theorem
(i : σ) (f g : MvPolynomial σ R) : degreeOf i (f * g) ≤ degreeOf i f + degreeOf i g
Full source 
theorem degreeOf_mul_le (i : σ) (f g : MvPolynomial σ R) :
    degreeOf i (f * g) ≤ degreeOf i f + degreeOf i g := by
  classical
  simp only [degreeOf]
  convert Multiset.count_le_of_le i degrees_mul_le
  rw [Multiset.count_add]
Subadditivity of variable degree under polynomial multiplication: $\text{degreeOf}_i(f \cdot g) \leq \text{degreeOf}_i(f) + \text{degreeOf}_i(g)$
Informal description
For any variable $i$ in $\sigma$ and any multivariate polynomials $f$ and $g$ in $R[\sigma]$, the degree of $i$ in the product $f \cdot g$ is at most the sum of the degrees of $i$ in $f$ and $g$. In other words: \[ \text{degreeOf}_i(f \cdot g) \leq \text{degreeOf}_i(f) + \text{degreeOf}_i(g) \]
MvPolynomial.degreeOf_sum_le theorem
{ι : Type*} (i : σ) (s : Finset ι) (f : ι → MvPolynomial σ R) : degreeOf i (∑ j ∈ s, f j) ≤ s.sup fun j => degreeOf i (f j)
Full source 
theorem degreeOf_sum_le {ι : Type*} (i : σ) (s : Finset ι) (f : ι → MvPolynomial σ R) :
    degreeOf i (∑ j ∈ s, f j) ≤ s.sup fun j => degreeOf i (f j) := by
  simp_rw [degreeOf_eq_sup]
  exact supDegree_sum_le
Degree of Variable in Sum of Polynomials is Bounded by Supremum of Degrees
Informal description
For any finite set $s$ of type $\iota$, any variable $i \in \sigma$, and any family of multivariate polynomials $f \colon \iota \to R[\sigma]$, the degree of $i$ in the sum $\sum_{j \in s} f(j)$ is at most the supremum of the degrees of $i$ in each $f(j)$ for $j \in s$. That is, \[ \text{degreeOf}_i\left(\sum_{j \in s} f(j)\right) \leq \sup_{j \in s} \text{degreeOf}_i(f(j)). \]
MvPolynomial.degreeOf_prod_le theorem
{ι : Type*} (i : σ) (s : Finset ι) (f : ι → MvPolynomial σ R) : degreeOf i (∏ j ∈ s, f j) ≤ ∑ j ∈ s, (f j).degreeOf i
Full source 
theorem degreeOf_prod_le {ι : Type*} (i : σ) (s : Finset ι) (f : ι → MvPolynomial σ R) :
    degreeOf i (∏ j ∈ s, f j) ≤ ∑ j ∈ s, (f j).degreeOf i := by
  simp_rw [degreeOf_eq_sup]
  exact supDegree_prod_le (by simp only [coe_zero, Pi.zero_apply])
    (fun _ _ => by simp only [coe_add, Pi.add_apply])
Subadditivity of Variable Degree under Finite Product of Polynomials: $\text{degreeOf}_i(\prod f_j) \leq \sum \text{degreeOf}_i(f_j)$
Informal description
For any variable $i$ in $\sigma$, any finite set $s$ of indices of type $\iota$, and any family of multivariate polynomials $f_j \in R[\sigma]$ indexed by $j \in s$, the degree of $i$ in the product $\prod_{j \in s} f_j$ is at most the sum over $j \in s$ of the degrees of $i$ in each $f_j$. That is, \[ \text{degreeOf}_i\left(\prod_{j \in s} f_j\right) \leq \sum_{j \in s} \text{degreeOf}_i(f_j). \]
MvPolynomial.degreeOf_pow_le theorem
(i : σ) (p : MvPolynomial σ R) (n : ℕ) : degreeOf i (p ^ n) ≤ n * degreeOf i p
Full source 
theorem degreeOf_pow_le (i : σ) (p : MvPolynomial σ R) (n : ℕ) :
    degreeOf i (p ^ n) ≤ n * degreeOf i p := by
  simpa using degreeOf_prod_le i (Finset.range n) (fun _ => p)
Degree Bound for Variable in Power of Polynomial: $\text{degreeOf}_i(p^n) \leq n \cdot \text{degreeOf}_i(p)$
Informal description
For any variable $i$ in $\sigma$, any multivariate polynomial $p \in R[\sigma]$, and any natural number $n$, the degree of $i$ in the polynomial $p^n$ is at most $n$ times the degree of $i$ in $p$. That is, \[ \text{degreeOf}_i(p^n) \leq n \cdot \text{degreeOf}_i(p). \]
MvPolynomial.degreeOf_mul_X_of_ne theorem
{i j : σ} (f : MvPolynomial σ R) (h : i ≠ j) : degreeOf i (f * X j) = degreeOf i f
Full source 
theorem degreeOf_mul_X_of_ne {i j : σ} (f : MvPolynomial σ R) (h : i ≠ j) :
    degreeOf i (f * X j) = degreeOf i f := by
  classical
  simp only [degreeOf_eq_sup i, support_mul_X, Finset.sup_map]
  congr
  ext
  simp only [Finsupp.single, add_eq_left, addRightEmbedding_apply, coe_mk,
    Pi.add_apply, comp_apply, ite_eq_right_iff, Finsupp.coe_add, Pi.single_eq_of_ne h]
Degree Preservation under Multiplication by Distinct Variable: $\text{degreeOf}(i, f \cdot X_j) = \text{degreeOf}(i, f)$ for $i \neq j$
Informal description
For any multivariate polynomial $f \in R[\sigma]$ and distinct variables $i, j \in \sigma$ with $i \neq j$, the degree of $i$ in the product $f \cdot X_j$ is equal to the degree of $i$ in $f$. That is, \[ \text{degreeOf}(i, f \cdot X_j) = \text{degreeOf}(i, f). \]
MvPolynomial.degreeOf_mul_X_self theorem
(j : σ) (f : MvPolynomial σ R) : degreeOf j (f * X j) ≤ degreeOf j f + 1
Full source 
theorem degreeOf_mul_X_self (j : σ) (f : MvPolynomial σ R) :
    degreeOf j (f * X j) ≤ degreeOf j f + 1 := by
  classical
  simp only [degreeOf]
  apply (Multiset.count_le_of_le j degrees_mul_le).trans
  simp only [Multiset.count_add, add_le_add_iff_left]
  convert Multiset.count_le_of_le j <| degrees_X' j
  rw [Multiset.count_singleton_self]
Degree Bound for Multiplication by $X_j$: $\text{degreeOf}_j (f \cdot X_j) \leq \text{degreeOf}_j f + 1$
Informal description
For any multivariate polynomial $f \in R[\sigma]$ and any variable $j \in \sigma$, the degree of $j$ in the product $f \cdot X_j$ is at most the degree of $j$ in $f$ plus one, i.e., \[ \text{degreeOf}_j (f \cdot X_j) \leq \text{degreeOf}_j f + 1. \]
MvPolynomial.degreeOf_mul_X_eq_degreeOf_add_one_iff theorem
(j : σ) (f : MvPolynomial σ R) : degreeOf j (f * X j) = degreeOf j f + 1 ↔ f ≠ 0
Full source 
theorem degreeOf_mul_X_eq_degreeOf_add_one_iff (j : σ) (f : MvPolynomial σ R) :
    degreeOfdegreeOf j (f * X j) = degreeOf j f + 1 ↔ f ≠ 0 := by
  refine ⟨fun h => by by_contra ha; simp [ha] at h, fun h => ?_⟩
  apply Nat.le_antisymm (degreeOf_mul_X_self j f)
  have : (f.support.sup fun m ↦ m j) + 1 = (f.support.sup fun m ↦ (m j + 1)) :=
    Finset.comp_sup_eq_sup_comp_of_nonempty @Nat.succ_le_succ (support_nonempty.mpr h)
  simp only [degreeOf_eq_sup, support_mul_X, this]
  apply Finset.sup_le
  intro x hx
  simp only [Finset.sup_map, bot_eq_zero', add_pos_iff, zero_lt_one, or_true, Finset.le_sup_iff]
  use x
  simpa using mem_support_iff.mp hx
Degree Increase Condition for Multiplication by $X_j$: $\text{degreeOf}_j (f \cdot X_j) = \text{degreeOf}_j f + 1 \leftrightarrow f \neq 0$
Informal description
For a multivariate polynomial $f \in R[\sigma]$ and a variable $j \in \sigma$, the degree of $j$ in the product $f \cdot X_j$ equals the degree of $j$ in $f$ plus one if and only if $f$ is not the zero polynomial. That is, \[ \text{degreeOf}_j (f \cdot X_j) = \text{degreeOf}_j f + 1 \leftrightarrow f \neq 0. \]
MvPolynomial.degreeOf_C_mul_le theorem
(p : MvPolynomial σ R) (i : σ) (c : R) : (C c * p).degreeOf i ≤ p.degreeOf i
Full source 
theorem degreeOf_C_mul_le (p : MvPolynomial σ R) (i : σ) (c : R) :
    (C c * p).degreeOf i ≤ p.degreeOf i := by
  unfold degreeOf
  convert Multiset.count_le_of_le i degrees_mul_le
  simp only [degrees_C, zero_add]
Degree Preservation under Scalar Multiplication: $\text{degreeOf}_i (c \cdot p) \leq \text{degreeOf}_i p$
Informal description
For any multivariate polynomial $p \in R[\sigma]$, any variable $i \in \sigma$, and any coefficient $c \in R$, the degree of the variable $i$ in the polynomial $c \cdot p$ is less than or equal to the degree of $i$ in $p$. In other words: \[ \text{degreeOf}_i (c \cdot p) \leq \text{degreeOf}_i p \]
MvPolynomial.degreeOf_mul_C_le theorem
(p : MvPolynomial σ R) (i : σ) (c : R) : (p * C c).degreeOf i ≤ p.degreeOf i
Full source 
theorem degreeOf_mul_C_le (p : MvPolynomial σ R) (i : σ) (c : R) :
    (p * C c).degreeOf i ≤ p.degreeOf i := by
  unfold degreeOf
  convert Multiset.count_le_of_le i degrees_mul_le
  simp only [degrees_C, add_zero]
Degree Preservation under Right Multiplication by Constant Polynomial
Informal description
For any multivariate polynomial $p \in R[\sigma]$, any variable $i \in \sigma$, and any coefficient $c \in R$, the degree of $i$ in the product $p \cdot C(c)$ is less than or equal to the degree of $i$ in $p$. In other words: \[ \text{degreeOf}_i(p \cdot C(c)) \leq \text{degreeOf}_i(p) \] where $C(c)$ denotes the constant polynomial with coefficient $c$.
MvPolynomial.degreeOf_rename_of_injective theorem
{p : MvPolynomial σ R} {f : σ → τ} (h : Function.Injective f) (i : σ) : degreeOf (f i) (rename f p) = degreeOf i p
Full source 
theorem degreeOf_rename_of_injective {p : MvPolynomial σ R} {f : σ → τ} (h : Function.Injective f)
    (i : σ) : degreeOf (f i) (rename f p) = degreeOf i p := by
  classical
  simp only [degreeOf, degrees_rename_of_injective h, Multiset.count_map_eq_count' f p.degrees h]
Degree Preservation under Injective Variable Renaming: $\text{degreeOf}_{f(i)}(\text{rename}\, f\, p) = \text{degreeOf}_i p$
Informal description
Let $p \in R[\sigma]$ be a multivariate polynomial, $f \colon \sigma \to \tau$ an injective function, and $i \in \sigma$ a variable. Then the degree of the variable $f(i)$ in the renamed polynomial $\text{rename}\, f\, p$ equals the degree of $i$ in $p$, i.e., \[ \text{degreeOf}\, (f(i))\, (\text{rename}\, f\, p) = \text{degreeOf}\, i\, p. \]
MvPolynomial.totalDegree definition
(p : MvPolynomial σ R) : ℕ
Full source 
/-- `totalDegree p` gives the maximum |s| over the monomials X^s in `p` -/
def totalDegree (p : MvPolynomial σ R) : ℕ :=
  p.support.sup fun s => s.sum fun _ e => e
Total degree of a multivariate polynomial
Informal description
The total degree of a multivariate polynomial $p \in R[X_1, \dots, X_n]$ is the maximum sum of exponents $\sum_{i=1}^n e_i$ over all monomials $X_1^{e_1} \cdots X_n^{e_n}$ appearing in $p$.
MvPolynomial.totalDegree_eq theorem
(p : MvPolynomial σ R) : p.totalDegree = p.support.sup fun m => Multiset.card (toMultiset m)
Full source 
theorem totalDegree_eq (p : MvPolynomial σ R) :
    p.totalDegree = p.support.sup fun m => Multiset.card (toMultiset m) := by
  rw [totalDegree]
  congr; funext m
  exact (Finsupp.card_toMultiset _).symm
Total Degree Equals Supremum of Monomial Cardinalities
Informal description
For any multivariate polynomial $p \in R[X_1, \dots, X_n]$, the total degree of $p$ is equal to the supremum of the cardinalities of the multisets associated to its monomials, i.e., \[ \text{totalDegree}(p) = \sup_{m \in \text{support}(p)} |\text{toMultiset}(m)|, \] where $\text{toMultiset}(m)$ is the multiset representation of the monomial $m$ (counting variable exponents) and $\text{support}(p)$ is the set of monomials appearing in $p$ with nonzero coefficients.
MvPolynomial.le_totalDegree theorem
{p : MvPolynomial σ R} {s : σ →₀ ℕ} (h : s ∈ p.support) : (s.sum fun _ e => e) ≤ totalDegree p
Full source 
theorem le_totalDegree {p : MvPolynomial σ R} {s : σ →₀ ℕ} (h : s ∈ p.support) :
    (s.sum fun _ e => e) ≤ totalDegree p :=
  Finset.le_sup (α := ℕ) (f := fun s => sum s fun _ e => e) h
Monomial Degree Bounded by Total Degree in Multivariate Polynomials
Informal description
For any multivariate polynomial $p \in R[X_1, \dots, X_n]$ and any monomial $s$ in the support of $p$, the sum of exponents in $s$ is less than or equal to the total degree of $p$. In other words, if $s = \sum_{i=1}^n e_i X_i$ appears in $p$ with a nonzero coefficient, then $\sum_{i=1}^n e_i \leq \text{totalDegree}(p)$.
MvPolynomial.totalDegree_le_degrees_card theorem
(p : MvPolynomial σ R) : p.totalDegree ≤ Multiset.card p.degrees
Full source 
theorem totalDegree_le_degrees_card (p : MvPolynomial σ R) :
    p.totalDegree ≤ Multiset.card p.degrees := by
  classical
  rw [totalDegree_eq]
  exact Finset.sup_le fun s hs => Multiset.card_le_card <| Finset.le_sup hs
Total Degree Bounded by Cardinality of Degrees Multiset
Informal description
For any multivariate polynomial $p \in R[X_1, \dots, X_n]$, the total degree of $p$ is less than or equal to the cardinality of its degrees multiset, i.e., \[ \text{totalDegree}(p) \leq |\text{degrees}(p)|, \] where $\text{degrees}(p)$ is the multiset of variables in $p$ with multiplicities equal to their maximal exponents in any monomial of $p$.
MvPolynomial.totalDegree_le_of_support_subset theorem
(h : p.support ⊆ q.support) : totalDegree p ≤ totalDegree q
Full source 
theorem totalDegree_le_of_support_subset (h : p.support ⊆ q.support) :
    totalDegree p ≤ totalDegree q :=
  Finset.sup_mono h
Total Degree Monotonicity under Support Inclusion
Informal description
For any two multivariate polynomials $p, q \in R[X_1, \dots, X_n]$, if the support of $p$ is a subset of the support of $q$, then the total degree of $p$ is less than or equal to the total degree of $q$.
MvPolynomial.totalDegree_C theorem
(a : R) : (C a : MvPolynomial σ R).totalDegree = 0
Full source 
@[simp]
theorem totalDegree_C (a : R) : (C a : MvPolynomial σ R).totalDegree = 0 :=
  (supDegree_single 0 a).trans <| by rw [sum_zero_index, bot_eq_zero', ite_self]
Total Degree of Constant Polynomial is Zero
Informal description
For any constant polynomial $C(a) \in R[X_1, \dots, X_n]$, where $a \in R$, the total degree is zero, i.e., $\text{totalDegree}(C(a)) = 0$.
MvPolynomial.totalDegree_zero theorem
: (0 : MvPolynomial σ R).totalDegree = 0
Full source 
@[simp]
theorem totalDegree_zero : (0 : MvPolynomial σ R).totalDegree = 0 := by
  rw [← C_0]; exact totalDegree_C (0 : R)
Total Degree of Zero Polynomial is Zero
Informal description
The total degree of the zero polynomial in the multivariate polynomial ring $R[X_1, \dots, X_n]$ is zero, i.e., $\text{totalDegree}(0) = 0$.
MvPolynomial.totalDegree_one theorem
: (1 : MvPolynomial σ R).totalDegree = 0
Full source 
@[simp]
theorem totalDegree_one : (1 : MvPolynomial σ R).totalDegree = 0 :=
  totalDegree_C (1 : R)
Total Degree of the Unit Polynomial is Zero
Informal description
The total degree of the constant polynomial $1$ in the multivariate polynomial ring $R[\sigma]$ is zero, i.e., $\text{totalDegree}(1) = 0$.
MvPolynomial.totalDegree_X theorem
{R} [CommSemiring R] [Nontrivial R] (s : σ) : (X s : MvPolynomial σ R).totalDegree = 1
Full source 
@[simp]
theorem totalDegree_X {R} [CommSemiring R] [Nontrivial R] (s : σ) :
    (X s : MvPolynomial σ R).totalDegree = 1 := by
  rw [totalDegree, support_X]
  simp only [Finset.sup, Finsupp.sum_single_index, Finset.fold_singleton, sup_bot_eq]
Total Degree of Variable Monomial in Multivariate Polynomial Ring is One
Informal description
Let $R$ be a commutative semiring that is nontrivial (i.e., $0 \neq 1$). For any variable $s$ in the index set $\sigma$, the total degree of the monomial $X_s$ in the multivariate polynomial ring $R[\sigma]$ is equal to 1.
MvPolynomial.totalDegree_add theorem
(a b : MvPolynomial σ R) : (a + b).totalDegree ≤ max a.totalDegree b.totalDegree
Full source 
theorem totalDegree_add (a b : MvPolynomial σ R) :
    (a + b).totalDegree ≤ max a.totalDegree b.totalDegree :=
  sup_support_add_le _ _ _
Total Degree Bound for Sum of Multivariate Polynomials: $\text{totalDegree}(a + b) \leq \max(\text{totalDegree}(a), \text{totalDegree}(b))$
Informal description
For any two multivariate polynomials $a$ and $b$ over variables $\sigma$ and coefficients in a commutative semiring $R$, the total degree of their sum satisfies the inequality: \[ \text{totalDegree}(a + b) \leq \max(\text{totalDegree}(a), \text{totalDegree}(b)) \]
MvPolynomial.totalDegree_add_eq_left_of_totalDegree_lt theorem
{p q : MvPolynomial σ R} (h : q.totalDegree < p.totalDegree) : (p + q).totalDegree = p.totalDegree
Full source 
theorem totalDegree_add_eq_left_of_totalDegree_lt {p q : MvPolynomial σ R}
    (h : q.totalDegree < p.totalDegree) : (p + q).totalDegree = p.totalDegree := by
  classical
    apply le_antisymm
    · rw [← max_eq_left_of_lt h]
      exact totalDegree_add p q
    by_cases hp : p = 0
    · simp [hp]
    obtain ⟨b, hb₁, hb₂⟩ :=
      p.support.exists_mem_eq_sup (Finsupp.support_nonempty_iff.mpr hp) fun m : σ →₀ ℕ =>
        Multiset.card (toMultiset m)
    have hb : ¬b ∈ q.support := by
      contrapose! h
      rw [totalDegree_eq p, hb₂, totalDegree_eq]
      apply Finset.le_sup h
    have hbb : b ∈ (p + q).support := by
      apply support_sdiff_support_subset_support_add
      rw [Finset.mem_sdiff]
      exact ⟨hb₁, hb⟩
    rw [totalDegree_eq, hb₂, totalDegree_eq]
    exact Finset.le_sup (f := fun m => Multiset.card (Finsupp.toMultiset m)) hbb
Total Degree Preservation Under Addition When One Polynomial Has Strictly Smaller Degree
Informal description
Let $p$ and $q$ be multivariate polynomials in $R[X_1, \dots, X_n]$. If the total degree of $q$ is strictly less than that of $p$, then the total degree of $p + q$ equals the total degree of $p$, i.e., \[ \text{totalDegree}(p + q) = \text{totalDegree}(p). \]
MvPolynomial.totalDegree_add_eq_right_of_totalDegree_lt theorem
{p q : MvPolynomial σ R} (h : q.totalDegree < p.totalDegree) : (q + p).totalDegree = p.totalDegree
Full source 
theorem totalDegree_add_eq_right_of_totalDegree_lt {p q : MvPolynomial σ R}
    (h : q.totalDegree < p.totalDegree) : (q + p).totalDegree = p.totalDegree := by
  rw [add_comm, totalDegree_add_eq_left_of_totalDegree_lt h]
Total Degree Preservation Under Addition When One Polynomial Has Strictly Smaller Degree (Right Version)
Informal description
Let $p$ and $q$ be multivariate polynomials in $R[X_1, \dots, X_n]$. If the total degree of $q$ is strictly less than that of $p$, then the total degree of $q + p$ equals the total degree of $p$, i.e., \[ \text{totalDegree}(q + p) = \text{totalDegree}(p). \]
MvPolynomial.totalDegree_mul theorem
(a b : MvPolynomial σ R) : (a * b).totalDegree ≤ a.totalDegree + b.totalDegree
Full source 
theorem totalDegree_mul (a b : MvPolynomial σ R) :
    (a * b).totalDegree ≤ a.totalDegree + b.totalDegree :=
  sup_support_mul_le (by exact (Finsupp.sum_add_index' (fun _ => rfl) (fun _ _ _ => rfl)).le) _ _
Total Degree Bound for Product of Multivariate Polynomials: $\text{totalDegree}(a \cdot b) \leq \text{totalDegree}(a) + \text{totalDegree}(b)$
Informal description
For any two multivariate polynomials $a$ and $b$ in $R[X_1, \dots, X_n]$, the total degree of their product satisfies $\text{totalDegree}(a \cdot b) \leq \text{totalDegree}(a) + \text{totalDegree}(b)$.
MvPolynomial.totalDegree_smul_le theorem
[CommSemiring S] [DistribMulAction R S] (a : R) (f : MvPolynomial σ S) : (a • f).totalDegree ≤ f.totalDegree
Full source 
theorem totalDegree_smul_le [CommSemiring S] [DistribMulAction R S] (a : R) (f : MvPolynomial σ S) :
    (a • f).totalDegree ≤ f.totalDegree :=
  Finset.sup_mono support_smul
Total Degree Bound for Scalar Multiplication of Multivariate Polynomials: $\text{totalDegree}(a \cdot f) \leq \text{totalDegree}(f)$
Informal description
Let $R$ and $S$ be commutative semirings with a distributive multiplicative action of $R$ on $S$. For any element $a \in R$ and any multivariate polynomial $f \in S[X_1, \dots, X_n]$, the total degree of the scalar multiple $a \cdot f$ is at most the total degree of $f$, i.e., \[ \text{totalDegree}(a \cdot f) \leq \text{totalDegree}(f). \]
MvPolynomial.totalDegree_pow theorem
(a : MvPolynomial σ R) (n : ℕ) : (a ^ n).totalDegree ≤ n * a.totalDegree
Full source 
theorem totalDegree_pow (a : MvPolynomial σ R) (n : ℕ) :
    (a ^ n).totalDegree ≤ n * a.totalDegree := by
  rw [Finset.pow_eq_prod_const, ← Nat.nsmul_eq_mul, Finset.nsmul_eq_sum_const]
  refine supDegree_prod_le rfl (fun _ _ => ?_)
  exact Finsupp.sum_add_index' (fun _ => rfl) (fun _ _ _ => rfl)
Total Degree Bound for Powers of Multivariate Polynomials: $\text{totalDegree}(a^n) \leq n \cdot \text{totalDegree}(a)$
Informal description
For any multivariate polynomial $a \in R[X_1, \dots, X_n]$ and any natural number $n$, the total degree of $a^n$ is at most $n$ times the total degree of $a$, i.e., \[ \text{totalDegree}(a^n) \leq n \cdot \text{totalDegree}(a). \]
MvPolynomial.totalDegree_monomial theorem
(s : σ →₀ ℕ) {c : R} (hc : c ≠ 0) : (monomial s c : MvPolynomial σ R).totalDegree = s.sum fun _ e => e
Full source 
@[simp]
theorem totalDegree_monomial (s : σ →₀ ℕ) {c : R} (hc : c ≠ 0) :
    (monomial s c : MvPolynomial σ R).totalDegree = s.sum fun _ e => e := by
  classical simp [totalDegree, support_monomial, if_neg hc]
Total Degree of Monomial Equals Sum of Exponents: $\text{totalDegree}(\text{monomial}\, s\, c) = \sum s$
Informal description
For any finitely supported function $s : \sigma \to \mathbb{N}$ and any nonzero coefficient $c \in R$, the total degree of the monomial $\text{monomial}\, s\, c$ in the multivariate polynomial ring $R[X_1, \dots, X_n]$ is equal to the sum of the exponents in $s$, i.e., \[ \text{totalDegree}(\text{monomial}\, s\, c) = \sum_{i \in \sigma} s(i). \]
MvPolynomial.totalDegree_monomial_le theorem
(s : σ →₀ ℕ) (c : R) : (monomial s c).totalDegree ≤ s.sum fun _ ↦ id
Full source 
theorem totalDegree_monomial_le (s : σ →₀ ℕ) (c : R) :
    (monomial s c).totalDegree ≤ s.sum fun _ ↦ id := by
  if hc : c = 0 then
    simp only [hc, map_zero, totalDegree_zero, zero_le]
  else
    rw [totalDegree_monomial _ hc, Function.id_def]
Upper Bound on Total Degree of Monomial: $\text{totalDegree}(\text{monomial}\, s\, c) \leq \sum s$
Informal description
For any finitely supported function $s : \sigma \to \mathbb{N}$ and any coefficient $c \in R$, the total degree of the monomial $\text{monomial}\, s\, c$ in the multivariate polynomial ring $R[X_1, \dots, X_n]$ is at most the sum of the exponents in $s$, i.e., \[ \text{totalDegree}(\text{monomial}\, s\, c) \leq \sum_{i \in \sigma} s(i). \]
MvPolynomial.totalDegree_X_pow theorem
[Nontrivial R] (s : σ) (n : ℕ) : (X s ^ n : MvPolynomial σ R).totalDegree = n
Full source 
@[simp]
theorem totalDegree_X_pow [Nontrivial R] (s : σ) (n : ℕ) :
    (X s ^ n : MvPolynomial σ R).totalDegree = n := by simp [X_pow_eq_monomial, one_ne_zero]
Total Degree of Variable Power: $\text{totalDegree}(X_s^n) = n$
Informal description
Let $R$ be a nontrivial commutative semiring and $\sigma$ a type indexing the variables. For any variable $s \in \sigma$ and natural number $n \in \mathbb{N}$, the total degree of the monomial $(X_s)^n$ in the multivariate polynomial ring $R[\sigma]$ is equal to $n$.
MvPolynomial.totalDegree_list_prod theorem
: ∀ s : List (MvPolynomial σ R), s.prod.totalDegree ≤ (s.map MvPolynomial.totalDegree).sum
Full source 
theorem totalDegree_list_prod :
    ∀ s : List (MvPolynomial σ R), s.prod.totalDegree ≤ (s.map MvPolynomial.totalDegree).sum
  | [] => by rw [List.prod_nil, totalDegree_one, List.map_nil, List.sum_nil]
  | p::ps => by
    rw [List.prod_cons, List.map, List.sum_cons]
    exact le_trans (totalDegree_mul _ _) (add_le_add_left (totalDegree_list_prod ps) _)
Total Degree Bound for Product of List of Multivariate Polynomials: $\text{totalDegree}(\prod p) \leq \sum \text{totalDegree}(p)$
Informal description
For any list $s$ of multivariate polynomials in $R[X_1, \dots, X_n]$, the total degree of their product is at most the sum of the total degrees of the polynomials in the list, i.e., \[ \text{totalDegree}\left(\prod_{p \in s} p\right) \leq \sum_{p \in s} \text{totalDegree}(p). \]
MvPolynomial.totalDegree_multiset_prod theorem
(s : Multiset (MvPolynomial σ R)) : s.prod.totalDegree ≤ (s.map MvPolynomial.totalDegree).sum
Full source 
theorem totalDegree_multiset_prod (s : Multiset (MvPolynomial σ R)) :
    s.prod.totalDegree ≤ (s.map MvPolynomial.totalDegree).sum := by
  refine Quotient.inductionOn s fun l => ?_
  rw [Multiset.quot_mk_to_coe, Multiset.prod_coe, Multiset.map_coe, Multiset.sum_coe]
  exact totalDegree_list_prod l
Total Degree Bound for Multiset Product of Multivariate Polynomials: $\text{totalDegree}(\prod p) \leq \sum \text{totalDegree}(p)$
Informal description
For any multiset $s$ of multivariate polynomials in $R[X_1, \dots, X_n]$, the total degree of their product is at most the sum of the total degrees of the polynomials in the multiset, i.e., \[ \text{totalDegree}\left(\prod_{p \in s} p\right) \leq \sum_{p \in s} \text{totalDegree}(p). \]
MvPolynomial.totalDegree_finset_prod theorem
{ι : Type*} (s : Finset ι) (f : ι → MvPolynomial σ R) : (s.prod f).totalDegree ≤ ∑ i ∈ s, (f i).totalDegree
Full source 
theorem totalDegree_finset_prod {ι : Type*} (s : Finset ι) (f : ι → MvPolynomial σ R) :
    (s.prod f).totalDegree ≤ ∑ i ∈ s, (f i).totalDegree := by
  refine le_trans (totalDegree_multiset_prod _) ?_
  simp only [Multiset.map_map, comp_apply, Finset.sum_map_val, le_refl]
Total Degree Bound for Finite Product of Multivariate Polynomials: $\text{totalDegree}(\prod f_i) \leq \sum \text{totalDegree}(f_i)$
Informal description
For any finite set $s$ of indices and any family of multivariate polynomials $(f_i)_{i \in s}$ over variables $\sigma$ and coefficients in a commutative semiring $R$, the total degree of the product $\prod_{i \in s} f_i$ is bounded by the sum of the total degrees of the individual polynomials: \[ \text{totalDegree}\left(\prod_{i \in s} f_i\right) \leq \sum_{i \in s} \text{totalDegree}(f_i). \]
MvPolynomial.totalDegree_finset_sum theorem
{ι : Type*} (s : Finset ι) (f : ι → MvPolynomial σ R) : (s.sum f).totalDegree ≤ Finset.sup s fun i => (f i).totalDegree
Full source 
theorem totalDegree_finset_sum {ι : Type*} (s : Finset ι) (f : ι → MvPolynomial σ R) :
    (s.sum f).totalDegree ≤ Finset.sup s fun i => (f i).totalDegree := by
  induction' s using Finset.cons_induction with a s has hind
  · exact zero_le _
  · rw [Finset.sum_cons, Finset.sup_cons]
    exact (MvPolynomial.totalDegree_add _ _).trans (max_le_max le_rfl hind)
Total Degree Bound for Finite Sum of Multivariate Polynomials: $\text{totalDegree}(\sum_{i \in s} f_i) \leq \sup_{i \in s} \text{totalDegree}(f_i)$
Informal description
For any finite set $s$ of indices and any family of multivariate polynomials $(f_i)_{i \in s}$ over variables $\sigma$ and coefficients in a commutative semiring $R$, the total degree of the sum $\sum_{i \in s} f_i$ is bounded by the supremum of the total degrees of the individual polynomials: \[ \text{totalDegree}\left(\sum_{i \in s} f_i\right) \leq \sup_{i \in s} \text{totalDegree}(f_i). \]
MvPolynomial.totalDegree_finsetSum_le theorem
{ι : Type*} {s : Finset ι} {f : ι → MvPolynomial σ R} {d : ℕ} (hf : ∀ i ∈ s, (f i).totalDegree ≤ d) : (s.sum f).totalDegree ≤ d
Full source 
lemma totalDegree_finsetSum_le {ι : Type*} {s : Finset ι} {f : ι → MvPolynomial σ R} {d : ℕ}
    (hf : ∀ i ∈ s, (f i).totalDegree ≤ d) : (s.sum f).totalDegree ≤ d :=
  (totalDegree_finset_sum ..).trans <| Finset.sup_le hf
Uniform Bound on Total Degree of Finite Sum of Multivariate Polynomials: $\text{totalDegree}(\sum_{i \in s} f_i) \leq d$ when $\text{totalDegree}(f_i) \leq d$ for all $i \in s$
Informal description
For any finite set $s$ of indices, any family of multivariate polynomials $(f_i)_{i \in s}$ over variables $\sigma$ and coefficients in a commutative semiring $R$, and any natural number $d$, if each polynomial $f_i$ satisfies $\text{totalDegree}(f_i) \leq d$ for all $i \in s$, then the total degree of the sum $\sum_{i \in s} f_i$ is also bounded by $d$: \[ \text{totalDegree}\left(\sum_{i \in s} f_i\right) \leq d. \]
MvPolynomial.degreeOf_le_totalDegree theorem
(f : MvPolynomial σ R) (i : σ) : f.degreeOf i ≤ f.totalDegree
Full source 
lemma degreeOf_le_totalDegree (f : MvPolynomial σ R) (i : σ) : f.degreeOf i ≤ f.totalDegree :=
  degreeOf_le_iff.mpr fun d hd ↦ (eq_or_ne (d i) 0).elim (·.trans_le zero_le') fun h ↦
    (Finset.single_le_sum (fun _ _ ↦ zero_le') <| Finsupp.mem_support_iff.mpr h).trans
    (le_totalDegree hd)
Degree of Variable Bounded by Total Degree in Multivariate Polynomials
Informal description
For any multivariate polynomial $f \in R[X_1, \dots, X_n]$ and any variable $X_i$, the degree of $X_i$ in $f$ is less than or equal to the total degree of $f$. That is, \[ \text{degreeOf}(X_i, f) \leq \text{totalDegree}(f). \]
MvPolynomial.exists_degree_lt theorem
[Fintype σ] (f : MvPolynomial σ R) (n : ℕ) (h : f.totalDegree < n * Fintype.card σ) {d : σ →₀ ℕ} (hd : d ∈ f.support) : ∃ i, d i < n
Full source 
theorem exists_degree_lt [Fintype σ] (f : MvPolynomial σ R) (n : ℕ)
    (h : f.totalDegree < n * Fintype.card σ) {d : σ →₀ ℕ} (hd : d ∈ f.support) : ∃ i, d i < n := by
  contrapose! h
  calc
    n * Fintype.card σ = ∑ _s : σ, n := by
      rw [Finset.sum_const, Nat.nsmul_eq_mul, mul_comm, Finset.card_univ]
    _ ≤ ∑ s, d s := Finset.sum_le_sum fun s _ => h s
    _ ≤ d.sum fun _ e => e := by
      rw [Finsupp.sum_fintype]
      intros
      rfl
    _ ≤ f.totalDegree := le_totalDegree hd
Existence of Variable with Exponent Less Than $n$ in Monomials of Bounded Total Degree Polynomial
Informal description
Let $\sigma$ be a finite type and $f$ be a multivariate polynomial in variables $\sigma$ with coefficients in a commutative semiring $R$. If the total degree of $f$ is less than $n \cdot |\sigma|$ for some natural number $n$, then for any monomial $d$ appearing in $f$ (i.e., $d \in \text{support}(f)$), there exists a variable $i \in \sigma$ such that the exponent of $i$ in $d$ is less than $n$.
MvPolynomial.coeff_eq_zero_of_totalDegree_lt theorem
{f : MvPolynomial σ R} {d : σ →₀ ℕ} (h : f.totalDegree < ∑ i ∈ d.support, d i) : coeff d f = 0
Full source 
theorem coeff_eq_zero_of_totalDegree_lt {f : MvPolynomial σ R} {d : σ →₀ ℕ}
    (h : f.totalDegree < ∑ i ∈ d.support, d i) : coeff d f = 0 := by
  classical
    rw [totalDegree, Finset.sup_lt_iff] at h
    · specialize h d
      rw [mem_support_iff] at h
      refine not_not.mp (mt h ?_)
      exact lt_irrefl _
    · exact lt_of_le_of_lt (Nat.zero_le _) h
Vanishing Coefficient Criterion for Multivariate Polynomials: $\text{totalDegree}(f) < \deg(d) \implies c_d(f) = 0$
Informal description
Let $f$ be a multivariate polynomial in variables $\sigma$ with coefficients in a commutative semiring $R$, and let $d$ be a monomial in $\sigma$. If the total degree of $f$ is strictly less than the sum of exponents $\sum_{i \in \text{supp}(d)} d(i)$ in the monomial $d$, then the coefficient of $d$ in $f$ is zero.
MvPolynomial.totalDegree_eq_zero_iff_eq_C theorem
{p : MvPolynomial σ R} : p.totalDegree = 0 ↔ p = C (p.coeff 0)
Full source 
theorem totalDegree_eq_zero_iff_eq_C {p : MvPolynomial σ R} :
    p.totalDegree = 0 ↔ p = C (p.coeff 0) := by
  constructor <;> intro h
  · ext m; classical rw [coeff_C]; split_ifs with hm; · rw [← hm]
    apply coeff_eq_zero_of_totalDegree_lt; rw [h]
    exact Finset.sum_pos (fun i hi ↦ Nat.pos_of_ne_zero <| Finsupp.mem_support_iff.mp hi)
      (Finsupp.support_nonempty_iff.mpr <| Ne.symm hm)
  · rw [h, totalDegree_C]
Characterization of Zero Total Degree Multivariate Polynomials: $\text{totalDegree}(p) = 0 \iff p$ is constant
Informal description
For any multivariate polynomial $p$ with coefficients in a commutative semiring $R$, the total degree of $p$ is zero if and only if $p$ is equal to the constant polynomial $C(c)$, where $c$ is the coefficient of the zero monomial in $p$. In other words, $\text{totalDegree}(p) = 0 \iff p = C(p(0))$.
MvPolynomial.totalDegree_rename_le theorem
(f : σ → τ) (p : MvPolynomial σ R) : (rename f p).totalDegree ≤ p.totalDegree
Full source 
theorem totalDegree_rename_le (f : σ → τ) (p : MvPolynomial σ R) :
    (rename f p).totalDegree ≤ p.totalDegree :=
  Finset.sup_le fun b => by
    classical
    intro h
    rw [rename_eq] at h
    have h' := Finsupp.mapDomain_support h
    rw [Finset.mem_image] at h'
    rcases h' with ⟨s, hs, rfl⟩
    exact (sum_mapDomain_index (fun _ => rfl) (fun _ _ _ => rfl)).trans_le (le_totalDegree hs)
Total Degree Does Not Increase Under Variable Renaming
Informal description
For any multivariate polynomial $p \in R[X_1, \dots, X_n]$ and any function $f : \{X_1, \dots, X_n\} \to \{Y_1, \dots, Y_m\}$, the total degree of the polynomial obtained by renaming variables according to $f$ is less than or equal to the total degree of $p$. That is, $\text{totalDegree}(\text{rename}\, f\, p) \leq \text{totalDegree}(p)$.
MvPolynomial.totalDegree_renameEquiv theorem
(f : σ ≃ τ) (p : MvPolynomial σ R) : (renameEquiv R f p).totalDegree = p.totalDegree
Full source 
lemma totalDegree_renameEquiv (f : σ ≃ τ) (p : MvPolynomial σ R) :
    (renameEquiv R f p).totalDegree = p.totalDegree :=
  (totalDegree_rename_le f p).antisymm (le_trans (by simp) (totalDegree_rename_le f.symm _))
Invariance of Total Degree Under Variable Renaming Equivalence
Informal description
For any equivalence $f : \sigma \simeq \tau$ between variable sets and any multivariate polynomial $p \in R[\sigma]$, the total degree of $p$ is preserved under renaming variables via $f$. That is, $\text{totalDegree}(\text{renameEquiv}_R\, f\, p) = \text{totalDegree}(p)$.
MvPolynomial.degreesLE definition
: Submodule R (MvPolynomial σ R)
Full source 
/-- The submodule of multivariate polynomials of degrees bounded by a monomial `s`. -/
def degreesLE : Submodule R (MvPolynomial σ R) where
  carrier := {p | p.degrees ≤ s}
  add_mem' {a b} ha hb := by classical exact degrees_add_le.trans (sup_le ha hb)
  zero_mem' := by simp
  smul_mem' c {x} hx := by
    dsimp
    rw [Algebra.smul_def]
    refine degrees_mul_le.trans ?_
    simpa [degrees_C] using hx
Submodule of polynomials with degrees bounded by a multiset
Informal description
The submodule `degreesLE R σ s` consists of all multivariate polynomials $p \in R[\sigma]$ whose degree multiset is bounded above by a given multiset $s$ of variables. More precisely, a polynomial $p$ is in `degreesLE R σ s` if for every variable $x \in \sigma$, the maximum exponent of $x$ in any monomial of $p$ is less than or equal to the multiplicity of $x$ in $s$.
MvPolynomial.mem_degreesLE theorem
: p ∈ degreesLE R σ s ↔ p.degrees ≤ s
Full source 
@[simp] lemma mem_degreesLE : p ∈ degreesLE R σ sp ∈ degreesLE R σ s ↔ p.degrees ≤ s := Iff.rfl
Membership in Degrees-Bounded Submodule via Multiset Comparison
Informal description
A multivariate polynomial $p \in R[\sigma]$ belongs to the submodule $\text{degreesLE}\, R\, \sigma\, s$ if and only if the multiset of maximal variable degrees of $p$ is bounded above by the multiset $s$ under the sub-multiset relation $\leq$.
MvPolynomial.degreesLE_add theorem
: degreesLE R σ (s + t) = degreesLE R σ s * degreesLE R σ t
Full source 
lemma degreesLE_add : degreesLE R σ (s + t) = degreesLE R σ s * degreesLE R σ t := by
  classical
  rw [le_antisymm_iff, Submodule.mul_le]
  refine ⟨fun x hx ↦ x.as_sum ▸ sum_mem fun i hi ↦ ?_,
    fun x hx y hy ↦ degrees_mul_le.trans (add_le_add hx hy)⟩
  replace hi : i.toMultiset ≤ s + t := (Finset.le_sup hi).trans hx
  let a := (i.toMultiset - t).toFinsupp
  let b := (i.toMultiset ⊓ t).toFinsupp
  have : a + b = i := Multiset.toFinsupp.symm.injective (by simp [a, b, Multiset.sub_add_inter])
  have ha : a.toMultiset ≤ s := by simpa [a, add_comm (a := t)] using hi
  have hb : b.toMultiset ≤ t := by simp [b, Multiset.inter_le_right]
  rw [show monomial i (x.coeff i) = monomial a (x.coeff i) * monomial b 1 by simp [this]]
  exact Submodule.mul_mem_mul ((degrees_monomial _ _).trans ha) ((degrees_monomial _ _).trans hb)
Additivity of Degrees-Bounded Submodules under Multiset Addition: $\text{degreesLE}(s + t) = \text{degreesLE}(s) \cdot \text{degreesLE}(t)$
Informal description
For any commutative semiring $R$ and any type $\sigma$ indexing the variables, the submodule of multivariate polynomials with degrees bounded by the sum of two multisets $s$ and $t$ is equal to the product of the submodules of polynomials with degrees bounded by $s$ and $t$ respectively. That is, \[ \text{degreesLE}\, R\, \sigma\, (s + t) = (\text{degreesLE}\, R\, \sigma\, s) \cdot (\text{degreesLE}\, R\, \sigma\, t). \]
MvPolynomial.degreesLE_zero theorem
: degreesLE R σ 0 = 1
Full source 
@[simp] lemma degreesLE_zero : degreesLE R σ 0 = 1 := by
  refine le_antisymm (fun x hx ↦ ?_) (by simp)
  simp only [mem_degreesLE, nonpos_iff_eq_zero] at hx
  have := (totalDegree_eq_zero_iff_eq_C (p := x)).mp
    (Nat.eq_zero_of_le_zero (x.totalDegree_le_degrees_card.trans (by simp [hx])))
  exact ⟨x.coeff 0, by simp [Algebra.smul_def, ← this]⟩
Degrees-Bounded Submodule for Empty Multiset is Trivial
Informal description
The submodule of multivariate polynomials with degrees bounded by the empty multiset is equal to the trivial submodule generated by the constant polynomial 1, i.e., $\text{degreesLE}\, R\, \sigma\, 0 = 1$.
MvPolynomial.degreesLE_nsmul theorem
: ∀ n, degreesLE R σ (n • s) = degreesLE R σ s ^ n
Full source 
lemma degreesLE_nsmul : ∀ n, degreesLE R σ (n • s) = degreesLE R σ s ^ n
  | 0 => by simp
  | k + 1 => by simp only [pow_succ, degreesLE_nsmul, degreesLE_add, add_smul, one_smul]
Scalar Multiplication of Degrees-Bounded Submodules: $\text{degreesLE}(n \cdot s) = \text{degreesLE}(s)^n$
Informal description
For any commutative semiring $R$, any type $\sigma$ indexing the variables, and any multiset $s$ of variables, the submodule of multivariate polynomials with degrees bounded by the $n$-th scalar multiple of $s$ is equal to the $n$-th power of the submodule of polynomials with degrees bounded by $s$. That is, for any natural number $n$, \[ \text{degreesLE}\, R\, \sigma\, (n \cdot s) = (\text{degreesLE}\, R\, \sigma\, s)^n. \]