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:

Definitions #

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

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
@[instance]
def mv_polynomial.inhabited {R : Type u} {σ : Type u_1} [comm_semiring R] :
Equations
@[instance]
def mv_polynomial.module {R : Type u} {S₁ : Type v} {σ : Type u_1} [semiring R] [comm_semiring S₁] [module R S₁] :
module R (mv_polynomial σ S₁)
Equations
@[instance]
def mv_polynomial.is_scalar_tower {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [monoid R] [monoid S₁] [comm_semiring S₂] [has_scalar R S₁] [distrib_mul_action R S₂] [distrib_mul_action S₁ S₂] [is_scalar_tower R S₁ S₂] :
@[instance]
def mv_polynomial.smul_comm_class {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [monoid R] [monoid S₁] [comm_semiring S₂] [distrib_mul_action R S₂] [distrib_mul_action S₁ S₂] [smul_comm_class R S₁ S₂] :
@[instance]
def mv_polynomial.algebra {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] [algebra R S₁] :
Equations
def mv_polynomial.monomial {R : Type u} {σ : Type u_1} [comm_semiring R] (s : σ →₀ ) (a : R) :

monomial s a is the monomial with coefficient a and exponents given by s

Equations
theorem mv_polynomial.single_eq_monomial {R : Type u} {σ : Type u_1} [comm_semiring R] (s : σ →₀ ) (a : R) :
theorem mv_polynomial.mul_def {R : Type u} {σ : Type u_1} [comm_semiring R] {p q : mv_polynomial σ R} :
p * q = finsupp.sum p (λ (m : σ →₀ ) (a : R), finsupp.sum q (λ (n : σ →₀ ) (b : R), mv_polynomial.monomial (m + n) (a * b)))
def mv_polynomial.C {R : Type u} {σ : Type u_1} [comm_semiring R] :

C a is the constant polynomial with value a

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

X n is the degree 1 monomial $X_n$.

Equations
theorem mv_polynomial.C_apply {R : Type u} {σ : Type u_1} {a : R} [comm_semiring R] :
@[simp]
theorem mv_polynomial.C_0 {R : Type u} {σ : Type u_1} [comm_semiring R] :
@[simp]
theorem mv_polynomial.C_1 {R : Type u} {σ : Type u_1} [comm_semiring R] :
theorem mv_polynomial.C_mul_monomial {R : Type u} {σ : Type u_1} {a a' : R} {s : σ →₀ } [comm_semiring R] :
@[simp]
theorem mv_polynomial.C_add {R : Type u} {σ : Type u_1} {a a' : R} [comm_semiring R] :
@[simp]
theorem mv_polynomial.C_mul {R : Type u} {σ : Type u_1} {a a' : R} [comm_semiring R] :
@[simp]
theorem mv_polynomial.C_pow {R : Type u} {σ : Type u_1} [comm_semiring R] (a : R) (n : ) :
@[simp]
theorem mv_polynomial.C_inj {σ : Type u_1} (R : Type u_2) [comm_semiring R] (r s : R) :
@[instance]
def mv_polynomial.infinite_of_infinite (σ : Type u_1) (R : Type u_2) [comm_semiring R] [infinite R] :
@[instance]
def mv_polynomial.infinite_of_nonempty (σ : Type u_1) (R : Type u_2) [nonempty σ] [comm_semiring R] [nontrivial R] :
theorem mv_polynomial.C_eq_coe_nat {R : Type u} {σ : Type u_1} [comm_semiring R] (n : ) :
theorem mv_polynomial.C_mul' {R : Type u} {σ : Type u_1} {a : R} [comm_semiring R] {p : mv_polynomial σ R} :
theorem mv_polynomial.smul_eq_C_mul {R : Type u} {σ : Type u_1} [comm_semiring R] (p : mv_polynomial σ R) (a : R) :
theorem mv_polynomial.X_pow_eq_single {R : Type u} {σ : Type u_1} {e : } {n : σ} [comm_semiring R] :
theorem mv_polynomial.monomial_add_single {R : Type u} {σ : Type u_1} {a : R} {e : } {n : σ} {s : σ →₀ } [comm_semiring R] :
theorem mv_polynomial.monomial_single_add {R : Type u} {σ : Type u_1} {a : R} {e : } {n : σ} {s : σ →₀ } [comm_semiring R] :
theorem mv_polynomial.monomial_eq_C_mul_X {R : Type u} {σ : Type u_1} [comm_semiring R] {s : σ} {a : R} {n : } :
@[simp]
theorem mv_polynomial.monomial_add {R : Type u} {σ : Type u_1} [comm_semiring R] {s : σ →₀ } {a b : R} :
@[simp]
theorem mv_polynomial.monomial_mul {R : Type u} {σ : Type u_1} [comm_semiring R] {s s' : σ →₀ } {a b : R} :
@[simp]
theorem mv_polynomial.monomial_zero {R : Type u} {σ : Type u_1} [comm_semiring R] {s : σ →₀ } :
@[simp]
theorem mv_polynomial.sum_monomial_eq {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) :
@[simp]
theorem mv_polynomial.sum_C {R : Type u} {σ : Type u_1} {a : R} [comm_semiring R] {A : Type u_2} [add_comm_monoid A] {b : →₀ )R → A} (w : b 0 0 = 0) :
theorem mv_polynomial.monomial_eq {R : Type u} {σ : Type u_1} {a : R} {s : σ →₀ } [comm_semiring R] :
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 pM qM (p + q)) (h_X : ∀ (p : mv_polynomial σ R) (n : σ), M pM (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 pP qP (p + q)) :
P p
@[ext]
theorem mv_polynomial.ring_hom_ext {R : Type u} {σ : Type u_1} [comm_semiring R] {A : Type u_2} [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.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
@[ext]
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) :
def mv_polynomial.support {R : Type u} {σ : Type u_1} [comm_semiring R] (p : mv_polynomial σ R) :

The finite set of all m : σ →₀ ℕ such that X^m has a non-zero coefficient.

Equations
theorem mv_polynomial.support_monomial {R : Type u} {σ : Type u_1} {a : R} {s : σ →₀ } [comm_semiring R] [decidable (a = 0)] :
theorem mv_polynomial.support_monomial_subset {R : Type u} {σ : Type u_1} {a : R} {s : σ →₀ } [comm_semiring R] :
theorem mv_polynomial.support_add {R : Type u} {σ : Type u_1} [comm_semiring R] {p q : mv_polynomial σ R} :
theorem mv_polynomial.support_X {R : Type u} {σ : Type u_1} {n : σ} [comm_semiring R] [nontrivial 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
@[simp]
theorem mv_polynomial.mem_support_iff {R : Type u} {σ : Type u_1} [comm_semiring R] {p : mv_polynomial σ R} {m : σ →₀ } :
theorem mv_polynomial.not_mem_support_iff {R : Type u} {σ : Type u_1} [comm_semiring R] {p : mv_polynomial σ R} {m : σ →₀ } :
theorem mv_polynomial.sum_def {R : Type u} {σ : Type u_1} [comm_semiring R] {A : Type u_2} [add_comm_monoid A] {p : mv_polynomial σ R} {b : →₀ )R → A} :
finsupp.sum p b = ∑ (m : σ →₀ ) in p.support, b m (mv_polynomial.coeff m p)
theorem mv_polynomial.support_mul {R : Type u} {σ : Type u_1} [comm_semiring R] (p q : mv_polynomial σ R) :
(p * q).support p.support.bUnion (λ (a : σ →₀ ), q.support.bUnion (λ (b : σ →₀ ), {a + b}))
@[ext]
theorem mv_polynomial.ext {R : Type u} {σ : Type u_1} [comm_semiring R] (p q : mv_polynomial σ R) :
(∀ (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) :
@[simp]
theorem mv_polynomial.coeff_add {R : Type u} {σ : Type u_1} [comm_semiring R] (m : σ →₀ ) (p q : mv_polynomial σ R) :
@[simp]
theorem mv_polynomial.coeff_smul {R : Type u} {σ : Type u_1} [comm_semiring R] {S₁ : Type u_2} [monoid S₁] [distrib_mul_action S₁ R] (m : σ →₀ ) (c : S₁) (p : mv_polynomial σ R) :
@[simp]
theorem mv_polynomial.coeff_zero {R : Type u} {σ : Type u_1} [comm_semiring R] (m : σ →₀ ) :
@[simp]
theorem mv_polynomial.coeff_zero_X {R : Type u} {σ : Type u_1} [comm_semiring R] (i : σ) :
@[instance]
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] [decidable_eq σ] (m n : σ →₀ ) (a : R) :
@[simp]
theorem mv_polynomial.coeff_C {R : Type u} {σ : Type u_1} [comm_semiring R] [decidable_eq σ] (m : σ →₀ ) (a : R) :
theorem mv_polynomial.coeff_one {R : Type u} {σ : Type u_1} [comm_semiring R] [decidable_eq σ] (m : σ →₀ ) :
mv_polynomial.coeff m 1 = ite (0 = m) 1 0
@[simp]
theorem mv_polynomial.coeff_zero_C {R : Type u} {σ : Type u_1} [comm_semiring R] (a : R) :
@[simp]
theorem mv_polynomial.coeff_zero_one {R : Type u} {σ : Type u_1} [comm_semiring R] :
theorem mv_polynomial.coeff_X_pow {R : Type u} {σ : Type u_1} [comm_semiring R] [decidable_eq σ] (i : σ) (m : σ →₀ ) (k : ) :
theorem mv_polynomial.coeff_X' {R : Type u} {σ : Type u_1} [comm_semiring R] [decidable_eq σ] (i : σ) (m : σ →₀ ) :
@[simp]
theorem mv_polynomial.coeff_X {R : Type u} {σ : Type u_1} [comm_semiring R] (i : σ) :
@[simp]
theorem mv_polynomial.coeff_C_mul {R : Type u} {σ : Type u_1} [comm_semiring R] (m : σ →₀ ) (a : R) (p : mv_polynomial σ R) :
theorem mv_polynomial.coeff_mul {R : Type u} {σ : Type u_1} [comm_semiring R] (p q : mv_polynomial σ R) (n : σ →₀ ) :
@[simp]
theorem mv_polynomial.coeff_mul_X {R : Type u} {σ : Type u_1} [comm_semiring R] (m : σ →₀ ) (s : σ) (p : mv_polynomial σ R) :
theorem mv_polynomial.coeff_mul_X' {R : Type u} {σ : Type u_1} [comm_semiring R] [decidable_eq σ] (m : σ →₀ ) (s : σ) (p : mv_polynomial σ R) :
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) :
def mv_polynomial.constant_coeff {R : Type u} {σ : Type u_1} [comm_semiring R] :

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

Equations
@[simp]
theorem mv_polynomial.constant_coeff_C {R : Type u} {σ : Type u_1} [comm_semiring R] (r : R) :
@[simp]
theorem mv_polynomial.constant_coeff_X {R : Type u} {σ : Type u_1} [comm_semiring R] (i : σ) :
theorem mv_polynomial.constant_coeff_monomial {R : Type u} {σ : Type u_1} [comm_semiring R] [decidable_eq σ] (d : σ →₀ ) (r : R) :
@[simp]
theorem mv_polynomial.support_sum_monomial_coeff {R : Type u} {σ : Type u_1} [comm_semiring R] (p : mv_polynomial σ R) :
theorem mv_polynomial.as_sum {R : Type u} {σ : Type u_1} [comm_semiring R] (p : mv_polynomial σ R) :
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
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₁) :
@[simp]
theorem mv_polynomial.eval₂_add {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] {p q : mv_polynomial σ R} (f : R →+* S₁) (g : σ → S₁) :
@[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) :
@[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₁) :
@[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 : σ) :
theorem mv_polynomial.eval₂_mul_monomial {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] {p : mv_polynomial σ R} (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] [comm_semiring S₁] {q : mv_polynomial σ R} (f : R →+* S₁) (g : σ → S₁) {p : mv_polynomial σ R} :
@[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 : } :
@[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₁) :
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.eval₂ as a ring_hom.

Equations
@[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₁) :
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₂g₁ = g₂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) :
@[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 : σ) :
@[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) :
@[simp]
theorem mv_polynomial.eval₂_congr {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] {p : mv_polynomial σ R} (f : R →+* S₁) (g₁ g₂ : σ → S₁) (h : ∀ {i : σ} {c : σ →₀ }, i c.supportmv_polynomial.coeff c p 0g₁ i = g₂ i) :
@[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) :
def mv_polynomial.eval {R : Type u} {σ : Type u_1} [comm_semiring R] (f : σ → R) :

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

Equations
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) :
@[simp]
theorem mv_polynomial.eval_X {R : Type u} {σ : Type u_1} [comm_semiring R] {f : σ → R} (n : σ) :
@[simp]
theorem mv_polynomial.smul_eval {R : Type u} {σ : Type u_1} [comm_semiring R] (x : σ → R) (p : mv_polynomial σ R) (s : R) :
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) :
def mv_polynomial.map {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] (f : R →+* S₁) :

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

