mathlib documentation

data.mv_polynomial.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

Notation

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

degrees

def mv_polynomial.degrees {R : Type u} {σ : Type u_1} [comm_semiring 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_monomial {R : Type u} {σ : Type u_1} [comm_semiring R] (s : σ →₀ ) (a : R) :

theorem mv_polynomial.degrees_monomial_eq {R : Type u} {σ : Type u_1} [comm_semiring R] (s : σ →₀ ) (a : R) :

theorem mv_polynomial.degrees_C {R : Type u} {σ : Type u_1} [comm_semiring R] (a : R) :

theorem mv_polynomial.degrees_X {R : Type u} {σ : Type u_1} [comm_semiring R] (n : σ) :

theorem mv_polynomial.degrees_zero {R : Type u} {σ : Type u_1} [comm_semiring R] :

theorem mv_polynomial.degrees_one {R : Type u} {σ : Type u_1} [comm_semiring R] :

theorem mv_polynomial.degrees_add {R : Type u} {σ : Type u_1} [comm_semiring R] (p q : mv_polynomial σ R) :

theorem mv_polynomial.degrees_sum {R : Type u} {σ : Type u_1} [comm_semiring R] {ι : Type u_2} (s : finset ι) (f : ι → mv_polynomial σ R) :
(∑ (i : ι) in s, f i).degrees s.sup (λ (i : ι), (f i).degrees)

theorem mv_polynomial.degrees_mul {R : Type u} {σ : Type u_1} [comm_semiring R] (p q : mv_polynomial σ R) :

theorem mv_polynomial.degrees_prod {R : Type u} {σ : Type u_1} [comm_semiring R] {ι : Type u_2} (s : finset ι) (f : ι → mv_polynomial σ R) :
(∏ (i : ι) in s, f i).degrees ∑ (i : ι) in s, (f i).degrees

theorem mv_polynomial.degrees_pow {R : Type u} {σ : Type u_1} [comm_semiring R] (p : mv_polynomial σ R) (n : ) :

theorem mv_polynomial.mem_degrees {R : Type u} {σ : Type u_1} [comm_semiring R] {p : mv_polynomial σ R} {i : σ} :

theorem mv_polynomial.le_degrees_add {R : Type u} {σ : Type u_1} [comm_semiring R] {p q : mv_polynomial σ R} :

theorem mv_polynomial.degrees_add_of_disjoint {R : Type u} {σ : Type u_1} [comm_semiring R] {p q : mv_polynomial σ R} :

theorem mv_polynomial.degrees_map {R : Type u} {S : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S] (p : mv_polynomial σ R) (f : R →+* S) :

theorem mv_polynomial.degrees_rename {R : Type u} {σ : Type u_1} {τ : Type u_2} [comm_semiring R] (f : σ → τ) (φ : mv_polynomial σ R) :

theorem mv_polynomial.degrees_map_of_injective {R : Type u} {S : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S] (p : mv_polynomial σ R) {f : R →+* S} :

vars

def mv_polynomial.vars {R : Type u} {σ : Type u_1} [comm_semiring R] :
mv_polynomial σ Rfinset σ

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

Equations
@[simp]
theorem mv_polynomial.vars_0 {R : Type u} {σ : Type u_1} [comm_semiring R] :

@[simp]
theorem mv_polynomial.vars_monomial {R : Type u} {σ : Type u_1} {r : R} {s : σ →₀ } [comm_semiring R] :

@[simp]
theorem mv_polynomial.vars_C {R : Type u} {σ : Type u_1} {r : R} [comm_semiring R] :

@[simp]
theorem mv_polynomial.vars_X {R : Type u} {σ : Type u_1} {n : σ} [comm_semiring R] [nontrivial R] :

theorem mv_polynomial.mem_vars {R : Type u} {σ : Type u_1} [comm_semiring R] {p : mv_polynomial σ 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} [comm_semiring R] {f : mv_polynomial σ R} {x : σ →₀ } (H : x f.support) {v : σ} :
v f.varsx v = 0

theorem mv_polynomial.vars_add_subset {R : Type u} {σ : Type u_1} [comm_semiring R] (p q : mv_polynomial σ R) :
(p + q).vars p.vars q.vars

theorem mv_polynomial.vars_add_of_disjoint {R : Type u} {σ : Type u_1} [comm_semiring R] {p q : mv_polynomial σ R} :
disjoint p.vars q.vars(p + q).vars = p.vars q.vars

theorem mv_polynomial.vars_mul {R : Type u} {σ : Type u_1} [comm_semiring R] (φ ψ : mv_polynomial σ R) :
* ψ).vars φ.vars ψ.vars

