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

source

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

Multiset σ

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

MvPolynomial.degrees p = Finset.sup (MvPolynomial.support p) fun (s : σ →₀ ℕ) => Finsupp.toMultiset s

Instances For

source

theorem MvPolynomial.degrees_def {R : Type u} {σ : Type u_1} [CommSemiring R] [DecidableEq σ] (p : MvPolynomial σ R) :

MvPolynomial.degrees p = Finset.sup (MvPolynomial.support p) fun (s : σ →₀ ℕ) => Finsupp.toMultiset s

source

theorem MvPolynomial.degrees_monomial {R : Type u} {σ : Type u_1} [CommSemiring R] (s : σ →₀ ℕ) (a : R) :

MvPolynomial.degrees ((MvPolynomial.monomial s) a) ≤ Finsupp.toMultiset s

source

theorem MvPolynomial.degrees_monomial_eq {R : Type u} {σ : Type u_1} [CommSemiring R] (s : σ →₀ ℕ) (a : R) (ha : a ≠ 0) :

MvPolynomial.degrees ((MvPolynomial.monomial s) a) = Finsupp.toMultiset s

source

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

MvPolynomial.degrees (MvPolynomial.C a) = 0

source

theorem MvPolynomial.degrees_X' {R : Type u} {σ : Type u_1} [CommSemiring R] (n : σ) :

MvPolynomial.degrees (MvPolynomial.X n) ≤ {n}

source

@[simp]

theorem MvPolynomial.degrees_X {R : Type u} {σ : Type u_1} [CommSemiring R] [Nontrivial R] (n : σ) :

MvPolynomial.degrees (MvPolynomial.X n) = {n}

source

@[simp]

theorem MvPolynomial.degrees_zero {R : Type u} {σ : Type u_1} [CommSemiring R] :

MvPolynomial.degrees 0 = 0

source

@[simp]

theorem MvPolynomial.degrees_one {R : Type u} {σ : Type u_1} [CommSemiring R] :

MvPolynomial.degrees 1 = 0

source

theorem MvPolynomial.degrees_add {R : Type u} {σ : Type u_1} [CommSemiring R] [DecidableEq σ] (p : MvPolynomial σ R) (q : MvPolynomial σ R) :

MvPolynomial.degrees (p + q) ≤ MvPolynomial.degrees p ⊔ MvPolynomial.degrees q

source

theorem MvPolynomial.degrees_sum {R : Type u} {σ : Type u_1} [CommSemiring R] {ι : Type u_3} [DecidableEq σ] (s : Finset ι) (f : ι → MvPolynomial σ R) :

MvPolynomial.degrees (Finset.sum s fun (i : ι) => f i) ≤ Finset.sup s fun (i : ι) => MvPolynomial.degrees (f i)

source

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

MvPolynomial.degrees (p * q) ≤ MvPolynomial.degrees p + MvPolynomial.degrees q

source

theorem MvPolynomial.degrees_prod {R : Type u} {σ : Type u_1} [CommSemiring R] {ι : Type u_3} (s : Finset ι) (f : ι → MvPolynomial σ R) :

MvPolynomial.degrees (Finset.prod s fun (i : ι) => f i) ≤ Finset.sum s fun (i : ι) => MvPolynomial.degrees (f i)

source

theorem MvPolynomial.degrees_pow {R : Type u} {σ : Type u_1} [CommSemiring R] (p : MvPolynomial σ R) (n : ℕ) :

MvPolynomial.degrees (p ^ n) ≤ n • MvPolynomial.degrees p

source

theorem MvPolynomial.mem_degrees {R : Type u} {σ : Type u_1} [CommSemiring R] {p : MvPolynomial σ R} {i : σ} :

i ∈ MvPolynomial.degrees p ↔ ∃ (d : σ →₀ ℕ), MvPolynomial.coeff d p ≠ 0 ∧ i ∈ d.support

source

theorem MvPolynomial.le_degrees_add {R : Type u} {σ : Type u_1} [CommSemiring R] {p : MvPolynomial σ R} {q : MvPolynomial σ R} (h : Multiset.Disjoint (MvPolynomial.degrees p) (MvPolynomial.degrees q)) :

MvPolynomial.degrees p ≤ MvPolynomial.degrees (p + q)

source

