# Documentation

Mathlib.Data.MvPolynomial.Variables

# Degrees and variables of polynomials #

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 #

• 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.vars p : the finset of variables occurring in p. For example if p = x⁴y+yz then vars p = {x, y, z}

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

Instances For
theorem MvPolynomial.degrees_def {R : Type u} {σ : Type u_1} [] [] (p : ) :
= Finset.sup () fun s => Finsupp.toMultiset s
theorem MvPolynomial.degrees_monomial {R : Type u} {σ : Type u_1} [] (s : σ →₀ ) (a : R) :
Finsupp.toMultiset s
theorem MvPolynomial.degrees_monomial_eq {R : Type u} {σ : Type u_1} [] (s : σ →₀ ) (a : R) (ha : a 0) :
= Finsupp.toMultiset s
theorem MvPolynomial.degrees_C {R : Type u} {σ : Type u_1} [] (a : R) :
MvPolynomial.degrees (MvPolynomial.C a) = 0
theorem MvPolynomial.degrees_X' {R : Type u} {σ : Type u_1} [] (n : σ) :
@[simp]
theorem MvPolynomial.degrees_X {R : Type u} {σ : Type u_1} [] [] (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 : ) :
theorem MvPolynomial.degrees_sum {R : Type u} {σ : Type u_1} [] {ι : Type u_3} [] (s : ) (f : ι) :
theorem MvPolynomial.degrees_mul {R : Type u} {σ : Type u_1} [] (p : ) (q : ) :
theorem MvPolynomial.degrees_prod {R : Type u} {σ : Type u_1} [] {ι : Type u_3} (s : ) (f : ι) :
theorem MvPolynomial.degrees_pow {R : Type u} {σ : Type u_1} [] (p : ) (n : ) :
theorem MvPolynomial.mem_degrees {R : Type u} {σ : Type u_1} [] {p : } {i : σ} :
d, 0 i d.support
theorem MvPolynomial.le_degrees_add {R : Type u} {σ : Type u_1} [] {p : } {q : } (h : ) :
theorem MvPolynomial.degrees_add_of_disjoint {R : Type u} {σ : Type u_1} [] [] {p : } {q : } (h : ) :
theorem MvPolynomial.degrees_map {R : Type u} {S : Type v} {σ : Type u_1} [] [] (p : ) (f : R →+* S) :
theorem MvPolynomial.degrees_rename {R : Type u} {σ : Type u_1} {τ : Type u_2} [] (f : στ) (φ : ) :
theorem MvPolynomial.degrees_map_of_injective {R : Type u} {S : Type v} {σ : Type u_1} [] [] (p : ) {f : R →+* S} (hf : ) :
theorem MvPolynomial.degrees_rename_of_injective {R : Type u} {σ : Type u_1} {τ : Type u_2} [] {p : } {f : στ} (h : ) :

### vars#

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

vars p is the set of variables appearing in the polynomial p

Instances For
theorem MvPolynomial.vars_def {R : Type u} {σ : Type u_1} [] [] (p : ) :
@[simp]
theorem MvPolynomial.vars_0 {R : Type u} {σ : Type u_1} [] :
@[simp]
theorem MvPolynomial.vars_monomial {R : Type u} {σ : Type u_1} {r : R} {s : σ →₀ } [] (h : r 0) :
= s.support
@[simp]
theorem MvPolynomial.vars_C {R : Type u} {σ : Type u_1} {r : R} [] :
MvPolynomial.vars (MvPolynomial.C r) =
@[simp]
theorem MvPolynomial.vars_X {R : Type u} {σ : Type u_1} {n : σ} [] [] :
= {n}
theorem MvPolynomial.mem_vars {R : Type u} {σ : Type u_1} [] {p : } (i : σ) :
d x, i d.support
theorem MvPolynomial.mem_support_not_mem_vars_zero {R : Type u} {σ : Type u_1} [] {f : } {x : σ →₀ } (H : ) {v : σ} (h : ¬) :
x v = 0
theorem MvPolynomial.vars_add_subset {R : Type u} {σ : Type u_1} [] [] (p : ) (q : ) :
theorem MvPolynomial.vars_add_of_disjoint {R : Type u} {σ : Type u_1} [] {p : } {q : } [] (h : ) :
theorem MvPolynomial.vars_mul {R : Type u} {σ : Type u_1} [] [] (φ : ) (ψ : ) :
@[simp]
theorem MvPolynomial.vars_one {R : Type u} {σ : Type u_1} [] :
theorem MvPolynomial.vars_pow {R : Type u} {σ : Type u_1} [] (φ : ) (n : ) :
theorem MvPolynomial.vars_prod {R : Type u} {σ : Type u_1} [] {ι : Type u_3} [] {s : } (f : ι) :

