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 inmv_polynomial σ Rwhich mathematicians might callX^sa : Ri : σ, with corresponding monomialX i, often denotedX_iby mathematiciansp : mv_polynomial σ R
Definitions #
mv_polynomial σ R: the type of polynomials with variables of typeσand coefficients in the commutative semiringRmonomial s a: the monomial which mathematically would be denoteda * X^sC a: the constant polynomial with valueaX i: the degree one monomial corresponding to i; mathematically this might be denotedXᵢ.coeff s p: the coefficient ofsinp.eval₂ (f : R → S₁) (g : σ → S₁) p: given a semiring homomorphism fromRto another semiringS₁, and a mapσ → S₁, evaluatespat this valuation, returning a term of typeS₁. Note thateval₂can be made usingevalandmap(see below), and it has been suggested that sticking toevalandmapmight make the code less brittle.eval (g : σ → R) p: given a mapσ → R, evaluatespat this valuation, returning a term of typeRmap (f : R → S₁) p: returns the multivariate polynomial obtained frompby the change of coefficient semiring corresponding tof
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
Multivariate polynomial, where σ is the index set of the variables and
R is the coefficient ring
Equations
- mv_polynomial σ R = add_monoid_algebra R (σ →₀ ℕ)
Instances for mv_polynomial
- mv_polynomial.unique_factorization_monoid
- mv_polynomial.comm_semiring
- mv_polynomial.inhabited
- mv_polynomial.distrib_mul_action
- mv_polynomial.has_faithful_smul
- mv_polynomial.module
- mv_polynomial.is_scalar_tower
- mv_polynomial.smul_comm_class
- mv_polynomial.is_central_scalar
- mv_polynomial.algebra
- mv_polynomial.is_scalar_tower'
- mv_polynomial.unique
- mv_polynomial.infinite_of_infinite
- mv_polynomial.infinite_of_nonempty
- mv_polynomial.monad
- mv_polynomial.is_lawful_functor
- mv_polynomial.is_lawful_monad
- mv_polynomial.comm_ring
- mv_polynomial.is_noetherian_ring
- mv_polynomial.no_zero_divisors
- mv_polynomial.is_domain
- mv_polynomial.coe_to_mv_power_series
- mv_power_series.algebra_mv_polynomial
- mv_polynomial.char_p
- algebra.formally_smooth.mv_polynomial
- ideal.mv_polynomial.mv_polynomial.ideal.is_jacobson
@[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)
@[protected, instance]
noncomputable
def
mv_polynomial.comm_semiring
{R : Type u}
{σ : Type u_1}
[comm_semiring R] :
comm_semiring (mv_polynomial σ R)
@[protected, instance]
noncomputable
def
mv_polynomial.inhabited
{R : Type u}
{σ : Type u_1}
[comm_semiring R] :
inhabited (mv_polynomial σ R)
Equations
- mv_polynomial.inhabited = {default := 0}
@[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₁)
@[protected, instance]
def
mv_polynomial.has_faithful_smul
{R : Type u}
{S₁ : Type v}
{σ : Type u_1}
[monoid R]
[comm_semiring S₁]
[distrib_mul_action R S₁]
[has_faithful_smul R S₁] :
has_faithful_smul R (mv_polynomial σ S₁)
@[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
@[protected, 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_smul R S₁]
[distrib_mul_action R S₂]
[distrib_mul_action S₁ S₂]
[is_scalar_tower R S₁ S₂] :
is_scalar_tower R S₁ (mv_polynomial σ S₂)
@[protected, 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₂] :
smul_comm_class R S₁ (mv_polynomial σ S₂)
@[protected, instance]
def
mv_polynomial.is_central_scalar
{R : Type u}
{S₁ : Type v}
{σ : Type u_1}
[monoid R]
[comm_semiring S₁]
[distrib_mul_action R S₁]
[distrib_mul_action Rᵐᵒᵖ S₁]
[is_central_scalar R S₁] :
is_central_scalar R (mv_polynomial σ S₁)
@[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
@[protected, instance]
def
mv_polynomial.is_scalar_tower'
{R : Type u}
{S₁ : Type v}
{σ : Type u_1}
[comm_semiring R]
[comm_semiring S₁]
[algebra R S₁] :
is_scalar_tower R (mv_polynomial σ S₁) (mv_polynomial σ S₁)
@[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
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
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
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)))
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
- 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
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
- mv_polynomial.X n = ⇑(mv_polynomial.monomial (finsupp.single n 1)) 1
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)
@[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
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
@[simp]
@[simp]
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
@[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
@[protected, instance]
def
mv_polynomial.infinite_of_infinite
(σ : Type u_1)
(R : Type u_2)
[comm_semiring R]
[infinite R] :
infinite (mv_polynomial σ R)
@[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)
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.C_eq_smul_one
{R : Type u}
{σ : Type u_1}
{a : R}
[comm_semiring R] :
⇑mv_polynomial.C a = a • 1
@[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
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)
@[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)
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
- mv_polynomial.monomial_one_hom R σ = add_monoid_algebra.of R (σ →₀ ℕ)
@[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
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
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.monomial_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_zero
{R : Type u}
{σ : Type u_1}
[comm_semiring R]
{s : σ →₀ ℕ} :
⇑(mv_polynomial.monomial s) 0 = 0
@[simp]
@[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
@[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
@[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
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)
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)
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)
theorem
mv_polynomial.monomial_eq_monomial_iff
{R : Type u}
[comm_semiring R]
{α : Type u_1}
(a₁ a₂ : α →₀ ℕ)
(b₁ b₂ : 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_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)
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.
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.
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.
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.
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
@[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
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) :
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) :
@[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
@[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
@[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
@[simp]
@[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
The finite set of all m : σ →₀ ℕ such that X^m has a non-zero coefficient.
theorem
mv_polynomial.finsupp_support_eq_support
{R : Type u}
{σ : Type u_1}
[comm_semiring R]
(p : mv_polynomial σ R) :
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] :
(⇑(mv_polynomial.monomial s) a).support ⊆ {s}
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] :
(mv_polynomial.X n).support = {finsupp.single n 1}
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}
@[simp]
theorem
mv_polynomial.support_sum
{R : Type u}
{σ : Type u_1}
[comm_semiring R]
{α : Type u_2}
{s : finset α}
{f : α → mv_polynomial σ 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
@[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
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
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))
@[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) :
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_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) :
mv_polynomial.coeff m (c • p) = c • mv_polynomial.coeff m p
@[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
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
- mv_polynomial.coeff_add_monoid_hom m = {to_fun := mv_polynomial.coeff m, map_zero' := _, map_add' := _}
@[simp]
theorem
mv_polynomial.coeff_add_monoid_hom_apply
{R : Type u}
{σ : Type u_1}
[comm_semiring R]
(m : σ →₀ ℕ)
(p : mv_polynomial σ R) :
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))
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) :
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]
[decidable_eq σ]
(m : σ →₀ ℕ)
(a : R) :
mv_polynomial.coeff m (⇑mv_polynomial.C a) = ite (0 = m) a 0
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) :
mv_polynomial.coeff 0 (⇑mv_polynomial.C a) = a
@[simp]
theorem
mv_polynomial.coeff_zero_one
{R : Type u}
{σ : Type u_1}
[comm_semiring R] :
mv_polynomial.coeff 0 1 = 1
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
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
@[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) = n.antidiagonal.sum (λ (x : (σ →₀ ℕ) × (σ →₀ ℕ)), mv_polynomial.coeff x.fst p * mv_polynomial.coeff x.snd q)
@[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
@[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
@[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
@[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
@[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
@[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
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) :
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) :
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
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
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
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
theorem
mv_polynomial.eq_zero_iff
{R : Type u}
{σ : Type u_1}
[comm_semiring R]
{p : mv_polynomial σ R} :
theorem
mv_polynomial.ne_zero_iff
{R : Type u}
{σ : Type u_1}
[comm_semiring R]
{p : mv_polynomial σ R} :
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' := _}
@[simp]
@[simp]
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
@[simp]
@[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) :
p.support.sum (λ (v : σ →₀ ℕ), ⇑(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 = p.support.sum (λ (v : σ →₀ ℕ), ⇑(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) :
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))
@[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]
[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
@[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]
[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)
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
@[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
@[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
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 = {to_fun := mv_polynomial.eval₂ f g, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
@[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} :
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) :
⇑(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) :
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
@[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))
@[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))
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
theorem
mv_polynomial.eval_eq
{R : Type u}
{σ : Type u_1}
[comm_semiring R]
(x : σ → R)
(f : mv_polynomial σ R) :
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))
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) (s.sum (λ (i : ι), f i)) = s.sum (λ (i : ι), ⇑(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) (s.prod (λ (i : ι), f i)) = s.prod (λ (i : ι), ⇑(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)
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
@[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) :
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) :
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) :
If f is a left-inverse of g then map f is a left-inverse of map g.
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) :
If f is a right-inverse of g then map f is a right-inverse of map g.
@[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) :
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₁) :
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
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 φ
@[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) ᾰ
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.
@[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₁)
@[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₂) :
The algebra of multivariate polynomials #
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
- 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]
[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
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
@[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
@[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
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₁]
[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))
@[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₂) :
@[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
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)
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)
@[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)
@[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)
@[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)
@[simp]
@[simp]
theorem
mv_polynomial.eval_zero'
{R : Type u}
{σ : Type u_1}
[comm_semiring R] :
mv_polynomial.eval (λ (_x : σ), 0) = mv_polynomial.constant_coeff
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
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))
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))
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
theorem
algebra.adjoin_eq_range
(R : Type u)
{S₁ : Type v}
[comm_semiring R]
[comm_semiring S₁]
[algebra R S₁]
(s : set S₁) :
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.
@[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
@[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
@[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) :
@[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
@[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
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
@[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
@[simp]
@[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] :