# Variables of polynomials #

This file establishes many results about the 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$.

## Main declarations #

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

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

### vars#

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

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

Equations
• p.vars = p.degrees.toFinset
Instances For
theorem MvPolynomial.vars_def {R : Type u} {σ : Type u_1} [] [] (p : ) :
p.vars = p.degrees.toFinset
@[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) :
( r).vars = s.support
@[simp]
theorem MvPolynomial.vars_C {R : Type u} {σ : Type u_1} {r : R} [] :
(MvPolynomial.C r).vars =
@[simp]
theorem MvPolynomial.vars_X {R : Type u} {σ : Type u_1} {n : σ} [] [] :
.vars = {n}
theorem MvPolynomial.mem_vars {R : Type u} {σ : Type u_1} [] {p : } (i : σ) :
i p.vars dp.support, i d.support
theorem MvPolynomial.mem_support_not_mem_vars_zero {R : Type u} {σ : Type u_1} [] {f : } {x : σ →₀ } (H : x f.support) {v : σ} (h : vf.vars) :
x v = 0
theorem MvPolynomial.vars_add_subset {R : Type u} {σ : Type u_1} [] [] (p : ) (q : ) :
(p + q).vars p.vars q.vars
theorem MvPolynomial.vars_add_of_disjoint {R : Type u} {σ : Type u_1} [] {p : } {q : } [] (h : Disjoint p.vars q.vars) :
(p + q).vars = p.vars q.vars
theorem MvPolynomial.vars_mul {R : Type u} {σ : Type u_1} [] [] (φ : ) (ψ : ) :
(φ * ψ).vars φ.vars ψ.vars
@[simp]
theorem MvPolynomial.vars_one {R : Type u} {σ : Type u_1} [] :
theorem MvPolynomial.vars_pow {R : Type u} {σ : Type u_1} [] (φ : ) (n : ) :
(φ ^ n).vars φ.vars
theorem MvPolynomial.vars_prod {R : Type u} {σ : Type u_1} [] {ι : Type u_3} [] {s : } (f : ι) :
(∏ is, f i).vars s.biUnion fun (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 MvPolynomial.vars_C_mul {σ : Type u_1} {A : Type u_3} [] [] (a : A) (ha : a 0) (φ : ) :
(MvPolynomial.C a * φ).vars = φ.vars
theorem MvPolynomial.vars_sum_subset {R : Type u} {σ : Type u_1} [] {ι : Type u_3} (t : ) (φ : ι) [] :
(∑ it, φ i).vars t.biUnion fun (i : ι) => (φ i).vars
theorem MvPolynomial.vars_sum_of_disjoint {R : Type u} {σ : Type u_1} [] {ι : Type u_3} (t : ) (φ : ι) [] (h : Pairwise (Disjoint on fun (i : ι) => (φ i).vars)) :
(∑ it, φ i).vars = t.biUnion fun (i : ι) => (φ i).vars
theorem MvPolynomial.vars_map {R : Type u} {S : Type v} {σ : Type u_1} [] (p : ) [] (f : R →+* S) :
( p).vars p.vars
theorem MvPolynomial.vars_map_of_injective {R : Type u} {S : Type v} {σ : Type u_1} [] (p : ) [] {f : R →+* S} (hf : ) :
( p).vars = p.vars
theorem MvPolynomial.vars_monomial_single {R : Type u} {σ : Type u_1} [] (i : σ) {e : } {r : R} (he : e 0) (hr : r 0) :
( r).vars = {i}
theorem MvPolynomial.vars_eq_support_biUnion_support {R : Type u} {σ : Type u_1} [] (p : ) [] :
p.vars = p.support.biUnion Finsupp.support

### 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 : ip.vars, 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 : ip.vars, g i = 0) :
p = (algebraMap R 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₂(∀ ip₁.vars, i p₂.varsg₁ i = g₂ i)p₁ = p₂(MvPolynomial.eval₂Hom f₁ g₁) p₁ = (MvPolynomial.eval₂Hom f₂ g₂) p₂
theorem MvPolynomial.hom_congr_vars {R : Type u} {S : Type v} {σ : Type u_1} [] [] {f₁ : →+* S} {f₂ : →+* S} {p₁ : } {p₂ : } (hC : f₁.comp MvPolynomial.C = f₂.comp MvPolynomial.C) (hv : ip₁.vars, i p₂.varsf₁ = 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 : p.vars ) :
∃ (q : ), q = p
theorem MvPolynomial.vars_rename {R : Type u} {σ : Type u_1} {τ : Type u_2} [] [] (f : στ) (φ : ) :
( φ).vars Finset.image f φ.vars
theorem MvPolynomial.mem_vars_rename {R : Type u} {σ : Type u_1} {τ : Type u_2} [] (f : στ) (φ : ) {j : τ} (h : j ( φ).vars) :
iφ.vars, f i = j
theorem MvPolynomial.leadingCoeff_toLex {R : Type u} {σ : Type u_1} [] {p : } [] :
theorem MvPolynomial.supDegree_toLex_C {R : Type u} {σ : Type u_1} [] [] (r : R) :
AddMonoidAlgebra.supDegree (⇑toLex) (MvPolynomial.C r) = 0
theorem MvPolynomial.leadingCoeff_toLex_C {R : Type u} {σ : Type u_1} [] [] (r : R) :