# mathlib3documentation

data.mv_polynomial.variables

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

noncomputable def mv_polynomial.degrees {R : Type u} {σ : Type u_1} (p : R) :

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
theorem mv_polynomial.degrees_def {R : Type u} {σ : Type u_1} [decidable_eq σ] (p : R) :
p.degrees = p.support.sup (λ (s : σ →₀ ),
theorem mv_polynomial.degrees_monomial {R : Type u} {σ : Type u_1} (s : σ →₀ ) (a : R) :
theorem mv_polynomial.degrees_monomial_eq {R : Type u} {σ : Type u_1} (s : σ →₀ ) (a : R) (ha : a 0) :
theorem mv_polynomial.degrees_C {R : Type u} {σ : Type u_1} (a : R) :
= 0
theorem mv_polynomial.degrees_X' {R : Type u} {σ : Type u_1} (n : σ) :
{n}
@[simp]
theorem mv_polynomial.degrees_X {R : Type u} {σ : Type u_1} [nontrivial R] (n : σ) :
= {n}
@[simp]
theorem mv_polynomial.degrees_zero {R : Type u} {σ : Type u_1}  :
@[simp]
theorem mv_polynomial.degrees_one {R : Type u} {σ : Type u_1}  :
theorem mv_polynomial.degrees_add {R : Type u} {σ : Type u_1} [decidable_eq σ] (p q : R) :
theorem mv_polynomial.degrees_sum {R : Type u} {σ : Type u_1} {ι : Type u_2} [decidable_eq σ] (s : finset ι) (f : ι ) :
(s.sum (λ (i : ι), f i)).degrees s.sup (λ (i : ι), (f i).degrees)
theorem mv_polynomial.degrees_mul {R : Type u} {σ : Type u_1} (p q : R) :
theorem mv_polynomial.degrees_prod {R : Type u} {σ : Type u_1} {ι : Type u_2} (s : finset ι) (f : ι ) :
(s.prod (λ (i : ι), f i)).degrees s.sum (λ (i : ι), (f i).degrees)
theorem mv_polynomial.degrees_pow {R : Type u} {σ : Type u_1} (p : R) (n : ) :
(p ^ n).degrees n p.degrees
theorem mv_polynomial.mem_degrees {R : Type u} {σ : Type u_1} {p : R} {i : σ} :
i p.degrees (d : σ →₀ ), 0 i d.support
theorem mv_polynomial.le_degrees_add {R : Type u} {σ : Type u_1} {p q : R} (h : p.degrees.disjoint q.degrees) :
theorem mv_polynomial.degrees_add_of_disjoint {R : Type u} {σ : Type u_1} [decidable_eq σ] {p q : R} (h : p.degrees.disjoint q.degrees) :
theorem mv_polynomial.degrees_map {R : Type u} {S : Type v} {σ : Type u_1} (p : R) (f : R →+* S) :
theorem mv_polynomial.degrees_rename {R : Type u} {σ : Type u_1} {τ : Type u_2} (f : σ τ) (φ : R) :
φ).degrees
theorem mv_polynomial.degrees_map_of_injective {R : Type u} {S : Type v} {σ : Type u_1} (p : R) {f : R →+* S} (hf : function.injective f) :
theorem mv_polynomial.degrees_rename_of_injective {R : Type u} {σ : Type u_1} {τ : Type u_2} {p : R} {f : σ τ} (h : function.injective f) :
p).degrees =

### vars#

noncomputable def mv_polynomial.vars {R : Type u} {σ : Type u_1} (p : R) :

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