@[simp]
theorem mv_polynomial.vars_one {R : Type u} {σ : Type u_1} [comm_semiring R] :

theorem mv_polynomial.vars_pow {R : Type u} {σ : Type u_1} [comm_semiring R] (φ : mv_polynomial σ R) (n : ) :
^ n).vars φ.vars

theorem mv_polynomial.vars_prod {R : Type u} {σ : Type u_1} [comm_semiring R] {ι : Type u_2} {s : finset ι} (f : ι → mv_polynomial σ R) :
(∏ (i : ι) in s, f i).vars s.bind (λ (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} [integral_domain A] (a : A) (ha : a 0) (φ : mv_polynomial σ A) :

theorem mv_polynomial.vars_sum_subset {R : Type u} {σ : Type u_1} [comm_semiring R] {ι : Type u_3} (t : finset ι) (φ : ι → mv_polynomial σ R) :
(∑ (i : ι) in t, φ i).vars t.bind (λ (i : ι), (φ i).vars)

theorem mv_polynomial.vars_sum_of_disjoint {R : Type u} {σ : Type u_1} [comm_semiring R] {ι : Type u_3} (t : finset ι) (φ : ι → mv_polynomial σ R) :
pairwise (disjoint on λ (i : ι), (φ i).vars)(∑ (i : ι) in t, φ i).vars = t.bind (λ (i : ι), (φ i).vars)

theorem mv_polynomial.vars_map {R : Type u} {S : Type v} {σ : Type u_1} [comm_semiring R] (p : mv_polynomial σ R) [comm_semiring S] (f : R →+* S) :

theorem mv_polynomial.vars_map_of_injective {R : Type u} {S : Type v} {σ : Type u_1} [comm_semiring R] (p : mv_polynomial σ R) [comm_semiring S] {f : R →+* S} :

theorem mv_polynomial.vars_monomial_single {R : Type u} {σ : Type u_1} [comm_semiring R] (i : σ) {e : } {r : R} :
e 0r 0(mv_polynomial.monomial (finsupp.single i e) r).vars = {i}

degree_of

def mv_polynomial.degree_of {R : Type u} {σ : Type u_1} [comm_semiring R] :
σ → mv_polynomial σ R

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

Equations

total_degree

def mv_polynomial.total_degree {R : Type u} {σ : Type u_1} [comm_semiring 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} [comm_semiring R] (p : mv_polynomial σ R) :

theorem mv_polynomial.total_degree_le_degrees_card {R : Type u} {σ : Type u_1} [comm_semiring R] (p : mv_polynomial σ R) :

@[simp]
theorem mv_polynomial.total_degree_C {R : Type u} {σ : Type u_1} [comm_semiring R] (a : R) :

@[simp]
theorem mv_polynomial.total_degree_zero {R : Type u} {σ : Type u_1} [comm_semiring R] :

@[simp]
theorem mv_polynomial.total_degree_one {R : Type u} {σ : Type u_1} [comm_semiring R] :

@[simp]
theorem mv_polynomial.total_degree_X {σ : Type u_1} {R : Type u_2} [comm_semiring R] [nontrivial R] (s : σ) :

theorem mv_polynomial.total_degree_add {R : Type u} {σ : Type u_1} [comm_semiring R] (a b : mv_polynomial σ R) :

theorem mv_polynomial.total_degree_mul {R : Type u} {σ : Type u_1} [comm_semiring R] (a b : mv_polynomial σ R) :

theorem mv_polynomial.total_degree_pow {R : Type u} {σ : Type u_1} [comm_semiring R] (a : mv_polynomial σ R) (n : ) :

theorem mv_polynomial.total_degree_finset_prod {R : Type u} {σ : Type u_1} [comm_semiring R] {ι : Type u_2} (s : finset ι) (f : ι → mv_polynomial σ R) :
(s.prod f).total_degree ∑ (i : ι) in s, (f i).total_degree

theorem mv_polynomial.exists_degree_lt {R : Type u} {σ : Type u_1} [comm_semiring R] [fintype σ] (f : mv_polynomial σ R) (n : ) (h : f.total_degree < n * fintype.card σ) {d : σ →₀ } :
d f.support(∃ (i : σ), d i < n)

theorem mv_polynomial.coeff_eq_zero_of_total_degree_lt {R : Type u} {σ : Type u_1} [comm_semiring R] {f : mv_polynomial σ R} {d : σ →₀ } :
f.total_degree < ∑ (i : σ) in d.support, d imv_polynomial.coeff d f = 0

theorem mv_polynomial.total_degree_rename_le {R : Type u} {σ : Type u_1} {τ : Type u_2} [comm_semiring R] (f : σ → τ) (p : mv_polynomial σ R) :

vars and eval

theorem mv_polynomial.eval₂_hom_eq_constant_coeff_of_vars {R : Type u} {S : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S] (f : R →+* S) {g : σ → S} {p : mv_polynomial σ R} :
(∀ (i : σ), i p.varsg i = 0)(mv_polynomial.eval₂_hom f g) p = f (mv_polynomial.constant_coeff p)

theorem mv_polynomial.aeval_eq_constant_coeff_of_vars {R : Type u} {S : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S] [algebra R S] {g : σ → S} {p : mv_polynomial σ R} :
(∀ (i : σ), i p.varsg i = 0)(mv_polynomial.aeval g) p = (algebra_map R S) (mv_polynomial.constant_coeff p)

theorem mv_polynomial.eval₂_hom_congr' {R : Type u} {S : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S] {f₁ f₂ : R →+* S} {g₁ g₂ : σ → S} {p₁ p₂ : mv_polynomial σ R} :
f₁ = f₂(∀ (i : σ), i p₁.varsi p₂.varsg₁ i = g₂ i)p₁ = p₂(mv_polynomial.eval₂_hom f₁ g₁) p₁ = (mv_polynomial.eval₂_hom f₂ g₂) p₂

theorem mv_polynomial.vars_bind₁ {R : Type u} {σ : Type u_1} {τ : Type u_2} [comm_semiring R] (f : σ → mv_polynomial τ R) (φ : mv_polynomial σ R) :
((mv_polynomial.bind₁ f) φ).vars φ.vars.bind (λ (i : σ), (f i).vars)

theorem mv_polynomial.mem_vars_bind₁ {R : Type u} {σ : Type u_1} {τ : Type u_2} [comm_semiring R] (f : σ → mv_polynomial τ R) (φ : mv_polynomial σ R) {j : τ} :
j ((mv_polynomial.bind₁ f) φ).vars(∃ (i : σ), i φ.vars j (f i).vars)

theorem mv_polynomial.vars_rename {R : Type u} {σ : Type u_1} {τ : Type u_2} [comm_semiring R] (f : σ → τ) (φ : mv_polynomial σ R) :

theorem mv_polynomial.mem_vars_rename {R : Type u} {σ : Type u_1} {τ : Type u_2} [comm_semiring R] (f : σ → τ) (φ : mv_polynomial σ R) {j : τ} :
j ((mv_polynomial.rename f) φ).vars(∃ (i : σ), i φ.vars f i = j)