# 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#

def MvPolynomial.degrees {R : Type u} {σ : Type u_1} [] (p : ) :

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}.)

Equations
• p.degrees = p.support.sup fun (s : σ →₀ ) => Finsupp.toMultiset s
Instances For
theorem MvPolynomial.degrees_def {R : Type u} {σ : Type u_1} [] [] (p : ) :
p.degrees = p.support.sup fun (s : σ →₀ ) => Finsupp.toMultiset s
theorem MvPolynomial.degrees_monomial {R : Type u} {σ : Type u_1} [] (s : σ →₀ ) (a : R) :
( a).degrees Finsupp.toMultiset s
theorem MvPolynomial.degrees_monomial_eq {R : Type u} {σ : Type u_1} [] (s : σ →₀ ) (a : R) (ha : a 0) :
( a).degrees = Finsupp.toMultiset s
theorem MvPolynomial.degrees_C {R : Type u} {σ : Type u_1} [] (a : R) :
(MvPolynomial.C a).degrees = 0
theorem MvPolynomial.degrees_X' {R : Type u} {σ : Type u_1} [] (n : σ) :
.degrees {n}
@[simp]
theorem MvPolynomial.degrees_X {R : Type u} {σ : Type u_1} [] [] (n : σ) :
.degrees = {n}
@[simp]
theorem MvPolynomial.degrees_zero {R : Type u} {σ : Type u_1} [] :
@[simp]
theorem MvPolynomial.degrees_one {R : Type u} {σ : Type u_1} [] :
theorem MvPolynomial.degrees_add {R : Type u} {σ : Type u_1} [] [] (p : ) (q : ) :
(p + q).degrees p.degrees q.degrees
theorem MvPolynomial.degrees_sum {R : Type u} {σ : Type u_1} [] {ι : Type u_3} [] (s : ) (f : ι) :
(∑ is, f i).degrees s.sup fun (i : ι) => (f i).degrees
theorem MvPolynomial.degrees_mul {R : Type u} {σ : Type u_1} [] (p : ) (q : ) :
(p * q).degrees p.degrees + q.degrees
theorem MvPolynomial.degrees_prod {R : Type u} {σ : Type u_1} [] {ι : Type u_3} (s : ) (f : ι) :
(∏ is, f i).degrees is, (f i).degrees
theorem MvPolynomial.degrees_pow {R : Type u} {σ : Type u_1} [] (p : ) (n : ) :
(p ^ n).degrees n p.degrees
theorem MvPolynomial.mem_degrees {R : Type u} {σ : Type u_1} [] {p : } {i : σ} :
i p.degrees ∃ (d : σ →₀ ), 0 i d.support
theorem MvPolynomial.le_degrees_add {R : Type u} {σ : Type u_1} [] {p : } {q : } (h : p.degrees.Disjoint q.degrees) :
p.degrees (p + q).degrees
theorem MvPolynomial.degrees_add_of_disjoint {R : Type u} {σ : Type u_1} [] [] {p : } {q : } (h : p.degrees.Disjoint q.degrees) :
(p + q).degrees = p.degrees q.degrees
theorem MvPolynomial.degrees_map {R : Type u} {S : Type v} {σ : Type u_1} [] [] (p : ) (f : R →+* S) :
( p).degrees p.degrees
theorem MvPolynomial.degrees_rename {R : Type u} {σ : Type u_1} {τ : Type u_2} [] (f : στ) (φ : ) :
( φ).degrees Multiset.map f φ.degrees
theorem MvPolynomial.degrees_map_of_injective {R : Type u} {S : Type v} {σ : Type u_1} [] [] (p : ) {f : R →+* S} (hf : ) :
( p).degrees = p.degrees
theorem MvPolynomial.degrees_rename_of_injective {R : Type u} {σ : Type u_1} {τ : Type u_2} [] {p : } {f : στ} (h : ) :
( p).degrees = Multiset.map f p.degrees

### degreeOf#

def MvPolynomial.degreeOf {R : Type u} {σ : Type u_1} [] (n : σ) (p : ) :

degreeOf n p gives the highest power of X_n that appears in p