theorem MvPolynomial.degrees_add_of_disjoint {R : Type u} {σ : Type u_1} [CommSemiring R] [DecidableEq σ] {p : MvPolynomial σ R} {q : MvPolynomial σ R} (h : Multiset.Disjoint (MvPolynomial.degrees p) (MvPolynomial.degrees q)) :

MvPolynomial.degrees (p + q) = MvPolynomial.degrees p ∪ MvPolynomial.degrees q

source

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

MvPolynomial.degrees ((MvPolynomial.map f) p) ⊆ MvPolynomial.degrees p

source

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

MvPolynomial.degrees ((MvPolynomial.rename f) φ) ⊆ Multiset.map f (MvPolynomial.degrees φ)

source

theorem MvPolynomial.degrees_map_of_injective {R : Type u} {S : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S] (p : MvPolynomial σ R) {f : R →+* S} (hf : Function.Injective ⇑f) :

MvPolynomial.degrees ((MvPolynomial.map f) p) = MvPolynomial.degrees p

source

theorem MvPolynomial.degrees_rename_of_injective {R : Type u} {σ : Type u_1} {τ : Type u_2} [CommSemiring R] {p : MvPolynomial σ R} {f : σ → τ} (h : Function.Injective f) :

MvPolynomial.degrees ((MvPolynomial.rename f) p) = Multiset.map f (MvPolynomial.degrees p)

`vars` #

source

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

Finset σ

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

Equations

MvPolynomial.vars p = Multiset.toFinset (MvPolynomial.degrees p)

Instances For

source

theorem MvPolynomial.vars_def {R : Type u} {σ : Type u_1} [CommSemiring R] [DecidableEq σ] (p : MvPolynomial σ R) :

MvPolynomial.vars p = Multiset.toFinset (MvPolynomial.degrees p)

source

@[simp]

theorem MvPolynomial.vars_0 {R : Type u} {σ : Type u_1} [CommSemiring R] :

MvPolynomial.vars 0 = ∅

source

@[simp]

theorem MvPolynomial.vars_monomial {R : Type u} {σ : Type u_1} {r : R} {s : σ →₀ ℕ} [CommSemiring R] (h : r ≠ 0) :

MvPolynomial.vars ((MvPolynomial.monomial s) r) = s.support

source

@[simp]

theorem MvPolynomial.vars_C {R : Type u} {σ : Type u_1} {r : R} [CommSemiring R] :

MvPolynomial.vars (MvPolynomial.C r) = ∅

source

@[simp]

theorem MvPolynomial.vars_X {R : Type u} {σ : Type u_1} {n : σ} [CommSemiring R] [Nontrivial R] :

MvPolynomial.vars (MvPolynomial.X n) = {n}

source

theorem MvPolynomial.mem_vars {R : Type u} {σ : Type u_1} [CommSemiring R] {p : MvPolynomial σ R} (i : σ) :

i ∈ MvPolynomial.vars p ↔ ∃ d ∈ MvPolynomial.support p, i ∈ d.support

source

theorem MvPolynomial.mem_support_not_mem_vars_zero {R : Type u} {σ : Type u_1} [CommSemiring R] {f : MvPolynomial σ R} {x : σ →₀ ℕ} (H : x ∈ MvPolynomial.support f) {v : σ} (h : v ∉ MvPolynomial.vars f) :

x v = 0

source

theorem MvPolynomial.vars_add_subset {R : Type u} {σ : Type u_1} [CommSemiring R] [DecidableEq σ] (p : MvPolynomial σ R) (q : MvPolynomial σ R) :

MvPolynomial.vars (p + q) ⊆ MvPolynomial.vars p ∪ MvPolynomial.vars q

source

theorem MvPolynomial.vars_add_of_disjoint {R : Type u} {σ : Type u_1} [CommSemiring R] {p : MvPolynomial σ R} {q : MvPolynomial σ R} [DecidableEq σ] (h : Disjoint (MvPolynomial.vars p) (MvPolynomial.vars q)) :

MvPolynomial.vars (p + q) = MvPolynomial.vars p ∪ MvPolynomial.vars q

source

theorem MvPolynomial.vars_mul {R : Type u} {σ : Type u_1} [CommSemiring R] [DecidableEq σ] (φ : MvPolynomial σ R) (ψ : MvPolynomial σ R) :