Equations
theorem mv_polynomial.vars_def {R : Type u} {σ : Type u_1} [decidable_eq σ] (p : R) :
@[simp]
theorem mv_polynomial.vars_0 {R : Type u} {σ : Type u_1}  :
@[simp]
theorem mv_polynomial.vars_monomial {R : Type u} {σ : Type u_1} {r : R} {s : σ →₀ } (h : r 0) :
r).vars = s.support
@[simp]
theorem mv_polynomial.vars_C {R : Type u} {σ : Type u_1} {r : R}  :
@[simp]
theorem mv_polynomial.vars_X {R : Type u} {σ : Type u_1} {n : σ} [nontrivial R] :
.vars = {n}
theorem mv_polynomial.mem_vars {R : Type u} {σ : Type u_1} {p : R} (i : σ) :
i p.vars (d : σ →₀ ) (H : d p.support), i d.support
theorem mv_polynomial.mem_support_not_mem_vars_zero {R : Type u} {σ : Type u_1} {f : R} {x : σ →₀ } (H : x f.support) {v : σ} (h : v f.vars) :
x v = 0
theorem mv_polynomial.vars_add_subset {R : Type u} {σ : Type u_1} [decidable_eq σ] (p q : R) :
(p + q).vars p.vars q.vars
theorem mv_polynomial.vars_add_of_disjoint {R : Type u} {σ : Type u_1} {p q : R} [decidable_eq σ] (h : q.vars) :
(p + q).vars = p.vars q.vars
theorem mv_polynomial.vars_mul {R : Type u} {σ : Type u_1} [decidable_eq σ] (φ ψ : R) :
* ψ).vars φ.vars ψ.vars
@[simp]
theorem mv_polynomial.vars_one {R : Type u} {σ : Type u_1}  :
theorem mv_polynomial.vars_pow {R : Type u} {σ : Type u_1} (φ : R) (n : ) :
^ n).vars φ.vars
theorem mv_polynomial.vars_prod {R : Type u} {σ : Type u_1} {ι : Type u_2} [decidable_eq σ] {s : finset ι} (f : ι ) :
(s.prod (λ (i : ι), f i)).vars s.bUnion (λ (i : ι), (f i).vars)

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 mv_polynomial.vars_C_mul {σ : Type u_1} {A : Type u_3} [comm_ring A] [is_domain A] (a : A) (ha : a 0) (φ : A) :
* φ).vars = φ.vars
theorem mv_polynomial.vars_sum_subset {R : Type u} {σ : Type u_1} {ι : Type u_3} (t : finset ι) (φ : ι ) [decidable_eq σ] :
(t.sum (λ (i : ι), φ i)).vars t.bUnion (λ (i : ι), (φ i).vars)
theorem mv_polynomial.vars_sum_of_disjoint {R : Type u} {σ : Type u_1} {ι : Type u_3} (t : finset ι) (φ : ι ) [decidable_eq σ] (h : pairwise (disjoint on λ (i : ι), (φ i).vars)) :
(t.sum (λ (i : ι), φ i)).vars = t.bUnion (λ (i : ι), (φ i).vars)
theorem mv_polynomial.vars_map {R : Type u} {S : Type v} {σ : Type u_1} (p : R) (f : R →+* S) :
theorem mv_polynomial.vars_map_of_injective {R : Type u} {S : Type v} {σ : Type u_1} (p : R) {f : R →+* S} (hf : function.injective f) :
( p).vars = p.vars
theorem mv_polynomial.vars_monomial_single {R : Type u} {σ : Type u_1} (i : σ) {e : } {r : R} (he : e 0) (hr : r 0) :
( r).vars = {i}
theorem mv_polynomial.vars_eq_support_bUnion_support {R : Type u} {σ : Type u_1} (p : R) [decidable_eq σ] :

### degree_of#

noncomputable def mv_polynomial.degree_of {R : Type u} {σ : Type u_1} (n : σ) (p : R) :

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

Equations
• = let _inst : := in
theorem mv_polynomial.degree_of_def {R : Type u} {σ : Type u_1} [decidable_eq σ] (n : σ) (p : R) :
theorem mv_polynomial.degree_of_eq_sup {R : Type u} {σ : Type u_1} (n : σ) (f : R) :
= f.support.sup (λ (m : σ →₀ ), m n)
theorem mv_polynomial.degree_of_lt_iff {R : Type u} {σ : Type u_1} {n : σ} {f : R} {d : } (h : 0 < d) :
(m : σ →₀ ), m f.support m n < d
@[simp]
theorem mv_polynomial.degree_of_zero {R : Type u} {σ : Type u_1} (n : σ) :
@[simp]
theorem mv_polynomial.degree_of_C {R : Type u} {σ : Type u_1} (a : R) (x : σ) :
theorem mv_polynomial.degree_of_X {R : Type u} {σ : Type u_1} [decidable_eq σ] (i j : σ) [nontrivial R] :
= ite (i = j) 1 0
theorem mv_polynomial.degree_of_add_le {R : Type u} {σ : Type u_1} (n : σ) (f g : R) :
(f + g)
theorem mv_polynomial.monomial_le_degree_of {R : Type u} {σ : Type u_1} (i : σ) {f : R} {m : σ →₀ } (h_m : m f.support) :
m i
theorem mv_polynomial.degree_of_mul_le {R : Type u} {σ : Type u_1} (i : σ) (f g : R) :
(f * g)
theorem mv_polynomial.degree_of_mul_X_ne {R : Type u} {σ : Type u_1} {i j : σ} (f : R) (h : i j) :
theorem mv_polynomial.degree_of_mul_X_eq {R : Type u} {σ : Type u_1} (j : σ) (f : R) :
theorem mv_polynomial.degree_of_rename_of_injective {R : Type u} {σ : Type u_1} {τ : Type u_2} {p : R} {f : σ τ} (h : function.injective f) (i : σ) :
p) =

### total_degree#

def mv_polynomial.total_degree {R : Type u} {σ : Type u_1} (p : R) :

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