Equations
Instances For
theorem MvPolynomial.degreeOf_def {R : Type u} {σ : Type u_1} [] [] (n : σ) (p : ) :
= Multiset.count n p.degrees
theorem MvPolynomial.degreeOf_eq_sup {R : Type u} {σ : Type u_1} [] (n : σ) (f : ) :
= f.support.sup fun (m : σ →₀ ) => m n
theorem MvPolynomial.degreeOf_lt_iff {R : Type u} {σ : Type u_1} [] {n : σ} {f : } {d : } (h : 0 < d) :
mf.support, m n < d
theorem MvPolynomial.degreeOf_le_iff {R : Type u} {σ : Type u_1} [] {n : σ} {f : } {d : } :
mf.support, m n d
@[simp]
theorem MvPolynomial.degreeOf_zero {R : Type u} {σ : Type u_1} [] (n : σ) :
@[simp]
theorem MvPolynomial.degreeOf_C {R : Type u} {σ : Type u_1} [] (a : R) (x : σ) :
MvPolynomial.degreeOf x (MvPolynomial.C a) = 0
theorem MvPolynomial.degreeOf_X {R : Type u} {σ : Type u_1} [] [] (i : σ) (j : σ) [] :
= if i = j then 1 else 0
theorem MvPolynomial.degreeOf_add_le {R : Type u} {σ : Type u_1} [] (n : σ) (f : ) (g : ) :
theorem MvPolynomial.monomial_le_degreeOf {R : Type u} {σ : Type u_1} [] (i : σ) {f : } {m : σ →₀ } (h_m : m f.support) :
m i
theorem MvPolynomial.degreeOf_mul_le {R : Type u} {σ : Type u_1} [] (i : σ) (f : ) (g : ) :
theorem MvPolynomial.degreeOf_mul_X_ne {R : Type u} {σ : Type u_1} [] {i : σ} {j : σ} (f : ) (h : i j) :
theorem MvPolynomial.degreeOf_mul_X_eq {R : Type u} {σ : Type u_1} [] (j : σ) (f : ) :
theorem MvPolynomial.degreeOf_C_mul_le {R : Type u} {σ : Type u_1} [] (p : ) (i : σ) (c : R) :
MvPolynomial.degreeOf i (MvPolynomial.C c * p)
theorem MvPolynomial.degreeOf_mul_C_le {R : Type u} {σ : Type u_1} [] (p : ) (i : σ) (c : R) :
MvPolynomial.degreeOf i (p * MvPolynomial.C c)
theorem MvPolynomial.degreeOf_rename_of_injective {R : Type u} {σ : Type u_1} {τ : Type u_2} [] {p : } {f : στ} (h : ) (i : σ) :

### totalDegree#

def MvPolynomial.totalDegree {R : Type u} {σ : Type u_1} [] (p : ) :

totalDegree p gives the maximum |s| over the monomials X^s in p