MvPolynomial.vars (φ * ψ) ⊆ MvPolynomial.vars φ ∪ MvPolynomial.vars ψ

source

@[simp]

theorem MvPolynomial.vars_one {R : Type u} {σ : Type u_1} [CommSemiring R] :

MvPolynomial.vars 1 = ∅

source

theorem MvPolynomial.vars_pow {R : Type u} {σ : Type u_1} [CommSemiring R] (φ : MvPolynomial σ R) (n : ℕ) :

MvPolynomial.vars (φ ^ n) ⊆ MvPolynomial.vars φ

source

theorem MvPolynomial.vars_prod {R : Type u} {σ : Type u_1} [CommSemiring R] {ι : Type u_3} [DecidableEq σ] {s : Finset ι} (f : ι → MvPolynomial σ R) :

MvPolynomial.vars (Finset.prod s fun (i : ι) => f i) ⊆ Finset.biUnion s fun (i : ι) => MvPolynomial.vars (f i)

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

source

theorem MvPolynomial.vars_C_mul {σ : Type u_1} {A : Type u_3} [CommRing A] [IsDomain A] (a : A) (ha : a ≠ 0) (φ : MvPolynomial σ A) :

MvPolynomial.vars (MvPolynomial.C a * φ) = MvPolynomial.vars φ

source

theorem MvPolynomial.vars_sum_subset {R : Type u} {σ : Type u_1} [CommSemiring R] {ι : Type u_3} (t : Finset ι) (φ : ι → MvPolynomial σ R) [DecidableEq σ] :

MvPolynomial.vars (Finset.sum t fun (i : ι) => φ i) ⊆ Finset.biUnion t fun (i : ι) => MvPolynomial.vars (φ i)

source

theorem MvPolynomial.vars_sum_of_disjoint {R : Type u} {σ : Type u_1} [CommSemiring R] {ι : Type u_3} (t : Finset ι) (φ : ι → MvPolynomial σ R) [DecidableEq σ] (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)

source

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

MvPolynomial.vars ((MvPolynomial.map f) p) ⊆ MvPolynomial.vars p

source

theorem MvPolynomial.vars_map_of_injective {R : Type u} {S : Type v} {σ : Type u_1} [CommSemiring R] (p : MvPolynomial σ R) [CommSemiring S] {f : R →+* S} (hf : Function.Injective ⇑f) :

MvPolynomial.vars ((MvPolynomial.map f) p) = MvPolynomial.vars p

source

theorem MvPolynomial.vars_monomial_single {R : Type u} {σ : Type u_1} [CommSemiring R] (i : σ) {e : ℕ} {r : R} (he : e ≠ 0) (hr : r ≠ 0) :

MvPolynomial.vars ((MvPolynomial.monomial (Finsupp.single i e)) r) = {i}

source

theorem MvPolynomial.vars_eq_support_biUnion_support {R : Type u} {σ : Type u_1} [CommSemiring R] (p : MvPolynomial σ R) [DecidableEq σ] :

MvPolynomial.vars p = Finset.biUnion (MvPolynomial.support p) Finsupp.support

`degreeOf` #

source

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

ℕ

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

Equations

MvPolynomial.degreeOf n p = Multiset.count n (MvPolynomial.degrees p)

Instances For

source

theorem MvPolynomial.degreeOf_def {R : Type u} {σ : Type u_1} [CommSemiring R] [DecidableEq σ] (n : σ) (p : MvPolynomial σ R) :

MvPolynomial.degreeOf n p = Multiset.count n (MvPolynomial.degrees p)

source

theorem MvPolynomial.degreeOf_eq_sup {R : Type u} {σ : Type u_1} [CommSemiring R] (n : σ) (f : MvPolynomial σ R) :

MvPolynomial.degreeOf n f = Finset.sup (MvPolynomial.support f) fun (m : σ →₀ ℕ) => m n

source

theorem MvPolynomial.degreeOf_lt_iff {R : Type u} {σ : Type u_1} [CommSemiring R] {n : σ} {f : MvPolynomial σ R} {d : ℕ} (h : 0 < d) :

MvPolynomial.degreeOf n f < d ↔ ∀ m ∈ MvPolynomial.support f, m n < d

source

theorem MvPolynomial.degreeOf_le_iff {R : Type u} {σ : Type u_1} [CommSemiring R] {n : σ} {f : MvPolynomial σ R} {d : ℕ} :