Equations
@[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) :
@[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) :
@[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 : σ) :
theorem mv_polynomial.map_id {R : Type u} {σ : Type u_1} [comm_semiring R] (p : mv_polynomial σ R) :
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) :
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) :
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) :
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) :
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 : σ →₀ ) :
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) :
@[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) :
@[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) :
@[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) :
@[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) :
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) :
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) :
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) :
theorem mv_polynomial.map_map_range_eq_iff {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] (f : R →+* S₁) (g : S₁ → R) (hg : g 0 = 0) (φ : mv_polynomial σ S₁) :

The algebra of multivariate polynomials #

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

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

Equations
theorem mv_polynomial.aeval_def {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] (f : σ → S₁) [algebra R S₁] (p : mv_polynomial σ R) :
theorem mv_polynomial.aeval_eq_eval₂_hom {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] (f : σ → S₁) [algebra R S₁] (p : mv_polynomial σ R) :
@[simp]
theorem mv_polynomial.aeval_X {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] (f : σ → S₁) [algebra R S₁] (s : σ) :
@[simp]
theorem mv_polynomial.aeval_C {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] (f : σ → S₁) [algebra R S₁] (r : R) :
theorem mv_polynomial.aeval_unique {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] [algebra R S₁] (φ : mv_polynomial σ R →ₐ[R] S₁) :
theorem mv_polynomial.comp_aeval {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] (f : σ → 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.eval₂_hom_zero {R : Type u} {S₂ : Type w} {σ : Type u_1} [comm_semiring R] [comm_semiring S₂] (f : R →+* S₂) (p : mv_polynomial σ R) :
@[simp]
theorem mv_polynomial.eval₂_hom_zero' {R : Type u} {S₂ : Type w} {σ : Type u_1} [comm_semiring R] [comm_semiring S₂] (f : R →+* S₂) (p : mv_polynomial σ R) :
@[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) :
@[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) :
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)) :
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)) :