Equations
• p.totalDegree = p.support.sup fun (s : σ →₀ ) => s.sum fun (x : σ) (e : ) => e
Instances For
theorem MvPolynomial.totalDegree_eq {R : Type u} {σ : Type u_1} [] (p : ) :
p.totalDegree = p.support.sup fun (m : σ →₀ ) => Multiset.card (Finsupp.toMultiset m)
theorem MvPolynomial.le_totalDegree {R : Type u} {σ : Type u_1} [] {p : } {s : σ →₀ } (h : s p.support) :
(s.sum fun (x : σ) (e : ) => e) p.totalDegree
theorem MvPolynomial.totalDegree_le_degrees_card {R : Type u} {σ : Type u_1} [] (p : ) :
p.totalDegree Multiset.card p.degrees
theorem MvPolynomial.totalDegree_le_of_support_subset {R : Type u} {σ : Type u_1} [] {p : } {q : } (h : p.support q.support) :
p.totalDegree q.totalDegree
@[simp]
theorem MvPolynomial.totalDegree_C {R : Type u} {σ : Type u_1} [] (a : R) :
(MvPolynomial.C a).totalDegree = 0
@[simp]
theorem MvPolynomial.totalDegree_zero {R : Type u} {σ : Type u_1} [] :
@[simp]
theorem MvPolynomial.totalDegree_one {R : Type u} {σ : Type u_1} [] :
@[simp]
theorem MvPolynomial.totalDegree_X {σ : Type u_1} {R : Type u_3} [] [] (s : σ) :
.totalDegree = 1
theorem MvPolynomial.totalDegree_add {R : Type u} {σ : Type u_1} [] (a : ) (b : ) :
(a + b).totalDegree max a.totalDegree b.totalDegree
theorem MvPolynomial.totalDegree_add_eq_left_of_totalDegree_lt {R : Type u} {σ : Type u_1} [] {p : } {q : } (h : q.totalDegree < p.totalDegree) :
(p + q).totalDegree = p.totalDegree
theorem MvPolynomial.totalDegree_add_eq_right_of_totalDegree_lt {R : Type u} {σ : Type u_1} [] {p : } {q : } (h : q.totalDegree < p.totalDegree) :
(q + p).totalDegree = p.totalDegree
theorem MvPolynomial.totalDegree_mul {R : Type u} {σ : Type u_1} [] (a : ) (b : ) :
(a * b).totalDegree a.totalDegree + b.totalDegree
theorem MvPolynomial.totalDegree_smul_le {R : Type u} {S : Type v} {σ : Type u_1} [] [] [] (a : R) (f : ) :
(a f).totalDegree f.totalDegree
theorem MvPolynomial.totalDegree_pow {R : Type u} {σ : Type u_1} [] (a : ) (n : ) :
(a ^ n).totalDegree n * a.totalDegree
@[simp]
theorem MvPolynomial.totalDegree_monomial {R : Type u} {σ : Type u_1} [] (s : σ →₀ ) {c : R} (hc : c 0) :
( c).totalDegree = s.sum fun (x : σ) (e : ) => e
theorem MvPolynomial.totalDegree_monomial_le {R : Type u} {σ : Type u_1} [] (s : σ →₀ ) (c : R) :
( c).totalDegree s.sum fun (x : σ) => id
@[simp]
theorem MvPolynomial.totalDegree_X_pow {R : Type u} {σ : Type u_1} [] [] (s : σ) (n : ) :
( ^ n).totalDegree = n
theorem MvPolynomial.totalDegree_list_prod {R : Type u} {σ : Type u_1} [] (s : List (MvPolynomial σ R)) :
s.prod.totalDegree (List.map MvPolynomial.totalDegree s).sum
theorem MvPolynomial.totalDegree_multiset_prod {R : Type u} {σ : Type u_1} [] (s : Multiset (MvPolynomial σ R)) :
s.prod.totalDegree (Multiset.map MvPolynomial.totalDegree s).sum
theorem MvPolynomial.totalDegree_finset_prod {R : Type u} {σ : Type u_1} [] {ι : Type u_3} (s : ) (f : ι) :
(s.prod f).totalDegree is, (f i).totalDegree
theorem MvPolynomial.totalDegree_finset_sum {R : Type u} {σ : Type u_1} [] {ι : Type u_3} (s : ) (f : ι) :
(s.sum f).totalDegree s.sup fun (i : ι) => (f i).totalDegree
theorem MvPolynomial.totalDegree_finsetSum_le {R : Type u} {σ : Type u_1} [] {ι : Type u_3} {s : } {f : ι} {d : } (hf : is, (f i).totalDegree d) :
(s.sum f).totalDegree d
theorem MvPolynomial.degreeOf_le_totalDegree {R : Type u} {σ : Type u_1} [] (f : ) (i : σ) :
f.totalDegree
theorem MvPolynomial.exists_degree_lt {R : Type u} {σ : Type u_1} [] [] (f : ) (n : ) (h : f.totalDegree < ) {d : σ →₀ } (hd : d f.support) :
∃ (i : σ), d i < n
theorem MvPolynomial.coeff_eq_zero_of_totalDegree_lt {R : Type u} {σ : Type u_1} [] {f : } {d : σ →₀ } (h : f.totalDegree < id.support, d i) :
= 0
theorem MvPolynomial.totalDegree_rename_le {R : Type u} {σ : Type u_1} {τ : Type u_2} [] (f : στ) (p : ) :
( p).totalDegree p.totalDegree