MvPolynomial.degreeOf n f ≤ d ↔ ∀ m ∈ MvPolynomial.support f, m n ≤ d

source

@[simp]

theorem MvPolynomial.degreeOf_zero {R : Type u} {σ : Type u_1} [CommSemiring R] (n : σ) :

MvPolynomial.degreeOf n 0 = 0

source

@[simp]

theorem MvPolynomial.degreeOf_C {R : Type u} {σ : Type u_1} [CommSemiring R] (a : R) (x : σ) :

MvPolynomial.degreeOf x (MvPolynomial.C a) = 0

source

theorem MvPolynomial.degreeOf_X {R : Type u} {σ : Type u_1} [CommSemiring R] [DecidableEq σ] (i : σ) (j : σ) [Nontrivial R] :

MvPolynomial.degreeOf i (MvPolynomial.X j) = if i = j then 1 else 0

source

theorem MvPolynomial.degreeOf_add_le {R : Type u} {σ : Type u_1} [CommSemiring R] (n : σ) (f : MvPolynomial σ R) (g : MvPolynomial σ R) :

MvPolynomial.degreeOf n (f + g) ≤ max (MvPolynomial.degreeOf n f) (MvPolynomial.degreeOf n g)

source

theorem MvPolynomial.monomial_le_degreeOf {R : Type u} {σ : Type u_1} [CommSemiring R] (i : σ) {f : MvPolynomial σ R} {m : σ →₀ ℕ} (h_m : m ∈ MvPolynomial.support f) :

m i ≤ MvPolynomial.degreeOf i f

source

theorem MvPolynomial.degreeOf_mul_le {R : Type u} {σ : Type u_1} [CommSemiring R] (i : σ) (f : MvPolynomial σ R) (g : MvPolynomial σ R) :

MvPolynomial.degreeOf i (f * g) ≤ MvPolynomial.degreeOf i f + MvPolynomial.degreeOf i g

source

theorem MvPolynomial.degreeOf_mul_X_ne {R : Type u} {σ : Type u_1} [CommSemiring R] {i : σ} {j : σ} (f : MvPolynomial σ R) (h : i ≠ j) :

MvPolynomial.degreeOf i (f * MvPolynomial.X j) = MvPolynomial.degreeOf i f

source

theorem MvPolynomial.degreeOf_mul_X_eq {R : Type u} {σ : Type u_1} [CommSemiring R] (j : σ) (f : MvPolynomial σ R) :

MvPolynomial.degreeOf j (f * MvPolynomial.X j) ≤ MvPolynomial.degreeOf j f + 1

source

theorem MvPolynomial.degreeOf_rename_of_injective {R : Type u} {σ : Type u_1} {τ : Type u_2} [CommSemiring R] {p : MvPolynomial σ R} {f : σ → τ} (h : Function.Injective f) (i : σ) :

MvPolynomial.degreeOf (f i) ((MvPolynomial.rename f) p) = MvPolynomial.degreeOf i p

`totalDegree` #

source

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

ℕ

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

Equations

MvPolynomial.totalDegree p = Finset.sup (MvPolynomial.support p) fun (s : σ →₀ ℕ) => Finsupp.sum s fun (x : σ) (e : ℕ) => e

Instances For

source

theorem MvPolynomial.totalDegree_eq {R : Type u} {σ : Type u_1} [CommSemiring R] (p : MvPolynomial σ R) :

MvPolynomial.totalDegree p = Finset.sup (MvPolynomial.support p) fun (m : σ →₀ ℕ) => Multiset.card (Finsupp.toMultiset m)

source

theorem MvPolynomial.le_totalDegree {R : Type u} {σ : Type u_1} [CommSemiring R] {p : MvPolynomial σ R} {s : σ →₀ ℕ} (h : s ∈ MvPolynomial.support p) :

(Finsupp.sum s fun (x : σ) (e : ℕ) => e) ≤ MvPolynomial.totalDegree p

source

theorem MvPolynomial.totalDegree_le_degrees_card {R : Type u} {σ : Type u_1} [CommSemiring R] (p : MvPolynomial σ R) :

MvPolynomial.totalDegree p ≤ Multiset.card (MvPolynomial.degrees p)

source