The variables of the product of a family of polynomials are a subset of the union of the sets of variables of each polynomial.

theorem MvPolynomial.vars_C_mul {σ : Type u_1} {A : Type u_3} [] [] (a : A) (ha : a 0) (φ : ) :
MvPolynomial.vars (MvPolynomial.C a * φ) =
theorem MvPolynomial.vars_sum_subset {R : Type u} {σ : Type u_1} [] {ι : Type u_3} (t : ) (φ : ι) [] :
theorem MvPolynomial.vars_sum_of_disjoint {R : Type u} {σ : Type u_1} [] {ι : Type u_3} (t : ) (φ : ι) [] (h : Pairwise (Disjoint on fun i => MvPolynomial.vars (φ i))) :
MvPolynomial.vars (Finset.sum t fun i => φ i) = Finset.biUnion t fun i => MvPolynomial.vars (φ i)
theorem MvPolynomial.vars_map {R : Type u} {S : Type v} {σ : Type u_1} [] (p : ) [] (f : R →+* S) :
theorem MvPolynomial.vars_map_of_injective {R : Type u} {S : Type v} {σ : Type u_1} [] (p : ) [] {f : R →+* S} (hf : ) :
theorem MvPolynomial.vars_monomial_single {R : Type u} {σ : Type u_1} [] (i : σ) {e : } {r : R} (he : e 0) (hr : r 0) :
MvPolynomial.vars (↑(MvPolynomial.monomial fun₀ | i => e) r) = {i}
theorem MvPolynomial.vars_eq_support_biUnion_support {R : Type u} {σ : Type u_1} [] (p : ) [] :
= Finset.biUnion () Finsupp.support

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

Instances For
theorem MvPolynomial.degreeOf_def {R : Type u} {σ : Type u_1} [] [] (n : σ) (p : ) :
theorem MvPolynomial.degreeOf_eq_sup {R : Type u} {σ : Type u_1} [] (n : σ) (f : ) :
= Finset.sup () fun m => m n
theorem MvPolynomial.degreeOf_lt_iff {R : Type u} {σ : Type u_1} [] {n : σ} {f : } {d : } (h : 0 < d) :
∀ (m : σ →₀ ), 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 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_rename_of_injective {R : Type u} {σ : Type u_1} {τ : Type u_2} [] {p : } {f : στ} (h : ) (i : σ) :
MvPolynomial.degreeOf (f i) (↑() p) =

### totalDegree#

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

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

