mathlib documentation

data.mv_polynomial.basic

Multivariate polynomials

This file defines polynomial rings over a base ring (or even semiring), with variables from a general type σ (which could be infinite).

Important definitions

Let R be a commutative ring (or a semiring) and let σ be an arbitrary type. This file creates the type mv_polynomial σ R, which mathematicians might denote $R[X_i : i \in σ]$. It is the type of multivariate (a.k.a. multivariable) polynomials, with variables corresponding to the terms in σ, and coefficients in R.

Notation

In the definitions below, we use the following 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
a : R
i : σ, with corresponding monomial X i, often denoted X_i by mathematicians
p : mv_polynomial σ R

Definitions

mv_polynomial σ R : the type of polynomials with variables of type σ and coefficients in the commutative semiring R
monomial s a : the monomial which mathematically would be denoted a * X^s
C a : the constant polynomial with value a
X i : the degree one monomial corresponding to i; mathematically this might be denoted Xᵢ.
coeff s p : the coefficient of s in p.
eval₂ (f : R → S₁) (g : σ → S₁) p : given a semiring homomorphism from R to another semiring S₁, and a map σ → S₁, evaluates p at this valuation, returning a term of type S₁. Note that eval₂ can be made using eval and map (see below), and it has been suggested that sticking to eval and map might make the code less brittle.
eval (g : σ → R) p : given a map σ → R, evaluates p at this valuation, returning a term of type R
map (f : R → S₁) p : returns the multivariate polynomial obtained from p by the change of coefficient semiring corresponding to f

Implementation notes

Recall that if Y has a zero, then X →₀ Y is the type of functions from X to Y with finite support, i.e. such that only finitely many elements of X get sent to non-zero terms in Y. The definition of mv_polynomial σ R is (σ →₀ ℕ) →₀ R ; here σ →₀ ℕ denotes the space of all monomials in the variables, and the function to R sends a monomial to its coefficient in the polynomial being represented.

Tags

polynomial, multivariate polynomial, multivariable polynomial

S₁ S₂ S₃

def mv_polynomial (σ : Type u_1) (R : Type u_2) [comm_semiring R] :

Type (max u_1 u_2)

Multivariate polynomial, where σ is the index set of the variables and R is the coefficient ring

Equations

mv_polynomial σ R = add_monoid_algebra R (σ →₀ ℕ)

@[instance]

def mv_polynomial.decidable_eq_mv_polynomial {R : Type u} {σ : Type u_1} [comm_semiring R] [decidable_eq σ] [decidable_eq R] :

decidable_eq (mv_polynomial σ R)

Equations

mv_polynomial.decidable_eq_mv_polynomial = finsupp.finsupp.decidable_eq

@[instance]

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

comm_semiring (mv_polynomial σ R)

Equations

mv_polynomial.comm_semiring = add_monoid_algebra.comm_semiring

@[instance]

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

inhabited (mv_polynomial σ R)

Equations

mv_polynomial.inhabited = {default := 0}

@[instance]

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

has_scalar R (mv_polynomial σ R)

Equations

mv_polynomial.has_scalar = add_monoid_algebra.has_scalar

@[instance]

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

semimodule R (mv_polynomial σ R)

Equations

mv_polynomial.semimodule = add_monoid_algebra.semimodule

@[instance]

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

algebra R (mv_polynomial σ R)

Equations

mv_polynomial.algebra = add_monoid_algebra.algebra

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

has_coe_to_fun (mv_polynomial σ R)

the coercion turning an mv_polynomial into the function which reports the coefficient of a given monomial

Equations

mv_polynomial.coeff_coe_to_fun = finsupp.has_coe_to_fun

def mv_polynomial.monomial {R : Type u} {σ : Type u_1} [comm_semiring R] (s : σ →₀ ℕ) (a : R) :

mv_polynomial σ R

monomial s a is the monomial a * X^s

Equations

mv_polynomial.monomial s a = finsupp.single s a

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

R →+* mv_polynomial σ R

C a is the constant polynomial with value a

Equations

mv_polynomial.C = {to_fun := mv_polynomial.monomial 0, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}

theorem mv_polynomial.algebra_map_eq (R : Type u) (σ : Type u_1) [comm_semiring R] :

algebra_map R (mv_polynomial σ R) = mv_polynomial.C

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

mv_polynomial σ R

X n is the degree 1 monomial $X_n$.

Equations

mv_polynomial.X n = mv_polynomial.monomial (finsupp.single n 1) 1

@[simp]

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

⇑mv_polynomial.C 0 = 0

@[simp]

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

⇑mv_polynomial.C 1 = 1

theorem mv_polynomial.C_mul_monomial {R : Type u} {σ : Type u_1} {a a' : R} {s : σ →₀ ℕ} [comm_semiring R] :

(⇑mv_polynomial.C a) * mv_polynomial.monomial s a' = mv_polynomial.monomial s (a * a')

@[simp]

