mathlib3 documentation

data.mv_polynomial.basic

Multivariate polynomials #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

source
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
Instances for mv_polynomial
source
@[protected, 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
source
@[protected, instance]
noncomputable def mv_polynomial.comm_semiring {R : Type u} {σ : Type u_1} [comm_semiring R] :
comm_semiring (mv_polynomial σ R)
Equations
source
@[protected, instance]
noncomputable def mv_polynomial.inhabited {R : Type u} {σ : Type u_1} [comm_semiring R] :
inhabited (mv_polynomial σ R)
Equations
source
@[protected, instance]
noncomputable def mv_polynomial.distrib_mul_action {R : Type u} {S₁ : Type v} {σ : Type u_1} [monoid R] [comm_semiring S₁] [distrib_mul_action R S₁] :
distrib_mul_action R (mv_polynomial σ S₁)
Equations
source
@[protected, instance]
noncomputable def mv_polynomial.smul_zero_class {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring S₁] [smul_zero_class R S₁] :
smul_zero_class R (mv_polynomial σ S₁)
Equations
source
@[protected, instance]
def mv_polynomial.has_faithful_smul {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring S₁] [smul_zero_class R S₁] [has_faithful_smul R S₁] :
has_faithful_smul R (mv_polynomial σ S₁)
source
@[protected, instance]
noncomputable 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
source
@[protected, instance]
def mv_polynomial.is_scalar_tower {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [comm_semiring S₂] [has_smul R S₁] [smul_zero_class R S₂] [smul_zero_class S₁ S₂] [is_scalar_tower R S₁ S₂] :
is_scalar_tower R S₁ (mv_polynomial σ S₂)
source
@[protected, instance]
def mv_polynomial.smul_comm_class {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [comm_semiring S₂] [smul_zero_class R S₂] [smul_zero_class S₁ S₂] [smul_comm_class R S₁ S₂] :
smul_comm_class R S₁ (mv_polynomial σ S₂)
source
@[protected, instance]
def mv_polynomial.is_central_scalar {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring S₁] [smul_zero_class R S₁] [smul_zero_class Rᵐᵒᵖ S₁] [is_central_scalar R S₁] :
is_central_scalar R (mv_polynomial σ S₁)
source
@[protected, instance]
noncomputable def mv_polynomial.algebra {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] [algebra R S₁] :
algebra R (mv_polynomial σ S₁)
Equations
source
@[protected, instance]
def mv_polynomial.is_scalar_tower_right {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring S₁] [distrib_smul R S₁] [is_scalar_tower R S₁ S₁] :
is_scalar_tower R (mv_polynomial σ S₁) (mv_polynomial σ S₁)
source
@[protected, instance]
def mv_polynomial.smul_comm_class_right {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring S₁] [distrib_smul R S₁] [smul_comm_class R S₁ S₁] :
smul_comm_class R (mv_polynomial σ S₁) (mv_polynomial σ S₁)
source
@[protected, instance]
def mv_polynomial.unique {R : Type u} {σ : Type u_1} [comm_semiring R] [subsingleton R] :
unique (mv_polynomial σ R)

If R is a subsingleton, then mv_polynomial σ R has a unique element

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

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

Equations
source
theorem mv_polynomial.single_eq_monomial {R : Type u} {σ : Type u_1} [comm_semiring R] (s : σ →₀ ℕ) (a : R) :
finsupp.single s a = ⇑(mv_polynomial.monomial s) a
source
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)))
source
noncomputable 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
source
theorem mv_polynomial.algebra_map_eq (R : Type u) (σ : Type u_1) [comm_semiring R] :
algebra_map R (mv_polynomial σ R) = mv_polynomial.C
source
noncomputable 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
source
theorem mv_polynomial.monomial_left_injective {R : Type u} {σ : Type u_1} [comm_semiring R] {r : R} (hr : r ≠ 0) :
function.injective (λ (s : σ →₀ ℕ), ⇑(mv_polynomial.monomial s) r)
source
@[simp]
theorem mv_polynomial.monomial_left_inj {R : Type u} {σ : Type u_1} [comm_semiring R] {s t : σ →₀ ℕ} {r : R} (hr : r ≠ 0) :
⇑(mv_polynomial.monomial s) r = ⇑(mv_polynomial.monomial t) r ↔ s = t
source
theorem mv_polynomial.C_apply {R : Type u} {σ : Type u_1} {a : R} [comm_semiring R] :
⇑mv_polynomial.C a = ⇑(mv_polynomial.monomial 0) a
source
@[simp]
theorem mv_polynomial.C_0 {R : Type u} {σ : Type u_1} [comm_semiring R] :
⇑mv_polynomial.C 0 = 0
source
@[simp]
theorem mv_polynomial.C_1 {R : Type u} {σ : Type u_1} [comm_semiring R] :
⇑mv_polynomial.C 1 = 1
source
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')
source
@[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'
source
@[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'
source
@[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
source
theorem mv_polynomial.C_injective (σ : Type u_1) (R : Type u_2) [comm_semiring R] :
function.injective ⇑mv_polynomial.C
source
theorem mv_polynomial.C_surjective {R : Type u_1} [comm_semiring R] (σ : Type u_2) [is_empty σ] :
function.surjective ⇑mv_polynomial.C
source
@[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
source
@[protected, instance]
def mv_polynomial.infinite_of_infinite (σ : Type u_1) (R : Type u_2) [comm_semiring R] [infinite R] :
infinite (mv_polynomial σ R)
source
@[protected, instance]
def mv_polynomial.infinite_of_nonempty (σ : Type u_1) (R : Type u_2) [nonempty σ] [comm_semiring R] [nontrivial R] :
infinite (mv_polynomial σ R)
source
theorem mv_polynomial.C_eq_coe_nat {R : Type u} {σ : Type u_1} [comm_semiring R] (n : ℕ) :
⇑mv_polynomial.C ↑n = ↑n
source
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
source
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
source
theorem mv_polynomial.C_eq_smul_one {R : Type u} {σ : Type u_1} {a : R} [comm_semiring R] :
⇑mv_polynomial.C a = a • 1
source
theorem mv_polynomial.smul_monomial {R : Type u} {σ : Type u_1} {a : R} {s : σ →₀ ℕ} [comm_semiring R] {S₁ : Type u_2} [smul_zero_class S₁ R] (r : S₁) :
r • ⇑(mv_polynomial.monomial s) a = ⇑(mv_polynomial.monomial s) (r • a)
source
theorem mv_polynomial.X_injective {R : Type u} {σ : Type u_1} [comm_semiring R] [nontrivial R] :
function.injective mv_polynomial.X
source
@[simp]
theorem mv_polynomial.X_inj {R : Type u} {σ : Type u_1} [comm_semiring R] [nontrivial R] (m n : σ) :
mv_polynomial.X m = mv_polynomial.X n ↔ m = n
source
theorem mv_polynomial.monomial_pow {R : Type u} {σ : Type u_1} {a : R} {e : ℕ} {s : σ →₀ ℕ} [comm_semiring R] :
⇑(mv_polynomial.monomial s) a ^ e = ⇑(mv_polynomial.monomial (e • s)) (a ^ e)
source
@[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)
source
noncomputable def mv_polynomial.monomial_one_hom (R : Type u) (σ : Type u_1) [comm_semiring R] :
multiplicative (σ →₀ ℕ) →* mv_polynomial σ R

λ s, monomial s 1 as a homomorphism.

Equations
source
@[simp]
theorem mv_polynomial.monomial_one_hom_apply {R : Type u} {σ : Type u_1} {s : σ →₀ ℕ} [comm_semiring R] :
⇑(mv_polynomial.monomial_one_hom R σ) s = ⇑(mv_polynomial.monomial s) 1
source
theorem mv_polynomial.X_pow_eq_monomial {R : Type u} {σ : Type u_1} {e : ℕ} {n : σ} [comm_semiring R] :
mv_polynomial.X n ^ e = ⇑(mv_polynomial.monomial (finsupp.single n e)) 1
source
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
source
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
source
theorem mv_polynomial.C_mul_X_pow_eq_monomial {R : Type u} {σ : Type u_1} [comm_semiring R] {s : σ} {a : R} {n : ℕ} :
⇑mv_polynomial.C a * mv_polynomial.X s ^ n = ⇑(mv_polynomial.monomial (finsupp.single s n)) a
source
theorem mv_polynomial.C_mul_X_eq_monomial {R : Type u} {σ : Type u_1} [comm_semiring R] {s : σ} {a : R} :
⇑mv_polynomial.C a * mv_polynomial.X s = ⇑(mv_polynomial.monomial (finsupp.single s 1)) a
source
@[simp]
theorem mv_polynomial.monomial_zero {R : Type u} {σ : Type u_1} [comm_semiring R] {s : σ →₀ ℕ} :
⇑(mv_polynomial.monomial s) 0 = 0
source
@[simp]
theorem mv_polynomial.monomial_zero' {R : Type u} {σ : Type u_1} [comm_semiring R] :
⇑(mv_polynomial.monomial 0) = ⇑mv_polynomial.C
source
@[simp]
theorem mv_polynomial.monomial_eq_zero {R : Type u} {σ : Type u_1} [comm_semiring R] {s : σ →₀ ℕ} {b : R} :
⇑(mv_polynomial.monomial s) b = 0 ↔ b = 0
source
@[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) :
finsupp.sum (⇑(mv_polynomial.monomial u) r) b = b u r
source
@[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) :
finsupp.sum (⇑mv_polynomial.C a) b = b 0 a
source
theorem mv_polynomial.monomial_sum_one {R : Type u} {σ : Type u_1} [comm_semiring R] {α : Type u_2} (s : finset α) (f : α → σ →₀ ℕ) :
⇑(mv_polynomial.monomial (s.sum (λ (i : α), f i))) 1 = s.prod (λ (i : α), ⇑(mv_polynomial.monomial (f i)) 1)
source
theorem mv_polynomial.monomial_sum_index {R : Type u} {σ : Type u_1} [comm_semiring R] {α : Type u_2} (s : finset α) (f : α → σ →₀ ℕ) (a : R) :
⇑(mv_polynomial.monomial (s.sum (λ (i : α), f i))) a = ⇑mv_polynomial.C a * s.prod (λ (i : α), ⇑(mv_polynomial.monomial (f i)) 1)
source
theorem mv_polynomial.monomial_finsupp_sum_index {R : Type u} {σ : Type u_1} [comm_semiring R] {α : Type u_2} {β : Type u_3} [has_zero β] (f : α →₀ β) (g : α → β → σ →₀ ℕ) (a : R) :
⇑(mv_polynomial.monomial (f.sum g)) a = ⇑mv_polynomial.C a * f.prod (λ (a : α) (b : β), ⇑(mv_polynomial.monomial (g a b)) 1)
source
theorem mv_polynomial.monomial_eq_monomial_iff {R : Type u} [comm_semiring R] {α : Type u_1} (a₁ a₂ : α →₀ ℕ) (b₁ b₂ : R) :
⇑(mv_polynomial.monomial a₁) b₁ = ⇑(mv_polynomial.monomial a₂) b₂ ↔ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0
source
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)
source
theorem mv_polynomial.induction_on_monomial {R : Type u} {σ : Type u_1} [comm_semiring R] {M : mv_polynomial σ R → Prop} (h_C : ∀ (a : R), M (⇑mv_polynomial.C a)) (h_X : ∀ (p : mv_polynomial σ R) (n : σ), M p → M (p * mv_polynomial.X n)) (s : σ →₀ ℕ) (a : R) :
M (⇑(mv_polynomial.monomial s) a)
source
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

Analog of polynomial.induction_on'. To prove something about mv_polynomials, it suffices to show the condition is closed under taking sums, and it holds for monomials.

source
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_weak : ∀ (a : σ →₀ ℕ) (b : R) (f : (σ →₀ ℕ) →₀ R), a ∉ f.support → b ≠ 0 → M f → M (⇑(mv_polynomial.monomial a) b + f)) :
M p

Similar to mv_polynomial.induction_on but only a weak form of h_add is required.

source
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_weak : ∀ (a : σ →₀ ℕ) (b : R) (f : (σ →₀ ℕ) →₀ R), a ∉ f.support → b ≠ 0 → M f → M (⇑(mv_polynomial.monomial a) b) → M (⇑(mv_polynomial.monomial a) b + f)) (h_X : ∀ (p : mv_polynomial σ R) (n : σ), M p → M (p * mv_polynomial.X n)) :
M p

Similar to mv_polynomial.induction_on but only a yet weaker form of h_add is required.

source
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

Analog of polynomial.induction_on.

source
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
source
@[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 : f.comp mv_polynomial.C = g.comp mv_polynomial.C) (hX : ∀ (i : σ), ⇑f (mv_polynomial.X i) = ⇑g (mv_polynomial.X i)) :
f = g

See note [partially-applied ext lemmas].

source
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 : f.comp mv_polynomial.C = g.comp mv_polynomial.C) (hX : ∀ (n : σ), ⇑f (mv_polynomial.X n) = ⇑g (mv_polynomial.X n)) (p : mv_polynomial σ R) :
⇑f p = ⇑g p
source
theorem mv_polynomial.is_id {R : Type u} {σ : Type u_1} [comm_semiring R] (f : mv_polynomial σ R →+* mv_polynomial σ R) (hC : f.comp mv_polynomial.C = mv_polynomial.C) (hX : ∀ (n : σ), ⇑f (mv_polynomial.X n) = mv_polynomial.X n) (p : mv_polynomial σ R) :
⇑f p = p
source
@[ext]
theorem mv_polynomial.alg_hom_ext' {R : Type u} {σ : Type u_1} [comm_semiring R] {A : Type u_2} {B : Type u_3} [comm_semiring A] [comm_semiring B] [algebra R A] [algebra R B] {f g : mv_polynomial σ A →ₐ[R] B} (h₁ : f.comp (is_scalar_tower.to_alg_hom R A (mv_polynomial σ A)) = g.comp (is_scalar_tower.to_alg_hom R A (mv_polynomial σ A))) (h₂ : ∀ (i : σ), ⇑f (mv_polynomial.X i) = ⇑g (mv_polynomial.X i)) :
f = g
source
@[ext]
theorem mv_polynomial.alg_hom_ext {R : Type u} {σ : Type u_1} [comm_semiring R] {A : Type u_2} [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
source
@[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
source
@[simp]
theorem mv_polynomial.adjoin_range_X {R : Type u} {σ : Type u_1} [comm_semiring R] :
algebra.adjoin R (set.range mv_polynomial.X) = ⊤
source
@[ext]
theorem mv_polynomial.linear_map_ext {R : Type u} {σ : Type u_1} [comm_semiring R] {M : Type u_2} [add_comm_monoid M] [module R M] {f g : mv_polynomial σ R →ₗ[R] M} (h : ∀ (s : σ →₀ ℕ), f.comp (mv_polynomial.monomial s) = g.comp (mv_polynomial.monomial s)) :
f = g
source
def mv_polynomial.support {R : Type u} {σ : Type u_1} [comm_semiring R] (p : mv_polynomial σ R) :
finset (σ →₀ ℕ)

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

Equations
source
theorem mv_polynomial.finsupp_support_eq_support {R : Type u} {σ : Type u_1} [comm_semiring R] (p : mv_polynomial σ R) :
p.support = p.support
source
theorem mv_polynomial.support_monomial {R : Type u} {σ : Type u_1} {a : R} {s : σ →₀ ℕ} [comm_semiring R] [decidable (a = 0)] :
(⇑(mv_polynomial.monomial s) a).support = ite (a = 0) ∅ {s}
source
theorem mv_polynomial.support_monomial_subset {R : Type u} {σ : Type u_1} {a : R} {s : σ →₀ ℕ} [comm_semiring R] :
(⇑(mv_polynomial.monomial s) a).support ⊆ {s}
source
theorem mv_polynomial.support_add {R : Type u} {σ : Type u_1} [comm_semiring R] {p q : mv_polynomial σ R} [decidable_eq σ] :
(p + q).support ⊆ p.support ∪ q.support
source
theorem mv_polynomial.support_X {R : Type u} {σ : Type u_1} {n : σ} [comm_semiring R] [nontrivial R] :
(mv_polynomial.X n).support = {finsupp.single n 1}
source
theorem mv_polynomial.support_X_pow {R : Type u} {σ : Type u_1} [comm_semiring R] [nontrivial R] (s : σ) (n : ℕ) :
(mv_polynomial.X s ^ n).support = {finsupp.single s n}
source
@[simp]
theorem mv_polynomial.support_zero {R : Type u} {σ : Type u_1} [comm_semiring R] :
0.support = ∅
source
theorem mv_polynomial.support_smul {R : Type u} {σ : Type u_1} [comm_semiring R] {S₁ : Type u_2} [smul_zero_class S₁ R] {a : S₁} {f : mv_polynomial σ R} :
(a • f).support ⊆ f.support
source
theorem mv_polynomial.support_sum {R : Type u} {σ : Type u_1} [comm_semiring R] {α : Type u_2} [decidable_eq σ] {s : finset α} {f : α → mv_polynomial σ R} :
(s.sum (λ (x : α), f x)).support ⊆ s.bUnion (λ (x : α), (f x).support)
source
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
source
@[simp]
theorem mv_polynomial.mem_support_iff {R : Type u} {σ : Type u_1} [comm_semiring R] {p : mv_polynomial σ R} {m : σ →₀ ℕ} :
m ∈ p.support ↔ mv_polynomial.coeff m p ≠ 0
source
theorem mv_polynomial.not_mem_support_iff {R : Type u} {σ : Type u_1} [comm_semiring R] {p : mv_polynomial σ R} {m : σ →₀ ℕ} :
m ∉ p.support ↔ mv_polynomial.coeff m p = 0
source
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 = p.support.sum (λ (m : σ →₀ ℕ), b m (mv_polynomial.coeff m p))
source
theorem mv_polynomial.support_mul {R : Type u} {σ : Type u_1} [comm_semiring R] [decidable_eq σ] (p q : mv_polynomial σ R) :
(p * q).support ⊆ p.support.bUnion (λ (a : σ →₀ ℕ), q.support.bUnion (λ (b : σ →₀ ℕ), {a + b}))
source
@[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
source
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
source
@[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
source
@[simp]
theorem mv_polynomial.coeff_smul {R : Type u} {σ : Type u_1} [comm_semiring R] {S₁ : Type u_2} [smul_zero_class S₁ R] (m : σ →₀ ℕ) (c : S₁) (p : mv_polynomial σ R) :
mv_polynomial.coeff m (c • p) = c • mv_polynomial.coeff m p
source
@[simp]
theorem mv_polynomial.coeff_zero {R : Type u} {σ : Type u_1} [comm_semiring R] (m : σ →₀ ℕ) :
mv_polynomial.coeff m 0 = 0
source
@[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
source
def mv_polynomial.coeff_add_monoid_hom {R : Type u} {σ : Type u_1} [comm_semiring R] (m : σ →₀ ℕ) :
mv_polynomial σ R →+ R

mv_polynomial.coeff m but promoted to an add_monoid_hom.

Equations
source
@[simp]
theorem mv_polynomial.coeff_add_monoid_hom_apply {R : Type u} {σ : Type u_1} [comm_semiring R] (m : σ →₀ ℕ) (p : mv_polynomial σ R) :
⇑(mv_polynomial.coeff_add_monoid_hom m) p = mv_polynomial.coeff m p
source
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 (s.sum (λ (x : X), f x)) = s.sum (λ (x : X), mv_polynomial.coeff m (f x))
source
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)
source
@[simp]
theorem mv_polynomial.coeff_monomial {R : Type u} {σ : Type u_1} [comm_semiring R] [decidable_eq σ] (m n : σ →₀ ℕ) (a : R) :
mv_polynomial.coeff m (⇑(mv_polynomial.monomial n) a) = ite (n = m) a 0
source
@[simp]
theorem mv_polynomial.coeff_C {R : Type u} {σ : Type u_1} [comm_semiring R] [decidable_eq σ] (m : σ →₀ ℕ) (a : R) :
mv_polynomial.coeff m (⇑mv_polynomial.C a) = ite (0 = m) a 0
source
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
source
@[simp]
theorem mv_polynomial.coeff_zero_C {R : Type u} {σ : Type u_1} [comm_semiring R] (a : R) :
mv_polynomial.coeff 0 (⇑mv_polynomial.C a) = a
source
@[simp]
theorem mv_polynomial.coeff_zero_one {R : Type u} {σ : Type u_1} [comm_semiring R] :
mv_polynomial.coeff 0 1 = 1
source
theorem mv_polynomial.coeff_X_pow {R : Type u} {σ : Type u_1} [comm_semiring R] [decidable_eq σ] (i : σ) (m : σ →₀ ℕ) (k : ℕ) :
mv_polynomial.coeff m (mv_polynomial.X i ^ k) = ite (finsupp.single i k = m) 1 0
source
theorem mv_polynomial.coeff_X' {R : Type u} {σ : Type u_1} [comm_semiring R] [decidable_eq σ] (i : σ) (m : σ →₀ ℕ) :
mv_polynomial.coeff m (mv_polynomial.X i) = ite (finsupp.single i 1 = m) 1 0
source
@[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
source
@[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
source
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) = n.antidiagonal.sum (λ (x : (σ →₀ ℕ) × (σ →₀ ℕ)), mv_polynomial.coeff x.fst p * mv_polynomial.coeff x.snd q)
source
@[simp]
theorem mv_polynomial.coeff_mul_monomial {R : Type u} {σ : Type u_1} [comm_semiring R] (m s : σ →₀ ℕ) (r : R) (p : mv_polynomial σ R) :
mv_polynomial.coeff (m + s) (p * ⇑(mv_polynomial.monomial s) r) = mv_polynomial.coeff m p * r
source
@[simp]
theorem mv_polynomial.coeff_monomial_mul {R : Type u} {σ : Type u_1} [comm_semiring R] (m s : σ →₀ ℕ) (r : R) (p : mv_polynomial σ R) :
mv_polynomial.coeff (s + m) (⇑(mv_polynomial.monomial s) r * p) = r * mv_polynomial.coeff m p
source
@[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
source
@[simp]
theorem mv_polynomial.coeff_X_mul {R : Type u} {σ : Type u_1} [comm_semiring R] (m : σ →₀ ℕ) (s : σ) (p : mv_polynomial σ R) :
mv_polynomial.coeff (finsupp.single s 1 + m) (mv_polynomial.X s * p) = mv_polynomial.coeff m p
source
@[simp]
theorem mv_polynomial.support_mul_X {R : Type u} {σ : Type u_1} [comm_semiring R] (s : σ) (p : mv_polynomial σ R) :
(p * mv_polynomial.X s).support = finset.map (add_right_embedding (finsupp.single s 1)) p.support
source
@[simp]
theorem mv_polynomial.support_X_mul {R : Type u} {σ : Type u_1} [comm_semiring R] (s : σ) (p : mv_polynomial σ R) :
(mv_polynomial.X s * p).support = finset.map (add_left_embedding (finsupp.single s 1)) p.support
source
@[simp]
theorem mv_polynomial.support_smul_eq {R : Type u} {σ : Type u_1} [comm_semiring R] {S₁ : Type u_2} [semiring S₁] [module S₁ R] [no_zero_smul_divisors S₁ R] {a : S₁} (h : a ≠ 0) (p : mv_polynomial σ R) :
(a • p).support = p.support
source
theorem mv_polynomial.support_sdiff_support_subset_support_add {R : Type u} {σ : Type u_1} [comm_semiring R] [decidable_eq σ] (p q : mv_polynomial σ R) :
p.support \ q.support ⊆ (p + q).support
source
theorem mv_polynomial.support_symm_diff_support_subset_support_add {R : Type u} {σ : Type u_1} [comm_semiring R] [decidable_eq σ] (p q : mv_polynomial σ R) :
p.support ∆ q.support ⊆ (p + q).support
source
theorem mv_polynomial.coeff_mul_monomial' {R : Type u} {σ : Type u_1} [comm_semiring R] (m s : σ →₀ ℕ) (r : R) (p : mv_polynomial σ R) :
mv_polynomial.coeff m (p * ⇑(mv_polynomial.monomial s) r) = ite (s ≤ m) (mv_polynomial.coeff (m - s) p * r) 0
source
theorem mv_polynomial.coeff_monomial_mul' {R : Type u} {σ : Type u_1} [comm_semiring R] (m s : σ →₀ ℕ) (r : R) (p : mv_polynomial σ R) :
mv_polynomial.coeff m (⇑(mv_polynomial.monomial s) r * p) = ite (s ≤ m) (r * mv_polynomial.coeff (m - s) p) 0
source
theorem mv_polynomial.coeff_mul_X' {R : Type u} {σ : Type u_1} [comm_semiring R] [decidable_eq σ] (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
source
theorem mv_polynomial.coeff_X_mul' {R : Type u} {σ : Type u_1} [comm_semiring R] [decidable_eq σ] (m : σ →₀ ℕ) (s : σ) (p : mv_polynomial σ R) :
mv_polynomial.coeff m (mv_polynomial.X s * p) = ite (s ∈ m.support) (mv_polynomial.coeff (m - finsupp.single s 1) p) 0
source
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
source
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
source
@[simp]
theorem mv_polynomial.support_eq_empty {R : Type u} {σ : Type u_1} [comm_semiring R] {p : mv_polynomial σ R} :
p.support = ∅ ↔ p = 0
source
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
source
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 φ
source
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
source
theorem mv_polynomial.constant_coeff_eq {R : Type u} {σ : Type u_1} [comm_semiring R] :
⇑mv_polynomial.constant_coeff = mv_polynomial.coeff 0
source
@[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
source
@[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
source
@[simp]
theorem mv_polynomial.constant_coeff_smul {S₁ : Type v} {σ : Type u_1} [comm_semiring S₁] {R : Type u_2} [smul_zero_class R S₁] (a : R) (f : mv_polynomial σ S₁) :
⇑mv_polynomial.constant_coeff (a • f) = a • ⇑mv_polynomial.constant_coeff f
source
theorem mv_polynomial.constant_coeff_monomial {R : Type u} {σ : Type u_1} [comm_semiring R] [decidable_eq σ] (d : σ →₀ ℕ) (r : R) :
⇑mv_polynomial.constant_coeff (⇑(mv_polynomial.monomial d) r) = ite (d = 0) r 0
source
@[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
source
@[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
source
@[simp]
theorem mv_polynomial.support_sum_monomial_coeff {R : Type u} {σ : Type u_1} [comm_semiring R] (p : mv_polynomial σ R) :
p.support.sum (λ (v : σ →₀ ℕ), ⇑(mv_polynomial.monomial v) (mv_polynomial.coeff v p)) = p
source
theorem mv_polynomial.as_sum {R : Type u} {σ : Type u_1} [comm_semiring R] (p : mv_polynomial σ R) :
p = p.support.sum (λ (v : σ →₀ ℕ), ⇑(mv_polynomial.monomial v) (mv_polynomial.coeff v p))
source
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
source
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 = f.support.sum (λ (d : σ →₀ ℕ), ⇑g (mv_polynomial.coeff d f) * d.support.prod (λ (i : σ), x i ^ ⇑d i))
source
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 = f.support.sum (λ (d : σ →₀ ℕ), ⇑g (mv_polynomial.coeff d f) * finset.univ.prod (λ (i : σ), x i ^ ⇑d i))
source
@[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
source
@[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₁) :
mv_polynomial.eval₂ f g (p + q) = mv_polynomial.eval₂ f g p + mv_polynomial.eval₂ f g q
source
@[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)
source
@[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
source
@[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
source
@[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
source
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)
source
theorem mv_polynomial.eval₂_mul_C {R : Type u} {S₁ : Type v} {σ : Type u_1} {a : R} [comm_semiring R] [comm_semiring S₁] {p : mv_polynomial σ R} (f : R →+* S₁) (g : σ → S₁) :
mv_polynomial.eval₂ f g (p * ⇑mv_polynomial.C a) = mv_polynomial.eval₂ f g p * ⇑f a
source
@[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} :
mv_polynomial.eval₂ f g (p * q) = mv_polynomial.eval₂ f g p * mv_polynomial.eval₂ f g q
source
@[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
source
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
source
@[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
source
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₂
source
@[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
source
@[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
source
@[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))
source
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
source
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)
source
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
source
@[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
source
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.support → mv_polynomial.coeff c p ≠ 0 → g₁ i = g₂ i) :
mv_polynomial.eval₂ f g₁ p = mv_polynomial.eval₂ f g₂ p
source
@[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 (s.prod (λ (x : S₂), p x)) = s.prod (λ (x : S₂), mv_polynomial.eval₂ f g (p x))
source
@[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 (s.sum (λ (x : S₂), p x)) = s.sum (λ (x : S₂), mv_polynomial.eval₂ f g (p x))
source
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)
source
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
source
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 = f.support.sum (λ (d : σ →₀ ℕ), mv_polynomial.coeff d f * d.support.prod (λ (i : σ), x i ^ ⇑d i))
source
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 = f.support.sum (λ (d : σ →₀ ℕ), mv_polynomial.coeff d f * finset.univ.prod (λ (i : σ), x i ^ ⇑d i))
source
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)
source
@[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
source
@[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
source
@[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
source
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) (s.sum (λ (i : ι), f i)) = s.sum (λ (i : ι), ⇑(mv_polynomial.eval g) (f i))
source
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) (s.prod (λ (i : ι), f i)) = s.prod (λ (i : ι), ⇑(mv_polynomial.eval g) (f i))
source
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)
source
@[simp]
theorem mv_polynomial.eval₂_id {R : Type u} {σ : Type u_1} [comm_semiring R] (p : mv_polynomial σ R) (g : σ → R) :
mv_polynomial.eval₂ (ring_hom.id R) g p = ⇑(mv_polynomial.eval g) p
source
theorem mv_polynomial.eval_eval₂ {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] {τ : Type u_2} (f : R →+* mv_polynomial τ S₁) (g : σ → mv_polynomial τ S₁) (p : mv_polynomial σ R) (x : τ → S₁) :
⇑(mv_polynomial.eval x) (mv_polynomial.eval₂ f g p) = mv_polynomial.eval₂ ((mv_polynomial.eval x).comp f) (λ (s : σ), ⇑(mv_polynomial.eval x) (g s)) p
source
noncomputable 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
source
@[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)
source
@[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)
source
@[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
source
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
source
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
source
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)
source
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)
source
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)
source
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)
source
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)
source
theorem mv_polynomial.map_surjective {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] (f : R →+* S₁) (hf : function.surjective ⇑f) :
function.surjective ⇑(mv_polynomial.map f)
source
theorem mv_polynomial.map_left_inverse {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] {f : R →+* S₁} {g : S₁ →+* R} (hf : function.left_inverse ⇑f ⇑g) :
function.left_inverse ⇑(mv_polynomial.map f) ⇑(mv_polynomial.map g)

If f is a left-inverse of g then map f is a left-inverse of map g.

source
theorem mv_polynomial.map_right_inverse {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] {f : R →+* S₁} {g : S₁ →+* R} (hf : function.right_inverse ⇑f ⇑g) :
function.right_inverse ⇑(mv_polynomial.map f) ⇑(mv_polynomial.map g)

If f is a right-inverse of g then map f is a right-inverse of map g.

source
@[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
source
@[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
source
@[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
source
@[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 φ)
source
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
source
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
source
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
source
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
source
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₁) :
⇑(mv_polynomial.map f) (finsupp.map_range g hg φ) = φ ↔ ∀ (d : σ →₀ ℕ), ⇑f (g (mv_polynomial.coeff d φ)) = mv_polynomial.coeff d φ
source
@[simp]
theorem mv_polynomial.map_alg_hom_apply {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] [comm_semiring S₂] [algebra R S₁] [algebra R S₂] (f : S₁ →ₐ[R] S₂) (ᾰ : mv_polynomial σ S₁) :
⇑(mv_polynomial.map_alg_hom f) ᾰ = ⇑(mv_polynomial.map ↑f) ᾰ
source
noncomputable def mv_polynomial.map_alg_hom {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] [comm_semiring S₂] [algebra R S₁] [algebra R S₂] (f : S₁ →ₐ[R] S₂) :
mv_polynomial σ S₁ →ₐ[R] mv_polynomial σ S₂

If f : S₁ →ₐ[R] S₂ is a morphism of R-algebras, then so is mv_polynomial.map f.

Equations
source
@[simp]
theorem mv_polynomial.map_alg_hom_id {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] [algebra R S₁] :
mv_polynomial.map_alg_hom (alg_hom.id R S₁) = alg_hom.id R (mv_polynomial σ S₁)
source
@[simp]
theorem mv_polynomial.map_alg_hom_coe_ring_hom {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] [comm_semiring S₂] [algebra R S₁] [algebra R S₂] (f : S₁ →ₐ[R] S₂) :
↑(mv_polynomial.map_alg_hom f) = mv_polynomial.map ↑f

The algebra of multivariate polynomials #

source
theorem mv_polynomial.algebra_map_apply {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] [algebra R S₁] (r : R) :
⇑(algebra_map R (mv_polynomial σ S₁)) r = ⇑mv_polynomial.C (⇑(algebra_map R S₁) r)
source
noncomputable def mv_polynomial.aeval {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] [algebra R S₁] (f : σ → 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
source
theorem mv_polynomial.aeval_def {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] [algebra R S₁] (f : σ → S₁) (p : mv_polynomial σ R) :
⇑(mv_polynomial.aeval f) p = mv_polynomial.eval₂ (algebra_map R S₁) f p
source
theorem mv_polynomial.aeval_eq_eval₂_hom {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] [algebra R S₁] (f : σ → S₁) (p : mv_polynomial σ R) :
⇑(mv_polynomial.aeval f) p = ⇑(mv_polynomial.eval₂_hom (algebra_map R S₁) f) p
source
@[simp]
theorem mv_polynomial.aeval_X {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] [algebra R S₁] (f : σ → S₁) (s : σ) :
⇑(mv_polynomial.aeval f) (mv_polynomial.X s) = f s
source
@[simp]
theorem mv_polynomial.aeval_C {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] [algebra R S₁] (f : σ → S₁) (r : R) :
⇑(mv_polynomial.aeval f) (⇑mv_polynomial.C r) = ⇑(algebra_map R S₁) r
source
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₁) :
φ = mv_polynomial.aeval (⇑φ ∘ mv_polynomial.X)
source
theorem mv_polynomial.aeval_X_left {R : Type u} {σ : Type u_1} [comm_semiring R] :
mv_polynomial.aeval mv_polynomial.X = alg_hom.id R (mv_polynomial σ R)
source
theorem mv_polynomial.aeval_X_left_apply {R : Type u} {σ : Type u_1} [comm_semiring R] (p : mv_polynomial σ R) :
⇑(mv_polynomial.aeval mv_polynomial.X) p = p
source
theorem mv_polynomial.comp_aeval {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] [algebra R S₁] (f : σ → 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))
source
@[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
source
@[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₂) :
mv_polynomial.eval₂_hom f 0 = f.comp mv_polynomial.constant_coeff
source
@[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₂) :
mv_polynomial.eval₂_hom f (λ (_x : σ), 0) = f.comp mv_polynomial.constant_coeff
source
theorem mv_polynomial.eval₂_hom_zero_apply {R : Type u} {S₂ : Type w} {σ : Type u_1} [comm_semiring R] [comm_semiring S₂] (f : R →+* S₂) (p : mv_polynomial σ R) :
⇑(mv_polynomial.eval₂_hom f 0) p = ⇑f (⇑mv_polynomial.constant_coeff p)
source
theorem mv_polynomial.eval₂_hom_zero'_apply {R : Type u} {S₂ : Type w} {σ : Type u_1} [comm_semiring R] [comm_semiring S₂] (f : R →+* S₂) (p : mv_polynomial σ R) :
⇑(mv_polynomial.eval₂_hom f (λ (_x : σ), 0)) p = ⇑f (⇑mv_polynomial.constant_coeff p)
source
@[simp]
theorem mv_polynomial.eval₂_zero_apply {R : Type u} {S₂ : Type w} {σ : Type u_1} [comm_semiring R] [comm_semiring S₂] (f : R →+* S₂) (p : mv_polynomial σ R) :
mv_polynomial.eval₂ f 0 p = ⇑f (⇑mv_polynomial.constant_coeff p)
source
@[simp]
theorem mv_polynomial.eval₂_zero'_apply {R : Type u} {S₂ : Type w} {σ : Type u_1} [comm_semiring R] [comm_semiring S₂] (f : R →+* S₂) (p : mv_polynomial σ R) :
mv_polynomial.eval₂ f (λ (_x : σ), 0) p = ⇑f (⇑mv_polynomial.constant_coeff p)
source
@[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)
source
@[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)
source
@[simp]
theorem mv_polynomial.eval_zero {R : Type u} {σ : Type u_1} [comm_semiring R] :
mv_polynomial.eval 0 = mv_polynomial.constant_coeff
source
@[simp]
theorem mv_polynomial.eval_zero' {R : Type u} {σ : Type u_1} [comm_semiring R] :
mv_polynomial.eval (λ (_x : σ), 0) = mv_polynomial.constant_coeff
source
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)
source
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
source
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
source
theorem mv_polynomial.aeval_sum {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] [algebra R S₁] (f : σ → S₁) {ι : Type u_2} (s : finset ι) (φ : ι → mv_polynomial σ R) :
⇑(mv_polynomial.aeval f) (s.sum (λ (i : ι), φ i)) = s.sum (λ (i : ι), ⇑(mv_polynomial.aeval f) (φ i))
source
theorem mv_polynomial.aeval_prod {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] [algebra R S₁] (f : σ → S₁) {ι : Type u_2} (s : finset ι) (φ : ι → mv_polynomial σ R) :
⇑(mv_polynomial.aeval f) (s.prod (λ (i : ι), φ i)) = s.prod (λ (i : ι), ⇑(mv_polynomial.aeval f) (φ i))
source
theorem algebra.adjoin_range_eq_range_aeval (R : Type u) {S₁ : Type v} {σ : Type u_1} [comm_semiring R] [comm_semiring S₁] [algebra R S₁] (f : σ → S₁) :
algebra.adjoin R (set.range f) = (mv_polynomial.aeval f).range
source
theorem algebra.adjoin_eq_range (R : Type u) {S₁ : Type v} [comm_semiring R] [comm_semiring S₁] [algebra R S₁] (s : set S₁) :
algebra.adjoin R s = (mv_polynomial.aeval coe).range
source
noncomputable def mv_polynomial.aeval_tower {R : Type u} {σ : Type u_1} [comm_semiring R] {S : Type u_2} {A : Type u_3} [comm_semiring S] [comm_semiring A] [algebra S R] [algebra S A] (f : R →ₐ[S] A) (x : σ → A) :
mv_polynomial σ R →ₐ[S] A

Version of aeval for defining algebra homs out of mv_polynomial σ R over a smaller base ring than R.

Equations
source
@[simp]
theorem mv_polynomial.aeval_tower_X {R : Type u} {σ : Type u_1} [comm_semiring R] {S : Type u_2} {A : Type u_3} [comm_semiring S] [comm_semiring A] [algebra S R] [algebra S A] (g : R →ₐ[S] A) (y : σ → A) (i : σ) :
⇑(mv_polynomial.aeval_tower g y) (mv_polynomial.X i) = y i
source
@[simp]
theorem mv_polynomial.aeval_tower_C {R : Type u} {σ : Type u_1} [comm_semiring R] {S : Type u_2} {A : Type u_3} [comm_semiring S] [comm_semiring A] [algebra S R] [algebra S A] (g : R →ₐ[S] A) (y : σ → A) (x : R) :
⇑(mv_polynomial.aeval_tower g y) (⇑mv_polynomial.C x) = ⇑g x
source
@[simp]
theorem mv_polynomial.aeval_tower_comp_C {R : Type u} {σ : Type u_1} [comm_semiring R] {S : Type u_2} {A : Type u_3} [comm_semiring S] [comm_semiring A] [algebra S R] [algebra S A] (g : R →ₐ[S] A) (y : σ → A) :
↑(mv_polynomial.aeval_tower g y).comp mv_polynomial.C = ↑g
source
@[simp]
theorem mv_polynomial.aeval_tower_algebra_map {R : Type u} {σ : Type u_1} [comm_semiring R] {S : Type u_2} {A : Type u_3} [comm_semiring S] [comm_semiring A] [algebra S R] [algebra S A] (g : R →ₐ[S] A) (y : σ → A) (x : R) :
⇑(mv_polynomial.aeval_tower g y) (⇑(algebra_map R (mv_polynomial σ R)) x) = ⇑g x
source
@[simp]
theorem mv_polynomial.aeval_tower_comp_algebra_map {R : Type u} {σ : Type u_1} [comm_semiring R] {S : Type u_2} {A : Type u_3} [comm_semiring S] [comm_semiring A] [algebra S R] [algebra S A] (g : R →ₐ[S] A) (y : σ → A) :
↑(mv_polynomial.aeval_tower g y).comp (algebra_map R (mv_polynomial σ R)) = ↑g
source
theorem mv_polynomial.aeval_tower_to_alg_hom {R : Type u} {σ : Type u_1} [comm_semiring R] {S : Type u_2} {A : Type u_3} [comm_semiring S] [comm_semiring A] [algebra S R] [algebra S A] (g : R →ₐ[S] A) (y : σ → A) (x : R) :
⇑(mv_polynomial.aeval_tower g y) (⇑(is_scalar_tower.to_alg_hom S R (mv_polynomial σ R)) x) = ⇑g x
source
@[simp]
theorem mv_polynomial.aeval_tower_comp_to_alg_hom {R : Type u} {σ : Type u_1} [comm_semiring R] {S : Type u_2} {A : Type u_3} [comm_semiring S] [comm_semiring A] [algebra S R] [algebra S A] (g : R →ₐ[S] A) (y : σ → A) :
(mv_polynomial.aeval_tower g y).comp (is_scalar_tower.to_alg_hom S R (mv_polynomial σ R)) = g
source
@[simp]
theorem mv_polynomial.aeval_tower_id {σ : Type u_1} {S : Type u_2} [comm_semiring S] :
mv_polynomial.aeval_tower (alg_hom.id S S) = mv_polynomial.aeval
source
@[simp]
theorem mv_polynomial.aeval_tower_of_id {σ : Type u_1} {S : Type u_2} {A : Type u_3} [comm_semiring S] [comm_semiring A] [algebra S A] :
mv_polynomial.aeval_tower (algebra.of_id S A) = mv_polynomial.aeval
source
theorem mv_polynomial.eval₂_mem {R : Type u} {σ : Type u_1} [comm_semiring R] {S : Type u_2} {subS : Type u_3} [comm_semiring S] [set_like subS S] [subsemiring_class subS S] {f : R →+* S} {p : mv_polynomial σ R} {s : subS} (hs : ∀ (i : σ →₀ ℕ), i ∈ p.support → ⇑f (mv_polynomial.coeff i p) ∈ s) {v : σ → S} (hv : ∀ (i : σ), v i ∈ s) :
mv_polynomial.eval₂ f v p ∈ s
source
theorem mv_polynomial.eval_mem {σ : Type u_1} {S : Type u_2} {subS : Type u_3} [comm_semiring S] [set_like subS S] [subsemiring_class subS S] {p : mv_polynomial σ S} {s : subS} (hs : ∀ (i : σ →₀ ℕ), i ∈ p.support → mv_polynomial.coeff i p ∈ s) {v : σ → S} (hv : ∀ (i : σ), v i ∈ s) :
⇑(mv_polynomial.eval v) p ∈ s