theorem MvPolynomial.totalDegree_le_of_support_subset {R : Type u} {σ : Type u_1} [CommSemiring R] {p : MvPolynomial σ R} {q : MvPolynomial σ R} (h : MvPolynomial.support p ⊆ MvPolynomial.support q) :

MvPolynomial.totalDegree p ≤ MvPolynomial.totalDegree q

source

@[simp]

theorem MvPolynomial.totalDegree_C {R : Type u} {σ : Type u_1} [CommSemiring R] (a : R) :

MvPolynomial.totalDegree (MvPolynomial.C a) = 0

source

@[simp]

theorem MvPolynomial.totalDegree_zero {R : Type u} {σ : Type u_1} [CommSemiring R] :

MvPolynomial.totalDegree 0 = 0

source

@[simp]

theorem MvPolynomial.totalDegree_one {R : Type u} {σ : Type u_1} [CommSemiring R] :

MvPolynomial.totalDegree 1 = 0

source

@[simp]

theorem MvPolynomial.totalDegree_X {σ : Type u_1} {R : Type u_3} [CommSemiring R] [Nontrivial R] (s : σ) :

MvPolynomial.totalDegree (MvPolynomial.X s) = 1

source

theorem MvPolynomial.totalDegree_add {R : Type u} {σ : Type u_1} [CommSemiring R] (a : MvPolynomial σ R) (b : MvPolynomial σ R) :

MvPolynomial.totalDegree (a + b) ≤ max (MvPolynomial.totalDegree a) (MvPolynomial.totalDegree b)

source

theorem MvPolynomial.totalDegree_add_eq_left_of_totalDegree_lt {R : Type u} {σ : Type u_1} [CommSemiring R] {p : MvPolynomial σ R} {q : MvPolynomial σ R} (h : MvPolynomial.totalDegree q < MvPolynomial.totalDegree p) :

MvPolynomial.totalDegree (p + q) = MvPolynomial.totalDegree p

source

theorem MvPolynomial.totalDegree_add_eq_right_of_totalDegree_lt {R : Type u} {σ : Type u_1} [CommSemiring R] {p : MvPolynomial σ R} {q : MvPolynomial σ R} (h : MvPolynomial.totalDegree q < MvPolynomial.totalDegree p) :

MvPolynomial.totalDegree (q + p) = MvPolynomial.totalDegree p

source

theorem MvPolynomial.totalDegree_mul {R : Type u} {σ : Type u_1} [CommSemiring R] (a : MvPolynomial σ R) (b : MvPolynomial σ R) :

MvPolynomial.totalDegree (a * b) ≤ MvPolynomial.totalDegree a + MvPolynomial.totalDegree b

source

theorem MvPolynomial.totalDegree_smul_le {R : Type u} {S : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S] [DistribMulAction R S] (a : R) (f : MvPolynomial σ S) :

MvPolynomial.totalDegree (a • f) ≤ MvPolynomial.totalDegree f

source

theorem MvPolynomial.totalDegree_pow {R : Type u} {σ : Type u_1} [CommSemiring R] (a : MvPolynomial σ R) (n : ℕ) :

MvPolynomial.totalDegree (a ^ n) ≤ n * MvPolynomial.totalDegree a

source

@[simp]

theorem MvPolynomial.totalDegree_monomial {R : Type u} {σ : Type u_1} [CommSemiring R] (s : σ →₀ ℕ) {c : R} (hc : c ≠ 0) :

MvPolynomial.totalDegree ((MvPolynomial.monomial s) c) = Finsupp.sum s fun (x : σ) (e : ℕ) => e

source

@[simp]

theorem MvPolynomial.totalDegree_X_pow {R : Type u} {σ : Type u_1} [CommSemiring R] [Nontrivial R] (s : σ) (n : ℕ) :

MvPolynomial.totalDegree (MvPolynomial.X s ^ n) = n

source

theorem MvPolynomial.totalDegree_list_prod {R : Type u} {σ : Type u_1} [CommSemiring R] (s : List (MvPolynomial σ R)) :

MvPolynomial.totalDegree (List.prod s) ≤ List.sum (List.map MvPolynomial.totalDegree s)

source

theorem MvPolynomial.totalDegree_multiset_prod {R : Type u} {σ : Type u_1} [CommSemiring R] (s : Multiset (MvPolynomial σ R)) :