Equations
theorem mv_polynomial.total_degree_eq {R : Type u} {σ : Type u_1} (p : R) :
p.total_degree = p.support.sup (λ (m : σ →₀ ),
theorem mv_polynomial.total_degree_le_degrees_card {R : Type u} {σ : Type u_1} (p : R) :
@[simp]
theorem mv_polynomial.total_degree_C {R : Type u} {σ : Type u_1} (a : R) :
@[simp]
theorem mv_polynomial.total_degree_zero {R : Type u} {σ : Type u_1}  :
@[simp]
theorem mv_polynomial.total_degree_one {R : Type u} {σ : Type u_1}  :
@[simp]
theorem mv_polynomial.total_degree_X {σ : Type u_1} {R : Type u_2} [nontrivial R] (s : σ) :
theorem mv_polynomial.total_degree_add {R : Type u} {σ : Type u_1} (a b : R) :
theorem mv_polynomial.total_degree_mul {R : Type u} {σ : Type u_1} (a b : R) :
theorem mv_polynomial.total_degree_smul_le {R : Type u} {S : Type v} {σ : Type u_1} [ S] (a : R) (f : S) :
theorem mv_polynomial.total_degree_pow {R : Type u} {σ : Type u_1} (a : R) (n : ) :
@[simp]
theorem mv_polynomial.total_degree_monomial {R : Type u} {σ : Type u_1} (s : σ →₀ ) {c : R} (hc : c 0) :
c).total_degree = s.sum (λ (_x : σ) (e : ), e)
@[simp]
theorem mv_polynomial.total_degree_X_pow {R : Type u} {σ : Type u_1} [nontrivial R] (s : σ) (n : ) :
theorem mv_polynomial.total_degree_list_prod {R : Type u} {σ : Type u_1} (s : list R)) :
theorem mv_polynomial.total_degree_multiset_prod {R : Type u} {σ : Type u_1} (s : multiset R)) :
theorem mv_polynomial.total_degree_finset_prod {R : Type u} {σ : Type u_1} {ι : Type u_2} (s : finset ι) (f : ι ) :
(s.prod f).total_degree s.sum (λ (i : ι), (f i).total_degree)
theorem mv_polynomial.total_degree_finset_sum {R : Type u} {σ : Type u_1} {ι : Type u_2} (s : finset ι) (f : ι ) :
(s.sum f).total_degree s.sup (λ (i : ι), (f i).total_degree)
theorem mv_polynomial.exists_degree_lt {R : Type u} {σ : Type u_1} [fintype σ] (f : R) (n : ) (h : f.total_degree < ) {d : σ →₀ } (hd : d f.support) :
(i : σ), d i < n
theorem mv_polynomial.coeff_eq_zero_of_total_degree_lt {R : Type u} {σ : Type u_1} {f : R} {d : σ →₀ } (h : f.total_degree < d.support.sum (λ (i : σ), d i)) :
= 0
theorem mv_polynomial.total_degree_rename_le {R : Type u} {σ : Type u_1} {τ : Type u_2} (f : σ τ) (p : R) :

### vars and eval#

theorem mv_polynomial.eval₂_hom_eq_constant_coeff_of_vars {R : Type u} {S : Type v} {σ : Type u_1} (f : R →+* S) {g : σ S} {p : R} (hp : (i : σ), i p.vars g i = 0) :
p =
theorem mv_polynomial.aeval_eq_constant_coeff_of_vars {R : Type u} {S : Type v} {σ : Type u_1} [ S] {g : σ S} {p : R} (hp : (i : σ), i p.vars g i = 0) :
p =
theorem mv_polynomial.eval₂_hom_congr' {R : Type u} {S : Type v} {σ : Type u_1} {f₁ f₂ : R →+* S} {g₁ g₂ : σ S} {p₁ p₂ : R} :
f₁ = f₂ ( (i : σ), i p₁.vars i p₂.vars g₁ i = g₂ i) p₁ = p₂ g₁) p₁ = g₂) p₂
theorem mv_polynomial.hom_congr_vars {R : Type u} {S : Type v} {σ : Type u_1} {f₁ f₂ : →+* S} {p₁ p₂ : R} (hC : = ) (hv : (i : σ), i p₁.vars i p₂.vars 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 mv_polynomial.exists_rename_eq_of_vars_subset_range {R : Type u} {σ : Type u_1} {τ : Type u_2} (p : R) (f : τ σ) (hfi : function.injective f) (hf : (p.vars) ) :
(q : R), = p
theorem mv_polynomial.vars_rename {R : Type u} {σ : Type u_1} {τ : Type u_2} [decidable_eq τ] (f : σ τ) (φ : R) :
φ).vars φ.vars
theorem mv_polynomial.mem_vars_rename {R : Type u} {σ : Type u_1} {τ : Type u_2} (f : σ τ) (φ : R) {j : τ} (h : j φ).vars) :
(i : σ), i φ.vars f i = j