theorem mv_polynomial.C_add {R : Type u} {σ : Type u_1} {a a' : R} [comm_semiring R] :

⇑mv_polynomial.C (a + a') = ⇑mv_polynomial.C a + ⇑mv_polynomial.C a'

@[simp]

theorem mv_polynomial.C_mul {R : Type u} {σ : Type u_1} {a a' : R} [comm_semiring R] :

⇑mv_polynomial.C (a * a') = (⇑mv_polynomial.C a) * ⇑mv_polynomial.C a'

@[simp]

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

⇑mv_polynomial.C (a ^ n) = ⇑mv_polynomial.C a ^ n

theorem mv_polynomial.C_injective (σ : Type u_1) (R : Type u_2) [comm_semiring R] :

function.injective ⇑mv_polynomial.C

@[simp]

theorem mv_polynomial.C_inj {σ : Type u_1} (R : Type u_2) [comm_semiring R] (r s : R) :

⇑mv_polynomial.C r = ⇑mv_polynomial.C s ↔ r = s

@[instance]

def mv_polynomial.infinite_of_infinite (σ : Type u_1) (R : Type u_2) [comm_semiring R] [infinite R] :

infinite (mv_polynomial σ R)

@[instance]

def mv_polynomial.infinite_of_nonempty (σ : Type u_1) (R : Type u_2) [nonempty σ] [comm_semiring R] [nontrivial R] :

infinite (mv_polynomial σ R)

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

⇑mv_polynomial.C ↑n = ↑n

theorem mv_polynomial.C_mul' {R : Type u} {σ : Type u_1} {a : R} [comm_semiring R] {p : mv_polynomial σ R} :

(⇑mv_polynomial.C a) * p = a • p

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

a • p = (⇑mv_polynomial.C a) * p

theorem mv_polynomial.X_pow_eq_single {R : Type u} {σ : Type u_1} {e : ℕ} {n : σ} [comm_semiring R] :

mv_polynomial.X n ^ e = mv_polynomial.monomial (finsupp.single n e) 1

theorem mv_polynomial.monomial_add_single {R : Type u} {σ : Type u_1} {a : R} {e : ℕ} {n : σ} {s : σ →₀ ℕ} [comm_semiring R] :

mv_polynomial.monomial (s + finsupp.single n e) a = (mv_polynomial.monomial s a) * mv_polynomial.X n ^ e

theorem mv_polynomial.monomial_single_add {R : Type u} {σ : Type u_1} {a : R} {e : ℕ} {n : σ} {s : σ →₀ ℕ} [comm_semiring R] :

mv_polynomial.monomial (finsupp.single n e + s) a = (mv_polynomial.X n ^ e) * mv_polynomial.monomial s a

theorem mv_polynomial.single_eq_C_mul_X {R : Type u} {σ : Type u_1} [comm_semiring R] {s : σ} {a : R} {n : ℕ} :

mv_polynomial.monomial (finsupp.single s n) a = (⇑mv_polynomial.C a) * mv_polynomial.X s ^ n

@[simp]

theorem mv_polynomial.monomial_add {R : Type u} {σ : Type u_1} [comm_semiring R] {s : σ →₀ ℕ} {a b : R} :

mv_polynomial.monomial s a + mv_polynomial.monomial s b = mv_polynomial.monomial s (a + b)

@[simp]

theorem mv_polynomial.monomial_mul {R : Type u} {σ : Type u_1} [comm_semiring R] {s s' : σ →₀ ℕ} {a b : R} :

(mv_polynomial.monomial s a) * mv_polynomial.monomial s' b = mv_polynomial.monomial (s + s') (a * b)

@[simp]

theorem mv_polynomial.monomial_zero {R : Type u} {σ : Type u_1} [comm_semiring R] {s : σ →₀ ℕ} :

mv_polynomial.monomial s 0 = 0

@[simp]

theorem mv_polynomial.sum_monomial {R : Type u} {σ : Type u_1} [comm_semiring R] {A : Type u_2} [add_comm_monoid A] {u : σ →₀ ℕ} {r : R} {b : (σ →₀ ℕ) → R → A} (w : b u 0 = 0) :

finsupp.sum (mv_polynomial.monomial u r) b = b u r

theorem mv_polynomial.monomial_eq {R : Type u} {σ : Type u_1} {a : R} {s : σ →₀ ℕ} [comm_semiring R] :

mv_polynomial.monomial s a = (⇑mv_polynomial.C a) * s.prod (λ (n : σ) (e : ℕ), mv_polynomial.X n ^ e)

theorem mv_polynomial.induction_on {R : Type u} {σ : Type u_1} [comm_semiring R] {M : mv_polynomial σ R → Prop} (p : mv_polynomial σ R) (h_C : ∀ (a : R), M (⇑mv_polynomial.C a)) (h_add : ∀ (p q : mv_polynomial σ R), M p → M q → M (p + q)) (h_X : ∀ (p : mv_polynomial σ R) (n : σ), M p → M (p * mv_polynomial.X n)) :

M p

theorem mv_polynomial.induction_on' {R : Type u} {σ : Type u_1} [comm_semiring R] {P : mv_polynomial σ R → Prop} (p : mv_polynomial σ R) (h1 : ∀ (u : σ →₀ ℕ) (a : R), P (mv_polynomial.monomial u a)) (h2 : ∀ (p q : mv_polynomial σ R), P p → P q → P (p + q)) :

P p

theorem mv_polynomial.hom_eq_hom {R : Type u} {S₂ : Type w} {σ : Type u_1} [comm_semiring R] [semiring S₂] (f g : mv_polynomial σ R →+* S₂) (hC : ∀ (a : R), ⇑f (⇑mv_polynomial.C a) = ⇑g (⇑mv_polynomial.C a)) (hX : ∀ (n : σ), ⇑f (mv_polynomial.X n) = ⇑g (mv_polynomial.X n)) (p : mv_polynomial σ R) :

⇑f p = ⇑g p

theorem mv_polynomial.is_id {R : Type u} {σ : Type u_1} [comm_semiring R] (f : mv_polynomial σ R →+* mv_polynomial σ R) (hC : ∀ (a : R), ⇑f (⇑mv_polynomial.C a) = ⇑mv_polynomial.C a) (hX : ∀ (n : σ), ⇑f (mv_polynomial.X n) = mv_polynomial.X n) (p : mv_polynomial σ R) :

⇑f p = p

theorem mv_polynomial.ring_hom_ext {R : Type u} {σ : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] (f g : mv_polynomial σ R →+* A) (hC : ∀ (r : R), ⇑f (⇑mv_polynomial.C r) = ⇑g (⇑mv_polynomial.C r)) (hX : ∀ (i : σ), ⇑f (mv_polynomial.X i) = ⇑g (mv_polynomial.X i)) :

f = g

theorem mv_polynomial.alg_hom_ext {R : Type u} {σ : Type u_1} [comm_semiring R] {A : Type u_2} [comm_semiring A] [algebra R A] (f g : mv_polynomial σ R →ₐ[R] A) (hf : ∀ (i : σ), ⇑f (mv_polynomial.X i) = ⇑g (mv_polynomial.X i)) :

f = g

@[simp]

theorem mv_polynomial.alg_hom_C {R : Type u} {σ : Type u_1} [comm_semiring R] (f : mv_polynomial σ R →ₐ[R] mv_polynomial σ R) (r : R) :

⇑f (⇑mv_polynomial.C r) = ⇑mv_polynomial.C r

def mv_polynomial.coeff {R : Type u} {σ : Type u_1} [comm_semiring R] (m : σ →₀ ℕ) (p : mv_polynomial σ R) :

R

The coefficient of the monomial m in the multi-variable polynomial p.

Equations

mv_polynomial.coeff m p = ⇑p m

theorem mv_polynomial.ext {R : Type u} {σ : Type u_1} [comm_semiring R] (p q : mv_polynomial σ R) (a : ∀ (m : σ →₀ ℕ), mv_polynomial.coeff m p = mv_polynomial.coeff m q) :

p = q

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

p = q ↔ ∀ (m : σ →₀ ℕ), mv_polynomial.coeff m p = mv_polynomial.coeff m q

@[simp]

theorem mv_polynomial.coeff_add {R : Type u} {σ : Type u_1} [comm_semiring R] (m : σ →₀ ℕ) (p q : mv_polynomial σ R) :

mv_polynomial.coeff m (p + q) = mv_polynomial.coeff m p + mv_polynomial.coeff m q

@[simp]

theorem mv_polynomial.coeff_zero {R : Type u} {σ : Type u_1} [comm_semiring R] (m : σ →₀ ℕ) :

mv_polynomial.coeff m 0 = 0

@[simp]

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

mv_polynomial.coeff 0 (mv_polynomial.X i) = 0

@[instance]

def mv_polynomial.coeff.is_add_monoid_hom {R : Type u} {σ : Type u_1} [comm_semiring R] (m : σ →₀ ℕ) :

is_add_monoid_hom (mv_polynomial.coeff m)

theorem mv_polynomial.coeff_sum {R : Type u} {σ : Type u_1} [comm_semiring R] {X : Type u_2} (s : finset X) (f : X → mv_polynomial σ R) (m : σ →₀ ℕ) :

mv_polynomial.coeff m (∑ (x : X) in s, f x) = ∑ (x : X) in s, mv_polynomial.coeff m (f x)

theorem mv_polynomial.monic_monomial_eq {R : Type u} {σ : Type u_1} [comm_semiring R] (m : σ →₀ ℕ) :

mv_polynomial.monomial m 1 = m.prod (λ (n : σ) (e : ℕ), mv_polynomial.X n ^ e)

@[simp]

theorem mv_polynomial.coeff_monomial {R : Type u} {σ : Type u_1} [comm_semiring R] (m n : σ →₀ ℕ) (a : R) :

mv_polynomial.coeff m (mv_polynomial.monomial n a) = ite (n = m) a 0

@[simp]

theorem mv_polynomial.coeff_C {R : Type u} {σ : Type u_1} [comm_semiring R] (m : σ →₀ ℕ) (a : R) :

mv_polynomial.coeff m (⇑mv_polynomial.C a) = ite (0 = m) a 0

theorem mv_polynomial.coeff_X_pow {R : Type u} {σ : Type u_1} [comm_semiring R] (i : σ) (m : σ →₀ ℕ) (k : ℕ) :

mv_polynomial.coeff m (mv_polynomial.X i ^ k) = ite (finsupp.single i k = m) 1 0

theorem mv_polynomial.coeff_X' {R : Type u} {σ : Type u_1} [comm_semiring R] (i : σ) (m : σ →₀ ℕ) :

mv_polynomial.coeff m (mv_polynomial.X i) = ite (finsupp.single i 1 = m) 1 0

@[simp]

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

mv_polynomial.coeff (finsupp.single i 1) (mv_polynomial.X i) = 1

@[simp]

theorem mv_polynomial.coeff_C_mul {R : Type u} {σ : Type u_1} [comm_semiring R] (m : σ →₀ ℕ) (a : R) (p : mv_polynomial σ R) :

mv_polynomial.coeff m ((⇑mv_polynomial.C a) * p) = a * mv_polynomial.coeff m p

theorem mv_polynomial.coeff_mul {R : Type u} {σ : Type u_1} [comm_semiring R] (p q : mv_polynomial σ R) (n : σ →₀ ℕ) :

mv_polynomial.coeff n (p * q) = ∑ (x : (σ →₀ ℕ) × (σ →₀ ℕ)) in n.antidiagonal.support, (mv_polynomial.coeff x.fst p) * mv_polynomial.coeff x.snd q

@[simp]

theorem mv_polynomial.coeff_mul_X {R : Type u} {σ : Type u_1} [comm_semiring R] (m : σ →₀ ℕ) (s : σ) (p : mv_polynomial σ R) :

mv_polynomial.coeff (m + finsupp.single s 1) (p * mv_polynomial.X s) = mv_polynomial.coeff m p

theorem mv_polynomial.coeff_mul_X' {R : Type u} {σ : Type u_1} [comm_semiring R] (m : σ →₀ ℕ) (s : σ) (p : mv_polynomial σ R) :

mv_polynomial.coeff m (p * mv_polynomial.X s) = ite (s ∈ m.support) (mv_polynomial.coeff (m - finsupp.single s 1) p) 0

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

p = 0 ↔ ∀ (d : σ →₀ ℕ), mv_polynomial.coeff d p = 0

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

p ≠ 0 ↔ ∃ (d : σ →₀ ℕ), mv_polynomial.coeff d p ≠ 0

theorem mv_polynomial.exists_coeff_ne_zero {R : Type u} {σ : Type u_1} [comm_semiring R] {p : mv_polynomial σ R} (h : p ≠ 0) :

∃ (d : σ →₀ ℕ), mv_polynomial.coeff d p ≠ 0

theorem mv_polynomial.C_dvd_iff_dvd_coeff {R : Type u} {σ : Type u_1} [comm_semiring R] (r : R) (φ : mv_polynomial σ R) :

⇑mv_polynomial.C r ∣ φ ↔ ∀ (i : σ →₀ ℕ), r ∣ mv_polynomial.coeff i φ

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

mv_polynomial σ R →+* R

constant_coeff p returns the constant term of the polynomial p, defined as coeff 0 p. This is a ring homomorphism.

Equations

mv_polynomial.constant_coeff = {to_fun := mv_polynomial.coeff 0, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}

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

⇑mv_polynomial.constant_coeff = mv_polynomial.coeff 0

@[simp]

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

⇑mv_polynomial.constant_coeff (⇑mv_polynomial.C r) = r

@[simp]

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

⇑mv_polynomial.constant_coeff (mv_polynomial.X i) = 0

theorem mv_polynomial.constant_coeff_monomial {R : Type u} {σ : Type u_1} [comm_semiring R] (d : σ →₀ ℕ) (r : R) :

⇑mv_polynomial.constant_coeff (mv_polynomial.monomial d r) = ite (d = 0) r 0

@[simp]

theorem mv_polynomial.constant_coeff_comp_C (R : Type u) (σ : Type u_1) [comm_semiring R] :

mv_polynomial.constant_coeff.comp mv_polynomial.C = ring_hom.id R

@[simp]

theorem mv_polynomial.constant_coeff_comp_algebra_map (R : Type u) (σ : Type u_1) [comm_semiring R] :

mv_polynomial.constant_coeff.comp (algebra_map R (mv_polynomial σ R)) = ring_hom.id R

@[simp]

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

∑ (v : σ →₀ ℕ) in p.support, mv_polynomial.monomial v (mv_polynomial.coeff v p) = p

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

p = ∑ (v : σ →₀ ℕ) in p.support, mv_polynomial.monomial v (mv_polynomial.coeff v p)

def mv_polynomial.eval₂ {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] (f : R →+* S₁) (g : σ → S₁) (p : mv_polynomial σ R) :

S₁

Evaluate a polynomial p given a valuation g of all the variables and a ring hom f from the scalar ring to the target

Equations

mv_polynomial.eval₂ f g p = finsupp.sum p (λ (s : σ →₀ ℕ) (a : R), (⇑f a) * s.prod (λ (n : σ) (e : ℕ), g n ^ e))

theorem mv_polynomial.eval₂_eq {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] (g : R →+* S₁) (x : σ → S₁) (f : mv_polynomial σ R) :

mv_polynomial.eval₂ g x f = ∑ (d : σ →₀ ℕ) in f.support, (⇑g (mv_polynomial.coeff d f)) * ∏ (i : σ) in d.support, x i ^ ⇑d i

theorem mv_polynomial.eval₂_eq' {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] [fintype σ] (g : R →+* S₁) (x : σ → S₁) (f : mv_polynomial σ R) :

mv_polynomial.eval₂ g x f = ∑ (d : σ →₀ ℕ) in f.support, (⇑g (mv_polynomial.coeff d f)) * ∏ (i : σ), x i ^ ⇑d i

@[simp]

theorem mv_polynomial.eval₂_zero {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] (f : R →+* S₁) (g : σ → S₁) :

mv_polynomial.eval₂ f g 0 = 0

@[simp]

theorem mv_polynomial.eval₂_add {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] {p q : mv_polynomial σ R} [comm_semiring S₁] (f : R →+* S₁) (g : σ → S₁) :

mv_polynomial.eval₂ f g (p + q) = mv_polynomial.eval₂ f g p + mv_polynomial.eval₂ f g q

@[simp]

theorem mv_polynomial.eval₂_monomial {R : Type u} {S₁ : Type v} {σ : Type u_1} {a : R} {s : σ →₀ ℕ} [comm_semiring R] [comm_semiring S₁] (f : R →+* S₁) (g : σ → S₁) :

mv_polynomial.eval₂ f g (mv_polynomial.monomial s a) = (⇑f a) * s.prod (λ (n : σ) (e : ℕ), g n ^ e)

@[simp]

theorem mv_polynomial.eval₂_C {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] (f : R →+* S₁) (g : σ → S₁) (a : R) :

mv_polynomial.eval₂ f g (⇑mv_polynomial.C a) = ⇑f a

@[simp]

theorem mv_polynomial.eval₂_one {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] (f : R →+* S₁) (g : σ → S₁) :

mv_polynomial.eval₂ f g 1 = 1

@[simp]

theorem mv_polynomial.eval₂_X {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] (f : R →+* S₁) (g : σ → S₁) (n : σ) :

mv_polynomial.eval₂ f g (mv_polynomial.X n) = g n

theorem mv_polynomial.eval₂_mul_monomial {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] {p : mv_polynomial σ R} [comm_semiring S₁] (f : R →+* S₁) (g : σ → S₁) {s : σ →₀ ℕ} {a : R} :

mv_polynomial.eval₂ f g (p * mv_polynomial.monomial s a) = ((mv_polynomial.eval₂ f g p) * ⇑f a) * s.prod (λ (n : σ) (e : ℕ), g n ^ e)

@[simp]

theorem mv_polynomial.eval₂_mul {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] {q : mv_polynomial σ R} [comm_semiring S₁] (f : R →+* S₁) (g : σ → S₁) {p : mv_polynomial σ R} :

mv_polynomial.eval₂ f g (p * q) = (mv_polynomial.eval₂ f g p) * mv_polynomial.eval₂ f g q

@[simp]

theorem mv_polynomial.eval₂_pow {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] (f : R →+* S₁) (g : σ → S₁) {p : mv_polynomial σ R} {n : ℕ} :

mv_polynomial.eval₂ f g (p ^ n) = mv_polynomial.eval₂ f g p ^ n

@[instance]

def mv_polynomial.eval₂.is_semiring_hom {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] (f : R →+* S₁) (g : σ → S₁) :

is_semiring_hom (mv_polynomial.eval₂ f g)

def mv_polynomial.eval₂_hom {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] (f : R →+* S₁) (g : σ → S₁) :

mv_polynomial σ R →+* S₁

mv_polynomial.eval₂ as a ring_hom.

Equations

mv_polynomial.eval₂_hom f g = ring_hom.of (mv_polynomial.eval₂ f g)

@[simp]

theorem mv_polynomial.coe_eval₂_hom {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] (f : R →+* S₁) (g : σ → S₁) :

⇑(mv_polynomial.eval₂_hom f g) = mv_polynomial.eval₂ f g

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} (a : f₁ = f₂) (a_1 : g₁ = g₂) (a_2 : p₁ = p₂) :

⇑(mv_polynomial.eval₂_hom f₁ g₁) p₁ = ⇑(mv_polynomial.eval₂_hom f₂ g₂) p₂

@[simp]

theorem mv_polynomial.eval₂_hom_C {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] (f : R →+* S₁) (g : σ → S₁) (r : R) :

⇑(mv_polynomial.eval₂_hom f g) (⇑mv_polynomial.C r) = ⇑f r

@[simp]

theorem mv_polynomial.eval₂_hom_X' {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] (f : R →+* S₁) (g : σ → S₁) (i : σ) :

⇑(mv_polynomial.eval₂_hom f g) (mv_polynomial.X i) = g i

@[simp]

theorem mv_polynomial.comp_eval₂_hom {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] [comm_semiring S₂] (f : R →+* S₁) (g : σ → S₁) (φ : S₁ →+* S₂) :

φ.comp (mv_polynomial.eval₂_hom f g) = mv_polynomial.eval₂_hom (φ.comp f) (λ (i : σ), ⇑φ (g i))

theorem mv_polynomial.map_eval₂_hom {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] [comm_semiring S₂] (f : R →+* S₁) (g : σ → S₁) (φ : S₁ →+* S₂) (p : mv_polynomial σ R) :

⇑φ (⇑(mv_polynomial.eval₂_hom f g) p) = ⇑(mv_polynomial.eval₂_hom (φ.comp f) (λ (i : σ), ⇑φ (g i))) p

theorem mv_polynomial.eval₂_hom_monomial {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] (f : R →+* S₁) (g : σ → S₁) (d : σ →₀ ℕ) (r : R) :

⇑(mv_polynomial.eval₂_hom f g) (mv_polynomial.monomial d r) = (⇑f r) * d.prod (λ (i : σ) (k : ℕ), g i ^ k)

theorem mv_polynomial.eval₂_comp_left {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] {S₂ : Type u_2} [comm_semiring S₂] (k : S₁ →+* S₂) (f : R →+* S₁) (g : σ → S₁) (p : mv_polynomial σ R) :

⇑k (mv_polynomial.eval₂ f g p) = mv_polynomial.eval₂ (k.comp f) (⇑k ∘ g) p

@[simp]

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

mv_polynomial.eval₂ mv_polynomial.C mv_polynomial.X p = p

theorem mv_polynomial.eval₂_congr {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] {p : mv_polynomial σ R} [comm_semiring S₁] (f : R →+* S₁) (g₁ g₂ : σ → S₁) (h : ∀ {i : σ} {c : σ →₀ ℕ}, i ∈ c.support → mv_polynomial.coeff c p ≠ 0 → g₁ i = g₂ i) :

mv_polynomial.eval₂ f g₁ p = mv_polynomial.eval₂ f g₂ p

@[simp]

theorem mv_polynomial.eval₂_prod {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] (f : R →+* S₁) (g : σ → S₁) (s : finset S₂) (p : S₂ → mv_polynomial σ R) :

mv_polynomial.eval₂ f g (∏ (x : S₂) in s, p x) = ∏ (x : S₂) in s, mv_polynomial.eval₂ f g (p x)

@[simp]

theorem mv_polynomial.eval₂_sum {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] (f : R →+* S₁) (g : σ → S₁) (s : finset S₂) (p : S₂ → mv_polynomial σ R) :

mv_polynomial.eval₂ f g (∑ (x : S₂) in s, p x) = ∑ (x : S₂) in s, mv_polynomial.eval₂ f g (p x)

theorem mv_polynomial.eval₂_assoc {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] (f : R →+* S₁) (g : σ → S₁) (q : S₂ → mv_polynomial σ R) (p : mv_polynomial S₂ R) :

mv_polynomial.eval₂ f (λ (t : S₂), mv_polynomial.eval₂ f g (q t)) p = mv_polynomial.eval₂ f g (mv_polynomial.eval₂ mv_polynomial.C q p)

def mv_polynomial.eval {R : Type u} {σ : Type u_1} [comm_semiring R] (f : σ → R) :

mv_polynomial σ R →+* R

Evaluate a polynomial p given a valuation f of all the variables

Equations

mv_polynomial.eval f = mv_polynomial.eval₂_hom (ring_hom.id R) f

theorem mv_polynomial.eval_eq {R : Type u} {σ : Type u_1} [comm_semiring R] (x : σ → R) (f : mv_polynomial σ R) :

⇑(mv_polynomial.eval x) f = ∑ (d : σ →₀ ℕ) in f.support, (mv_polynomial.coeff d f) * ∏ (i : σ) in d.support, x i ^ ⇑d i

theorem mv_polynomial.eval_eq' {R : Type u} {σ : Type u_1} [comm_semiring R] [fintype σ] (x : σ → R) (f : mv_polynomial σ R) :

⇑(mv_polynomial.eval x) f = ∑ (d : σ →₀ ℕ) in f.support, (mv_polynomial.coeff d f) * ∏ (i : σ), x i ^ ⇑d i

theorem mv_polynomial.eval_monomial {R : Type u} {σ : Type u_1} {a : R} {s : σ →₀ ℕ} [comm_semiring R] {f : σ → R} :

⇑(mv_polynomial.eval f) (mv_polynomial.monomial s a) = a * s.prod (λ (n : σ) (e : ℕ), f n ^ e)

@[simp]

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

⇑(mv_polynomial.eval f) (⇑mv_polynomial.C a) = a

@[simp]

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

⇑(mv_polynomial.eval f) (mv_polynomial.X n) = f n

@[simp]

theorem mv_polynomial.smul_eval {R : Type u} {σ : Type u_1} [comm_semiring R] (x : σ → R) (p : mv_polynomial σ R) (s : R) :

⇑(mv_polynomial.eval x) (s • p) = s * ⇑(mv_polynomial.eval x) p

theorem mv_polynomial.eval_sum {R : Type u} {σ : Type u_1} [comm_semiring R] {ι : Type u_2} (s : finset ι) (f : ι → mv_polynomial σ R) (g : σ → R) :

⇑(mv_polynomial.eval g) (∑ (i : ι) in s, f i) = ∑ (i : ι) in s, ⇑(mv_polynomial.eval g) (f i)

theorem mv_polynomial.eval_prod {R : Type u} {σ : Type u_1} [comm_semiring R] {ι : Type u_2} (s : finset ι) (f : ι → mv_polynomial σ R) (g : σ → R) :

⇑(mv_polynomial.eval g) (∏ (i : ι) in s, f i) = ∏ (i : ι) in s, ⇑(mv_polynomial.eval g) (f i)

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

⇑(mv_polynomial.eval (⇑(mv_polynomial.eval g) ∘ f)) p = ⇑(mv_polynomial.eval g) (mv_polynomial.eval₂ mv_polynomial.C f p)

def mv_polynomial.map {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] (f : R →+* S₁) :

mv_polynomial σ R →+* mv_polynomial σ S₁

map f p maps a polynomial p across a ring hom f

Equations

mv_polynomial.map f = mv_polynomial.eval₂_hom (mv_polynomial.C.comp f) mv_polynomial.X

@[simp]

theorem mv_polynomial.map_monomial {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] (f : R →+* S₁) (s : σ →₀ ℕ) (a : R) :

⇑(mv_polynomial.map f) (mv_polynomial.monomial s a) = mv_polynomial.monomial s (⇑f a)

@[simp]

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

⇑(mv_polynomial.map f) (⇑mv_polynomial.C a) = ⇑mv_polynomial.C (⇑f a)

@[simp]

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

⇑(mv_polynomial.map f) (mv_polynomial.X n) = mv_polynomial.X n

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

⇑(mv_polynomial.map (ring_hom.id R)) p = p

theorem mv_polynomial.map_map {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] (f : R →+* S₁) [comm_semiring S₂] (g : S₁ →+* S₂) (p : mv_polynomial σ R) :

⇑(mv_polynomial.map g) (⇑(mv_polynomial.map f) p) = ⇑(mv_polynomial.map (g.comp f)) p

theorem mv_polynomial.eval₂_eq_eval_map {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] (f : R →+* S₁) (g : σ → S₁) (p : mv_polynomial σ R) :

mv_polynomial.eval₂ f g p = ⇑(mv_polynomial.eval g) (⇑(mv_polynomial.map f) p)

theorem mv_polynomial.eval₂_comp_right {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] {S₂ : Type u_2} [comm_semiring S₂] (k : S₁ →+* S₂) (f : R →+* S₁) (g : σ → S₁) (p : mv_polynomial σ R) :

⇑k (mv_polynomial.eval₂ f g p) = mv_polynomial.eval₂ k (⇑k ∘ g) (⇑(mv_polynomial.map f) p)

theorem mv_polynomial.map_eval₂ {R : Type u} {S₁ : Type v} {S₂ : Type w} {S₃ : Type x} [comm_semiring R] [comm_semiring S₁] (f : R →+* S₁) (g : S₂ → mv_polynomial S₃ R) (p : mv_polynomial S₂ R) :

⇑(mv_polynomial.map f) (mv_polynomial.eval₂ mv_polynomial.C g p) = mv_polynomial.eval₂ mv_polynomial.C (⇑(mv_polynomial.map f) ∘ g) (⇑(mv_polynomial.map f) p)

theorem mv_polynomial.coeff_map {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] (f : R →+* S₁) (p : mv_polynomial σ R) (m : σ →₀ ℕ) :

mv_polynomial.coeff m (⇑(mv_polynomial.map f) p) = ⇑f (mv_polynomial.coeff m p)

theorem mv_polynomial.map_injective {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] (f : R →+* S₁) (hf : function.injective ⇑f) :

function.injective ⇑(mv_polynomial.map f)

@[simp]

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

⇑(mv_polynomial.eval g) (⇑(mv_polynomial.map f) p) = mv_polynomial.eval₂ f g p

@[simp]

theorem mv_polynomial.eval₂_map {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] [comm_semiring S₂] (f : R →+* S₁) (g : σ → S₂) (φ : S₁ →+* S₂) (p : mv_polynomial σ R) :

mv_polynomial.eval₂ φ g (⇑(mv_polynomial.map f) p) = mv_polynomial.eval₂ (φ.comp f) g p

@[simp]

theorem mv_polynomial.eval₂_hom_map_hom {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] [comm_semiring S₂] (f : R →+* S₁) (g : σ → S₂) (φ : S₁ →+* S₂) (p : mv_polynomial σ R) :

⇑(mv_polynomial.eval₂_hom φ g) (⇑(mv_polynomial.map f) p) = ⇑(mv_polynomial.eval₂_hom (φ.comp f) g) p

@[simp]

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

⇑mv_polynomial.constant_coeff (⇑(mv_polynomial.map f) φ) = ⇑f (⇑mv_polynomial.constant_coeff φ)

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

mv_polynomial.constant_coeff.comp (mv_polynomial.map f) = f.comp mv_polynomial.constant_coeff

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

(⇑(mv_polynomial.map f) p).support ⊆ p.support

theorem mv_polynomial.support_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₁} (hf : function.injective ⇑f) :

(⇑(mv_polynomial.map f) p).support = p.support

theorem mv_polynomial.C_dvd_iff_map_hom_eq_zero {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] (q : R →+* S₁) (r : R) (hr : ∀ (r' : R), ⇑q r' = 0 ↔ r ∣ r') (φ : mv_polynomial σ R) :

⇑mv_polynomial.C r ∣ φ ↔ ⇑(mv_polynomial.map q) φ = 0

The algebra of multivariate polynomials

def mv_polynomial.aeval {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] (f : σ → S₁) [comm_semiring S₁] [algebra R S₁] :

mv_polynomial σ R →ₐ[R] S₁

A map σ → S₁ where S₁ is an algebra over R generates an R-algebra homomorphism from multivariate polynomials over σ to S₁.

Equations

mv_polynomial.aeval f = {to_fun := (mv_polynomial.eval₂_hom (algebra_map R S₁) f).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}

theorem mv_polynomial.aeval_def {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] (f : σ → S₁) [comm_semiring S₁] [algebra R S₁] (p : mv_polynomial σ R) :

⇑(mv_polynomial.aeval f) p = mv_polynomial.eval₂ (algebra_map R S₁) f p

theorem mv_polynomial.aeval_eq_eval₂_hom {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] (f : σ → S₁) [comm_semiring S₁] [algebra R S₁] (p : mv_polynomial σ R) :

⇑(mv_polynomial.aeval f) p = ⇑(mv_polynomial.eval₂_hom (algebra_map R S₁) f) p

@[simp]

theorem mv_polynomial.aeval_X {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] (f : σ → S₁) [comm_semiring S₁] [algebra R S₁] (s : σ) :

⇑(mv_polynomial.aeval f) (mv_polynomial.X s) = f s

@[simp]

theorem mv_polynomial.aeval_C {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] (f : σ → S₁) [comm_semiring S₁] [algebra R S₁] (r : R) :

⇑(mv_polynomial.aeval f) (⇑mv_polynomial.C r) = ⇑(algebra_map R S₁) r

theorem mv_polynomial.eval_unique {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] [algebra R S₁] (φ : mv_polynomial σ R →ₐ[R] S₁) :

φ = mv_polynomial.aeval (⇑φ ∘ mv_polynomial.X)

theorem mv_polynomial.comp_aeval {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] (f : σ → S₁) [comm_semiring S₁] [algebra R S₁] {B : Type u_2} [comm_semiring B] [algebra R B] (φ : S₁ →ₐ[R] B) :

φ.comp (mv_polynomial.aeval f) = mv_polynomial.aeval (λ (i : σ), ⇑φ (f i))

@[simp]

theorem mv_polynomial.map_aeval {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] [algebra R S₁] {B : Type u_2} [comm_semiring B] (g : σ → S₁) (φ : S₁ →+* B) (p : mv_polynomial σ R) :

⇑φ (⇑(mv_polynomial.aeval g) p) = ⇑(mv_polynomial.eval₂_hom (φ.comp (algebra_map R S₁)) (λ (i : σ), ⇑φ (g i))) p

@[simp]

theorem mv_polynomial.aeval_zero {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] [algebra R S₁] (p : mv_polynomial σ R) :

⇑(mv_polynomial.aeval 0) p = ⇑(algebra_map R S₁) (⇑mv_polynomial.constant_coeff p)

@[simp]

theorem mv_polynomial.aeval_zero' {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] [algebra R S₁] (p : mv_polynomial σ R) :

⇑(mv_polynomial.aeval (λ (_x : σ), 0)) p = ⇑(algebra_map R S₁) (⇑mv_polynomial.constant_coeff p)

theorem mv_polynomial.aeval_monomial {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] [algebra R S₁] (g : σ → S₁) (d : σ →₀ ℕ) (r : R) :

⇑(mv_polynomial.aeval g) (mv_polynomial.monomial d r) = (⇑(algebra_map R S₁) r) * d.prod (λ (i : σ) (k : ℕ), g i ^ k)

theorem mv_polynomial.eval₂_hom_eq_zero {R : Type u} {S₂ : Type w} {σ : Type u_1} [comm_semiring R] [comm_semiring S₂] (f : R →+* S₂) (g : σ → S₂) (φ : mv_polynomial σ R) (h : ∀ (d : σ →₀ ℕ), mv_polynomial.coeff d φ ≠ 0 → (∃ (i : σ) (H : i ∈ d.support), g i = 0)) :

⇑(mv_polynomial.eval₂_hom f g) φ = 0

theorem mv_polynomial.aeval_eq_zero {R : Type u} {S₂ : Type w} {σ : Type u_1} [comm_semiring R] [comm_semiring S₂] [algebra R S₂] (f : σ → S₂) (φ : mv_polynomial σ R) (h : ∀ (d : σ →₀ ℕ), mv_polynomial.coeff d φ ≠ 0 → (∃ (i : σ) (H : i ∈ d.support), f i = 0)) :

⇑(mv_polynomial.aeval f) φ = 0