MvPolynomial.totalDegree (Multiset.prod s) ≤ Multiset.sum (Multiset.map MvPolynomial.totalDegree s)

source

theorem MvPolynomial.totalDegree_finset_prod {R : Type u} {σ : Type u_1} [CommSemiring R] {ι : Type u_3} (s : Finset ι) (f : ι → MvPolynomial σ R) :

MvPolynomial.totalDegree (Finset.prod s f) ≤ Finset.sum s fun (i : ι) => MvPolynomial.totalDegree (f i)

source

theorem MvPolynomial.totalDegree_finset_sum {R : Type u} {σ : Type u_1} [CommSemiring R] {ι : Type u_3} (s : Finset ι) (f : ι → MvPolynomial σ R) :

MvPolynomial.totalDegree (Finset.sum s f) ≤ Finset.sup s fun (i : ι) => MvPolynomial.totalDegree (f i)

source

theorem MvPolynomial.degreeOf_le_totalDegree {R : Type u} {σ : Type u_1} [CommSemiring R] (f : MvPolynomial σ R) (i : σ) :

MvPolynomial.degreeOf i f ≤ MvPolynomial.totalDegree f

source

theorem MvPolynomial.exists_degree_lt {R : Type u} {σ : Type u_1} [CommSemiring R] [Fintype σ] (f : MvPolynomial σ R) (n : ℕ) (h : MvPolynomial.totalDegree f < n * Fintype.card σ) {d : σ →₀ ℕ} (hd : d ∈ MvPolynomial.support f) :

∃ (i : σ), d i < n

source

theorem MvPolynomial.coeff_eq_zero_of_totalDegree_lt {R : Type u} {σ : Type u_1} [CommSemiring R] {f : MvPolynomial σ R} {d : σ →₀ ℕ} (h : MvPolynomial.totalDegree f < Finset.sum d.support fun (i : σ) => d i) :

MvPolynomial.coeff d f = 0

source

theorem MvPolynomial.totalDegree_rename_le {R : Type u} {σ : Type u_1} {τ : Type u_2} [CommSemiring R] (f : σ → τ) (p : MvPolynomial σ R) :

MvPolynomial.totalDegree ((MvPolynomial.rename f) p) ≤ MvPolynomial.totalDegree p

`vars` and `eval` #

source

theorem MvPolynomial.eval₂Hom_eq_constantCoeff_of_vars {R : Type u} {S : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S] (f : R →+* S) {g : σ → S} {p : MvPolynomial σ R} (hp : ∀ i ∈ MvPolynomial.vars p, g i = 0) :

(MvPolynomial.eval₂Hom f g) p = f (MvPolynomial.constantCoeff p)

source

theorem MvPolynomial.aeval_eq_constantCoeff_of_vars {R : Type u} {S : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S] [Algebra R S] {g : σ → S} {p : MvPolynomial σ R} (hp : ∀ i ∈ MvPolynomial.vars p, g i = 0) :

(MvPolynomial.aeval g) p = (algebraMap R S) (MvPolynomial.constantCoeff p)

source

theorem MvPolynomial.eval₂Hom_congr' {R : Type u} {S : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S] {f₁ : R →+* S} {f₂ : R →+* S} {g₁ : σ → S} {g₂ : σ → S} {p₁ : MvPolynomial σ R} {p₂ : MvPolynomial σ R} :

f₁ = f₂ → (∀ i ∈ MvPolynomial.vars p₁, i ∈ MvPolynomial.vars p₂ → g₁ i = g₂ i) → p₁ = p₂ → (MvPolynomial.eval₂Hom f₁ g₁) p₁ = (MvPolynomial.eval₂Hom f₂ g₂) p₂

source

theorem MvPolynomial.hom_congr_vars {R : Type u} {S : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S] {f₁ : MvPolynomial σ R →+* S} {f₂ : MvPolynomial σ R →+* S} {p₁ : MvPolynomial σ R} {p₂ : MvPolynomial σ R} (hC : RingHom.comp f₁ MvPolynomial.C = RingHom.comp f₂ MvPolynomial.C) (hv : ∀ i ∈ MvPolynomial.vars p₁, i ∈ MvPolynomial.vars p₂ → f₁ (MvPolynomial.X i) = f₂ (MvPolynomial.X i)) (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₁.

source