Instances For
theorem MvPolynomial.totalDegree_eq {R : Type u} {σ : Type u_1} [] (p : ) :
= Finset.sup () fun m => Multiset.card (Finsupp.toMultiset m)
theorem MvPolynomial.le_totalDegree {R : Type u} {σ : Type u_1} [] {p : } {s : σ →₀ } (h : ) :
(Finsupp.sum s fun x e => e)
theorem MvPolynomial.totalDegree_le_degrees_card {R : Type u} {σ : Type u_1} [] (p : ) :
Multiset.card ()
@[simp]
theorem MvPolynomial.totalDegree_C {R : Type u} {σ : Type u_1} [] (a : R) :
MvPolynomial.totalDegree (MvPolynomial.C a) = 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 : σ) :
theorem MvPolynomial.totalDegree_add {R : Type u} {σ : Type u_1} [] (a : ) (b : ) :
theorem MvPolynomial.totalDegree_add_eq_left_of_totalDegree_lt {R : Type u} {σ : Type u_1} [] {p : } {q : } :
theorem MvPolynomial.totalDegree_add_eq_right_of_totalDegree_lt {R : Type u} {σ : Type u_1} [] {p : } {q : } :
theorem MvPolynomial.totalDegree_mul {R : Type u} {σ : Type u_1} [] (a : ) (b : ) :
theorem MvPolynomial.totalDegree_smul_le {R : Type u} {S : Type v} {σ : Type u_1} [] [] [] (a : R) (f : ) :
theorem MvPolynomial.totalDegree_pow {R : Type u} {σ : Type u_1} [] (a : ) (n : ) :
@[simp]
theorem MvPolynomial.totalDegree_monomial {R : Type u} {σ : Type u_1} [] (s : σ →₀ ) {c : R} (hc : c 0) :
= Finsupp.sum s fun x e => e
@[simp]
theorem MvPolynomial.totalDegree_X_pow {R : Type u} {σ : Type u_1} [] [] (s : σ) (n : ) :
theorem MvPolynomial.totalDegree_list_prod {R : Type u} {σ : Type u_1} [] (s : List ()) :
List.sum (List.map MvPolynomial.totalDegree s)
theorem MvPolynomial.totalDegree_multiset_prod {R : Type u} {σ : Type u_1} [] (s : Multiset ()) :
Multiset.sum (Multiset.map MvPolynomial.totalDegree s)
theorem MvPolynomial.totalDegree_finset_prod {R : Type u} {σ : Type u_1} [] {ι : Type u_3} (s : ) (f : ι) :
Finset.sum s fun i =>
theorem MvPolynomial.totalDegree_finset_sum {R : Type u} {σ : Type u_1} [] {ι : Type u_3} (s : ) (f : ι) :
Finset.sup s fun i =>
theorem MvPolynomial.exists_degree_lt {R : Type u} {σ : Type u_1} [] [] (f : ) (n : ) (h : ) {d : σ →₀ } (hd : ) :
i, d i < n
theorem MvPolynomial.coeff_eq_zero_of_totalDegree_lt {R : Type u} {σ : Type u_1} [] {f : } {d : σ →₀ } (h : < Finset.sum d.support fun i => d i) :
= 0
theorem MvPolynomial.totalDegree_rename_le {R : Type u} {σ : Type u_1} {τ : Type u_2} [] (f : στ) (p : ) :

### vars and eval#

theorem MvPolynomial.eval₂Hom_eq_constantCoeff_of_vars {R : Type u} {S : Type v} {σ : Type u_1} [] [] (f : R →+* S) {g : σS} {p : } (hp : ∀ (i : σ), g i = 0) :
↑() p = f (MvPolynomial.constantCoeff p)
theorem MvPolynomial.aeval_eq_constantCoeff_of_vars {R : Type u} {S : Type v} {σ : Type u_1} [] [] [Algebra R S] {g : σS} {p : } (hp : ∀ (i : σ), g i = 0) :
↑() p = ↑(algebraMap ((fun x => R) p) S) (MvPolynomial.constantCoeff p)
theorem MvPolynomial.eval₂Hom_congr' {R : Type u} {S : Type v} {σ : Type u_1} [] [] {f₁ : R →+* S} {f₂ : R →+* S} {g₁ : σS} {g₂ : σS} {p₁ : } {p₂ : } :
f₁ = f₂(∀ (i : σ), g₁ i = g₂ i) → p₁ = p₂↑() p₁ = ↑() p₂
theorem MvPolynomial.hom_congr_vars {R : Type u} {S : Type v} {σ : Type u_1} [] [] {f₁ : →+* S} {f₂ : →+* S} {p₁ : } {p₂ : } (hC : RingHom.comp f₁ MvPolynomial.C = RingHom.comp f₂ MvPolynomial.C) (hv : ∀ (i : σ), f₁ () = f₂ ()) (hp : p₁ = p₂) :
f₁ p₁ = f₂ p₂

If f₁ and f₂ are ring homs out of the polynomial ring and p₁ and p₂ are polynomials, then f₁ p₁ = f₂ p₂ if p₁ = p₂ and f₁ and f₂ are equal on R and on the variables of p₁.

theorem MvPolynomial.exists_rename_eq_of_vars_subset_range {R : Type u} {σ : Type u_1} {τ : Type u_2} [] (p : ) (f : τσ) (hfi : ) (hf : ↑() ) :
q, ↑() q = p
theorem MvPolynomial.vars_rename {R : Type u} {σ : Type u_1} {τ : Type u_2} [] [] (f : στ) (φ : ) :
theorem MvPolynomial.mem_vars_rename {R : Type u} {σ : Type u_1} {τ : Type u_2} [] (f : στ) (φ : ) {j : τ} (h : j MvPolynomial.vars (↑() φ)) :
i, f i = j