# mathlib3documentation

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:

• σ : Type* (indexing the variables)
• R : Type* [comm_semiring R] (the coefficients)
• s : σ →₀ ℕ, a function from σ to ℕ which is zero away from a finite set. This will give rise to a monomial in mv_polynomial σ R which mathematicians might call X^s
• a : R
• i : σ, with corresponding monomial X i, often denoted X_i by mathematicians
• p : mv_polynomial σ R

### Definitions #

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

## Implementation notes #

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

## Tags #

polynomial, multivariate polynomial, multivariable polynomial

def mv_polynomial (σ : Type u_1) (R : Type u_2)  :
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
@[protected, instance]
Equations
@[protected, instance]
noncomputable def mv_polynomial.comm_semiring {R : Type u} {σ : Type u_1}  :
Equations
@[protected, instance]
noncomputable def mv_polynomial.inhabited {R : Type u} {σ : Type u_1}  :
Equations
@[protected, instance]
noncomputable def mv_polynomial.distrib_mul_action {R : Type u} {S₁ : Type v} {σ : Type u_1} [monoid R] [comm_semiring S₁] [ S₁] :
S₁)
Equations
@[protected, instance]
noncomputable def mv_polynomial.smul_zero_class {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring S₁] [ S₁] :
S₁)
Equations
@[protected, instance]
def mv_polynomial.has_faithful_smul {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring S₁] [ S₁] [ S₁] :
S₁)
@[protected, instance]
noncomputable def mv_polynomial.module {R : Type u} {S₁ : Type v} {σ : Type u_1} [semiring R] [comm_semiring S₁] [ S₁] :
S₁)
Equations
@[protected, instance]
def mv_polynomial.is_scalar_tower {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [comm_semiring S₂] [ S₁] [ S₂] [ S₂] [ S₁ S₂] :
S₁ S₂)
@[protected, instance]
def mv_polynomial.smul_comm_class {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [comm_semiring S₂] [ S₂] [ S₂] [ S₁ S₂] :
S₁ S₂)
@[protected, instance]
def mv_polynomial.is_central_scalar {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring S₁] [ S₁] [ S₁] [ S₁] :
S₁)
@[protected, instance]
noncomputable def mv_polynomial.algebra {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring S₁] [ S₁] :
S₁)
Equations
@[protected, instance]
def mv_polynomial.is_scalar_tower_right {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring S₁] [ S₁] [ S₁ S₁] :
S₁) S₁)
@[protected, instance]
def mv_polynomial.smul_comm_class_right {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring S₁] [ S₁] [ S₁ S₁] :
S₁) S₁)
@[protected, instance]
def mv_polynomial.unique {R : Type u} {σ : Type u_1} [subsingleton 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} (s : σ →₀ ) :

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} (s : σ →₀ ) (a : R) :
=
theorem mv_polynomial.mul_def {R : Type u} {σ : Type u_1} {p q : R} :
p * q = (λ (m : σ →₀ ) (a : R), (λ (n : σ →₀ ) (b : R), (mv_polynomial.monomial (m + n)) (a * b)))
noncomputable def mv_polynomial.C {R : Type u} {σ : Type u_1}  :

C a is the constant polynomial with value a

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

X n is the degree 1 monomial $X_n$.

Equations
theorem mv_polynomial.monomial_left_injective {R : Type u} {σ : Type u_1} {r : R} (hr : r 0) :
function.injective (λ (s : σ →₀ ), r)
@[simp]
theorem mv_polynomial.monomial_left_inj {R : Type u} {σ : Type u_1} {s t : σ →₀ } {r : R} (hr : r 0) :
= s = t
theorem mv_polynomial.C_apply {R : Type u} {σ : Type u_1} {a : R}  :
@[simp]
theorem mv_polynomial.C_0 {R : Type u} {σ : Type u_1}  :
@[simp]
theorem mv_polynomial.C_1 {R : Type u} {σ : Type u_1}  :
theorem mv_polynomial.C_mul_monomial {R : Type u} {σ : Type u_1} {a a' : R} {s : σ →₀ }  :
= (a * a')
@[simp]
theorem mv_polynomial.C_add {R : Type u} {σ : Type u_1} {a a' : R}  :
@[simp]
theorem mv_polynomial.C_mul {R : Type u} {σ : Type u_1} {a a' : R}  :
@[simp]
theorem mv_polynomial.C_pow {R : Type u} {σ : Type u_1} (a : R) (n : ) :
theorem mv_polynomial.C_injective (σ : Type u_1) (R : Type u_2)  :
theorem mv_polynomial.C_surjective {R : Type u_1} (σ : Type u_2) [is_empty σ] :
@[simp]
theorem mv_polynomial.C_inj {σ : Type u_1} (R : Type u_2) (r s : R) :
r = s
@[protected, instance]
def mv_polynomial.infinite_of_infinite (σ : Type u_1) (R : Type u_2) [infinite R] :
@[protected, instance]
def mv_polynomial.infinite_of_nonempty (σ : Type u_1) (R : Type u_2) [nonempty σ] [nontrivial R] :
theorem mv_polynomial.C_eq_coe_nat {R : Type u} {σ : Type u_1} (n : ) :
theorem mv_polynomial.C_mul' {R : Type u} {σ : Type u_1} {a : R} {p : R} :
= a p
theorem mv_polynomial.smul_eq_C_mul {R : Type u} {σ : Type u_1} (p : R) (a : R) :
a p =
theorem mv_polynomial.C_eq_smul_one {R : Type u} {σ : Type u_1} {a : R}  :
= a 1
theorem mv_polynomial.smul_monomial {R : Type u} {σ : Type u_1} {a : R} {s : σ →₀ } {S₁ : Type u_2} [ R] (r : S₁) :
r = (r a)
theorem mv_polynomial.X_injective {R : Type u} {σ : Type u_1} [nontrivial R] :
@[simp]
theorem mv_polynomial.X_inj {R : Type u} {σ : Type u_1} [nontrivial R] (m n : σ) :
m = n
theorem mv_polynomial.monomial_pow {R : Type u} {σ : Type u_1} {a : R} {e : } {s : σ →₀ }  :
^ e = (mv_polynomial.monomial (e s)) (a ^ e)
@[simp]
theorem mv_polynomial.monomial_mul {R : Type u} {σ : Type u_1} {s s' : σ →₀ } {a b : R} :
* b = (mv_polynomial.monomial (s + s')) (a * b)
noncomputable def mv_polynomial.monomial_one_hom (R : Type u) (σ : Type u_1)  :

λ s, monomial s 1 as a homomorphism.

Equations
@[simp]
theorem mv_polynomial.monomial_one_hom_apply {R : Type u} {σ : Type u_1} {s : σ →₀ }  :
=
theorem mv_polynomial.X_pow_eq_monomial {R : Type u} {σ : Type u_1} {e : } {n : σ}  :
= 1
theorem mv_polynomial.monomial_add_single {R : Type u} {σ : Type u_1} {a : R} {e : } {n : σ} {s : σ →₀ }  :
theorem mv_polynomial.monomial_single_add {R : Type u} {σ : Type u_1} {a : R} {e : } {n : σ} {s : σ →₀ }  :
theorem mv_polynomial.C_mul_X_pow_eq_monomial {R : Type u} {σ : Type u_1} {s : σ} {a : R} {n : } :
= a
theorem mv_polynomial.C_mul_X_eq_monomial {R : Type u} {σ : Type u_1} {s : σ} {a : R} :
@[simp]
theorem mv_polynomial.monomial_zero {R : Type u} {σ : Type u_1} {s : σ →₀ } :
= 0
@[simp]
theorem mv_polynomial.monomial_zero' {R : Type u} {σ : Type u_1}  :
@[simp]
theorem mv_polynomial.monomial_eq_zero {R : Type u} {σ : Type u_1} {s : σ →₀ } {b : R} :
= 0 b = 0
@[simp]
theorem mv_polynomial.sum_monomial_eq {R : Type u} {σ : Type u_1} {A : Type u_2} {u : σ →₀ } {r : R} {b : →₀ ) R A} (w : b u 0 = 0) :
b = b u r
@[simp]
theorem mv_polynomial.sum_C {R : Type u} {σ : Type u_1} {a : R} {A : Type u_2} {b : →₀ ) R A} (w : b 0 0 = 0) :
= b 0 a
theorem mv_polynomial.monomial_sum_one {R : Type u} {σ : Type u_1} {α : 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} {α : Type u_2} (s : finset α) (f : α σ →₀ ) (a : R) :
(mv_polynomial.monomial (s.sum (λ (i : α), f i))) a = * s.prod (λ (i : α), (mv_polynomial.monomial (f i)) 1)
theorem mv_polynomial.monomial_finsupp_sum_index {R : Type u} {σ : Type u_1} {α : Type u_2} {β : Type u_3} [has_zero β] (f : α →₀ β) (g : α β σ →₀ ) (a : R) :
(mv_polynomial.monomial (f.sum g)) a = * f.prod (λ (a : α) (b : β), (mv_polynomial.monomial (g a b)) 1)
theorem mv_polynomial.monomial_eq_monomial_iff {R : Type u} {α : Type u_1} (a₁ a₂ : α →₀ ) (b₁ b₂ : R) :
b₁ = b₂ a₁ = a₂ b₁ = b₂ b₁ = 0 b₂ = 0
theorem mv_polynomial.monomial_eq {R : Type u} {σ : Type u_1} {a : R} {s : σ →₀ }  :
= * s.prod (λ (n : σ) (e : ), ^ e)
theorem mv_polynomial.induction_on_monomial {R : Type u} {σ : Type u_1} {M : Prop} (h_C : (a : R), M ) (h_X : (p : R) (n : σ), M p M (p * ) (s : σ →₀ ) (a : R) :
M a)
theorem mv_polynomial.induction_on' {R : Type u} {σ : Type u_1} {P : Prop} (p : R) (h1 : (u : σ →₀ ) (a : R), P a)) (h2 : (p q : 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} {M : Prop} (p : R) (h_C : (a : R), M ) (h_add_weak : (a : σ →₀ ) (b : R) (f : →₀ ) →₀ R), a f.support b 0 M f M 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} {M : Prop} (p : R) (h_C : (a : R), M ) (h_add_weak : (a : σ →₀ ) (b : R) (f : →₀ ) →₀ R), a f.support b 0 M f M b) M b + f)) (h_X : (p : R) (n : σ), M p M (p * ) :
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} {M : Prop} (p : R) (h_C : (a : R), M ) (h_add : (p q : R), M p M q M (p + q)) (h_X : (p : R) (n : σ), M p M (p * ) :
M p

Analog of polynomial.induction_on.

theorem mv_polynomial.ring_hom_ext {R : Type u} {σ : Type u_1} {A : Type u_2} [semiring A] {f g : →+* A} (hC : (r : R), f = g ) (hX : (i : σ), f = g ) :
f = g
@[ext]
theorem mv_polynomial.ring_hom_ext' {R : Type u} {σ : Type u_1} {A : Type u_2} [semiring A] {f g : →+* A} (hC : = ) (hX : (i : σ), f = g ) :
f = g
theorem mv_polynomial.hom_eq_hom {R : Type u} {S₂ : Type w} {σ : Type u_1} [semiring S₂] (f g : →+* S₂) (hC : = ) (hX : (n : σ), f = g ) (p : R) :
f p = g p
theorem mv_polynomial.is_id {R : Type u} {σ : Type u_1} (f : →+* ) (hC : = mv_polynomial.C) (hX : (n : σ), f = ) (p : R) :
f p = p
@[ext]
theorem mv_polynomial.alg_hom_ext' {R : Type u} {σ : Type u_1} {A : Type u_2} {B : Type u_3} [ A] [ B] {f g : →ₐ[R] B} (h₁ : f.comp A)) = g.comp A))) (h₂ : (i : σ), f = g ) :
f = g
@[ext]
theorem mv_polynomial.alg_hom_ext {R : Type u} {σ : Type u_1} {A : Type u_2} [semiring A] [ A] {f g : →ₐ[R] A} (hf : (i : σ), f = g ) :
f = g
@[simp]
theorem mv_polynomial.alg_hom_C {R : Type u} {σ : Type u_1} (f : →ₐ[R] ) (r : R) :
@[simp]
theorem mv_polynomial.adjoin_range_X {R : Type u} {σ : Type u_1}  :
@[ext]
theorem mv_polynomial.linear_map_ext {R : Type u} {σ : Type u_1} {M : Type u_2} [ M] {f g : →ₗ[R] M} (h : (s : σ →₀ ), = ) :
f = g
def mv_polynomial.support {R : Type u} {σ : Type u_1} (p : R) :

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

Equations
theorem mv_polynomial.finsupp_support_eq_support {R : Type u} {σ : Type u_1} (p : R) :
theorem mv_polynomial.support_monomial {R : Type u} {σ : Type u_1} {a : R} {s : σ →₀ } [decidable (a = 0)] :
a).support = ite (a = 0) {s}
theorem mv_polynomial.support_monomial_subset {R : Type u} {σ : Type u_1} {a : R} {s : σ →₀ }  :
a).support {s}
theorem mv_polynomial.support_add {R : Type u} {σ : Type u_1} {p q : R} [decidable_eq σ] :
theorem mv_polynomial.support_X {R : Type u} {σ : Type u_1} {n : σ} [nontrivial R] :
= 1}
theorem mv_polynomial.support_X_pow {R : Type u} {σ : Type u_1} [nontrivial R] (s : σ) (n : ) :
^ n).support = n}
@[simp]
theorem mv_polynomial.support_zero {R : Type u} {σ : Type u_1}  :
theorem mv_polynomial.support_smul {R : Type u} {σ : Type u_1} {S₁ : Type u_2} [ R] {a : S₁} {f : R} :
theorem mv_polynomial.support_sum {R : Type u} {σ : Type u_1} {α : Type u_2} [decidable_eq σ] {s : finset α} {f : α } :
(s.sum (λ (x : α), f x)).support s.bUnion (λ (x : α), (f x).support)
def mv_polynomial.coeff {R : Type u} {σ : Type u_1} (m : σ →₀ ) (p : R) :
R

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

Equations
@[simp]
theorem mv_polynomial.mem_support_iff {R : Type u} {σ : Type u_1} {p : R} {m : σ →₀ } :
theorem mv_polynomial.not_mem_support_iff {R : Type u} {σ : Type u_1} {p : R} {m : σ →₀ } :
theorem mv_polynomial.sum_def {R : Type u} {σ : Type u_1} {A : Type u_2} {p : R} {b : →₀ ) R A} :
b = p.support.sum (λ (m : σ →₀ ), b m p))
theorem mv_polynomial.support_mul {R : Type u} {σ : Type u_1} [decidable_eq σ] (p q : R) :
(p * q).support p.support.bUnion (λ (a : σ →₀ ), q.support.bUnion (λ (b : σ →₀ ), {a + b}))
@[ext]
theorem mv_polynomial.ext {R : Type u} {σ : Type u_1} (p q : R) :
( (m : σ →₀ ), p = q
theorem mv_polynomial.ext_iff {R : Type u} {σ : Type u_1} (p q : R) :
p = q (m : σ →₀ ),
@[simp]
theorem mv_polynomial.coeff_add {R : Type u} {σ : Type u_1} (m : σ →₀ ) (p q : R) :
(p + q) =
@[simp]
theorem mv_polynomial.coeff_smul {R : Type u} {σ : Type u_1} {S₁ : Type u_2} [ R] (m : σ →₀ ) (c : S₁) (p : R) :
(c p) = c
@[simp]
theorem mv_polynomial.coeff_zero {R : Type u} {σ : Type u_1} (m : σ →₀ ) :
= 0
@[simp]
theorem mv_polynomial.coeff_zero_X {R : Type u} {σ : Type u_1} (i : σ) :
def mv_polynomial.coeff_add_monoid_hom {R : Type u} {σ : Type u_1} (m : σ →₀ ) :
→+ R

mv_polynomial.coeff m but promoted to an add_monoid_hom.

Equations
@[simp]
theorem mv_polynomial.coeff_add_monoid_hom_apply {R : Type u} {σ : Type u_1} (m : σ →₀ ) (p : R) :
theorem mv_polynomial.coeff_sum {R : Type u} {σ : Type u_1} {X : Type u_2} (s : finset X) (f : X ) (m : σ →₀ ) :
(s.sum (λ (x : X), f x)) = s.sum (λ (x : X), (f x))
theorem mv_polynomial.monic_monomial_eq {R : Type u} {σ : Type u_1} (m : σ →₀ ) :
= m.prod (λ (n : σ) (e : ), ^ e)
@[simp]
theorem mv_polynomial.coeff_monomial {R : Type u} {σ : Type u_1} [decidable_eq σ] (m n : σ →₀ ) (a : R) :
= ite (n = m) a 0
@[simp]
theorem mv_polynomial.coeff_C {R : Type u} {σ : Type u_1} [decidable_eq σ] (m : σ →₀ ) (a : R) :
= ite (0 = m) a 0
theorem mv_polynomial.coeff_one {R : Type u} {σ : Type u_1} [decidable_eq σ] (m : σ →₀ ) :
= ite (0 = m) 1 0
@[simp]
theorem mv_polynomial.coeff_zero_C {R : Type u} {σ : Type u_1} (a : R) :
@[simp]
theorem mv_polynomial.coeff_zero_one {R : Type u} {σ : Type u_1}  :
= 1
theorem mv_polynomial.coeff_X_pow {R : Type u} {σ : Type u_1} [decidable_eq σ] (i : σ) (m : σ →₀ ) (k : ) :
^ k) = ite k = m) 1 0
theorem mv_polynomial.coeff_X' {R : Type u} {σ : Type u_1} [decidable_eq σ] (i : σ) (m : σ →₀ ) :
= ite 1 = m) 1 0
@[simp]
theorem mv_polynomial.coeff_X {R : Type u} {σ : Type u_1} (i : σ) :
= 1
@[simp]
theorem mv_polynomial.coeff_C_mul {R : Type u} {σ : Type u_1} (m : σ →₀ ) (a : R) (p : R) :
* p) = a *
theorem mv_polynomial.coeff_mul {R : Type u} {σ : Type u_1} (p q : R) (n : σ →₀ ) :
(p * q) = n.antidiagonal.sum (λ (x : →₀ ) × →₀ )),
@[simp]
theorem mv_polynomial.coeff_mul_monomial {R : Type u} {σ : Type u_1} (m s : σ →₀ ) (r : R) (p : R) :
mv_polynomial.coeff (m + s) (p * r) = * r
@[simp]
theorem mv_polynomial.coeff_monomial_mul {R : Type u} {σ : Type u_1} (m s : σ →₀ ) (r : R) (p : R) :
mv_polynomial.coeff (s + m) r * p) = r *
@[simp]
theorem mv_polynomial.coeff_mul_X {R : Type u} {σ : Type u_1} (m : σ →₀ ) (s : σ) (p : R) :
@[simp]
theorem mv_polynomial.coeff_X_mul {R : Type u} {σ : Type u_1} (m : σ →₀ ) (s : σ) (p : R) :
@[simp]
theorem mv_polynomial.support_mul_X {R : Type u} {σ : Type u_1} (s : σ) (p : R) :
(p * .support =
@[simp]
theorem mv_polynomial.support_X_mul {R : Type u} {σ : Type u_1} (s : σ) (p : R) :
* p).support =
@[simp]
theorem mv_polynomial.support_smul_eq {R : Type u} {σ : Type u_1} {S₁ : Type u_2} [semiring S₁] [module S₁ R] [ R] {a : S₁} (h : a 0) (p : R) :
theorem mv_polynomial.coeff_mul_monomial' {R : Type u} {σ : Type u_1} (m s : σ →₀ ) (r : R) (p : R) :
(p * r) = ite (s m) (mv_polynomial.coeff (m - s) p * r) 0
theorem mv_polynomial.coeff_monomial_mul' {R : Type u} {σ : Type u_1} (m s : σ →₀ ) (r : R) (p : R) :
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} [decidable_eq σ] (m : σ →₀ ) (s : σ) (p : R) :
(p * = ite (s m.support) (mv_polynomial.coeff (m - 1) p) 0
theorem mv_polynomial.coeff_X_mul' {R : Type u} {σ : Type u_1} [decidable_eq σ] (m : σ →₀ ) (s : σ) (p : R) :
* p) = ite (s m.support) (mv_polynomial.coeff (m - 1) p) 0
theorem mv_polynomial.eq_zero_iff {R : Type u} {σ : Type u_1} {p : R} :
p = 0 (d : σ →₀ ), = 0
theorem mv_polynomial.ne_zero_iff {R : Type u} {σ : Type u_1} {p : R} :
p 0 (d : σ →₀ ), 0
@[simp]
theorem mv_polynomial.support_eq_empty {R : Type u} {σ : Type u_1} {p : R} :
p = 0
theorem mv_polynomial.exists_coeff_ne_zero {R : Type u} {σ : Type u_1} {p : R} (h : p 0) :
(d : σ →₀ ), 0
theorem mv_polynomial.C_dvd_iff_dvd_coeff {R : Type u} {σ : Type u_1} (r : R) (φ : R) :
(i : σ →₀ ), r
def mv_polynomial.constant_coeff {R : Type u} {σ : Type u_1}  :

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

Equations
theorem mv_polynomial.constant_coeff_eq {R : Type u} {σ : Type u_1}  :
@[simp]
theorem mv_polynomial.constant_coeff_C {R : Type u} (σ : Type u_1) (r : R) :
@[simp]
theorem mv_polynomial.constant_coeff_X (R : Type u) {σ : Type u_1} (i : σ) :
@[simp]
theorem mv_polynomial.constant_coeff_smul {S₁ : Type v} {σ : Type u_1} [comm_semiring S₁] {R : Type u_2} [ S₁] (a : R) (f : S₁) :
theorem mv_polynomial.constant_coeff_monomial {R : Type u} {σ : Type u_1} [decidable_eq σ] (d : σ →₀ ) (r : R) :
= ite (d = 0) r 0
@[simp]
theorem mv_polynomial.constant_coeff_comp_C (R : Type u) (σ : Type u_1)  :
@[simp]
@[simp]
theorem mv_polynomial.support_sum_monomial_coeff {R : Type u} {σ : Type u_1} (p : R) :
p.support.sum (λ (v : σ →₀ ), p)) = p
theorem mv_polynomial.as_sum {R : Type u} {σ : Type u_1} (p : R) :
p = p.support.sum (λ (v : σ →₀ ), p))
def mv_polynomial.eval₂ {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring S₁] (f : R →+* S₁) (g : σ S₁) (p : R) :
S₁

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

Equations
theorem mv_polynomial.eval₂_eq {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring S₁] (g : R →+* S₁) (x : σ S₁) (f : R) :
f = f.support.sum (λ (d : σ →₀ ), g f) * d.support.prod (λ (i : σ), x i ^ d i))
theorem mv_polynomial.eval₂_eq' {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring S₁] [fintype σ] (g : R →+* S₁) (x : σ S₁) (f : R) :
f = f.support.sum (λ (d : σ →₀ ), g 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 S₁] (f : R →+* S₁) (g : σ S₁) :
0 = 0
@[simp]
theorem mv_polynomial.eval₂_add {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring S₁] {p q : R} (f : R →+* S₁) (g : σ S₁) :
(p + q) = p + q
@[simp]
theorem mv_polynomial.eval₂_monomial {R : Type u} {S₁ : Type v} {σ : Type u_1} {a : R} {s : σ →₀ } [comm_semiring S₁] (f : R →+* S₁) (g : σ 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 S₁] (f : R →+* S₁) (g : σ S₁) (a : R) :
= f a
@[simp]
theorem mv_polynomial.eval₂_one {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring S₁] (f : R →+* S₁) (g : σ S₁) :
1 = 1
@[simp]
theorem mv_polynomial.eval₂_X {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring S₁] (f : R →+* S₁) (g : σ S₁) (n : σ) :
= g n
theorem mv_polynomial.eval₂_mul_monomial {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring S₁] {p : R} (f : R →+* S₁) (g : σ S₁) {s : σ →₀ } {a : R} :
(p * a) = 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 S₁] {p : R} (f : R →+* S₁) (g : σ S₁) :
(p * = p * f a
@[simp]
theorem mv_polynomial.eval₂_mul {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring S₁] {q : R} (f : R →+* S₁) (g : σ S₁) {p : R} :
(p * q) = p * q
@[simp]
theorem mv_polynomial.eval₂_pow {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring S₁] (f : R →+* S₁) (g : σ S₁) {p : R} {n : } :
(p ^ n) = p ^ n
def mv_polynomial.eval₂_hom {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring S₁] (f : R →+* S₁) (g : σ S₁) :
→+* S₁

mv_polynomial.eval₂ as a ring_hom.

Equations
@[simp]
theorem mv_polynomial.coe_eval₂_hom {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring S₁] (f : R →+* S₁) (g : σ S₁) :
theorem mv_polynomial.eval₂_hom_congr {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring S₁] {f₁ f₂ : R →+* S₁} {g₁ g₂ : σ S₁} {p₁ p₂ : R} :
f₁ = f₂ g₁ = g₂ p₁ = p₂ g₁) p₁ = g₂) p₂
@[simp]
theorem mv_polynomial.eval₂_hom_C {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring S₁] (f : R →+* S₁) (g : σ S₁) (r : R) :
= f r
@[simp]
theorem mv_polynomial.eval₂_hom_X' {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring S₁] (f : R →+* S₁) (g : σ S₁) (i : σ) :
= g i
@[simp]
theorem mv_polynomial.comp_eval₂_hom {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [comm_semiring S₁] [comm_semiring S₂] (f : R →+* S₁) (g : σ S₁) (φ : S₁ →+* S₂) :
φ.comp = (λ (i : σ), φ (g i))
theorem mv_polynomial.map_eval₂_hom {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [comm_semiring S₁] [comm_semiring S₂] (f : R →+* S₁) (g : σ S₁) (φ : S₁ →+* S₂) (p : R) :
φ ( 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 S₁] (f : R →+* S₁) (g : σ S₁) (d : σ →₀ ) (r : R) :
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 S₁] {S₂ : Type u_2} [comm_semiring S₂] (k : S₁ →+* S₂) (f : R →+* S₁) (g : σ S₁) (p : R) :
@[simp]
theorem mv_polynomial.eval₂_eta {R : Type u} {σ : Type u_1} (p : R) :
theorem mv_polynomial.eval₂_congr {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring S₁] {p : R} (f : R →+* S₁) (g₁ g₂ : σ S₁) (h : {i : σ} {c : σ →₀ }, i c.support 0 g₁ i = g₂ i) :
p = p
@[simp]
theorem mv_polynomial.eval₂_prod {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [comm_semiring S₁] (f : R →+* S₁) (g : σ S₁) (s : finset S₂) (p : S₂ ) :
(s.prod (λ (x : S₂), p x)) = s.prod (λ (x : S₂), (p x))
@[simp]
theorem mv_polynomial.eval₂_sum {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [comm_semiring S₁] (f : R →+* S₁) (g : σ S₁) (s : finset S₂) (p : S₂ ) :
(s.sum (λ (x : S₂), p x)) = s.sum (λ (x : S₂), (p x))
theorem mv_polynomial.eval₂_assoc {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [comm_semiring S₁] (f : R →+* S₁) (g : σ S₁) (q : S₂ ) (p : R) :
(λ (t : S₂), (q t)) p =
def mv_polynomial.eval {R : Type u} {σ : Type u_1} (f : σ R) :

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

Equations
theorem mv_polynomial.eval_eq {R : Type u} {σ : Type u_1} (x : σ R) (f : R) :
f = f.support.sum (λ (d : σ →₀ ), * d.support.prod (λ (i : σ), x i ^ d i))
theorem mv_polynomial.eval_eq' {R : Type u} {σ : Type u_1} [fintype σ] (x : σ R) (f : R) :
f = f.support.sum (λ (d : σ →₀ ), * finset.univ.prod (λ (i : σ), x i ^ d i))
theorem mv_polynomial.eval_monomial {R : Type u} {σ : Type u_1} {a : R} {s : σ →₀ } {f : σ R} :
a) = a * s.prod (λ (n : σ) (e : ), f n ^ e)
@[simp]
theorem mv_polynomial.eval_C {R : Type u} {σ : Type u_1} {f : σ R} (a : R) :
= a
@[simp]
theorem mv_polynomial.eval_X {R : Type u} {σ : Type u_1} {f : σ R} (n : σ) :
= f n
@[simp]
theorem mv_polynomial.smul_eval {R : Type u} {σ : Type u_1} (x : σ R) (p : R) (s : R) :
(s p) = s * p
theorem mv_polynomial.eval_sum {R : Type u} {σ : Type u_1} {ι : Type u_2} (s : finset ι) (f : ι ) (g : σ R) :
(s.sum (λ (i : ι), f i)) = s.sum (λ (i : ι), (f i))
theorem mv_polynomial.eval_prod {R : Type u} {σ : Type u_1} {ι : Type u_2} (s : finset ι) (f : ι ) (g : σ R) :
(s.prod (λ (i : ι), f i)) = s.prod (λ (i : ι), (f i))
theorem mv_polynomial.eval_assoc {R : Type u} {σ : Type u_1} {τ : Type u_2} (f : σ ) (g : τ R) (p : R) :
@[simp]
theorem mv_polynomial.eval₂_id {R : Type u} {σ : Type u_1} (p : R) (g : σ R) :
p = p
theorem mv_polynomial.eval_eval₂ {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring S₁] {τ : Type u_2} (f : R →+* S₁) (g : σ S₁) (p : R) (x : τ S₁) :
p) = (λ (s : σ), (g s)) p
noncomputable def mv_polynomial.map {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring S₁] (f : R →+* S₁) :
→+* 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 S₁] (f : R →+* S₁) (s : σ →₀ ) (a : R) :
a) = (f a)
@[simp]
theorem mv_polynomial.map_C {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring S₁] (f : R →+* S₁) (a : R) :
@[simp]
theorem mv_polynomial.map_X {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring S₁] (f : R →+* S₁) (n : σ) :
theorem mv_polynomial.map_id {R : Type u} {σ : Type u_1} (p : R) :
p = p
theorem mv_polynomial.map_map {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [comm_semiring S₁] (f : R →+* S₁) [comm_semiring S₂] (g : S₁ →+* S₂) (p : R) :
theorem mv_polynomial.eval₂_eq_eval_map {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring S₁] (f : R →+* S₁) (g : σ S₁) (p : R) :
p = ( p)
theorem mv_polynomial.eval₂_comp_right {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring S₁] {S₂ : Type u_2} [comm_semiring S₂] (k : S₁ →+* S₂) (f : R →+* S₁) (g : σ S₁) (p : R) :
k p) = (k g) ( p)
theorem mv_polynomial.map_eval₂ {R : Type u} {S₁ : Type v} {S₂ : Type w} {S₃ : Type x} [comm_semiring S₁] (f : R →+* S₁) (g : S₂ R) (p : R) :
= ( p)
theorem mv_polynomial.coeff_map {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring S₁] (f : R →+* S₁) (p : R) (m : σ →₀ ) :
( p) = f p)
theorem mv_polynomial.map_injective {R : Type u} {S₁ : Type v} {σ : Type u_1} [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 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 S₁] {f : R →+* S₁} {g : S₁ →+* R} (hf : 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 S₁] {f : R →+* S₁} {g : S₁ →+* R} (hf : 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 S₁] (f : R →+* S₁) (g : σ S₁) (p : R) :
( p) = p
@[simp]
theorem mv_polynomial.eval₂_map {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [comm_semiring S₁] [comm_semiring S₂] (f : R →+* S₁) (g : σ S₂) (φ : S₁ →+* S₂) (p : R) :
@[simp]
theorem mv_polynomial.eval₂_hom_map_hom {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [comm_semiring S₁] [comm_semiring S₂] (f : R →+* S₁) (g : σ S₂) (φ : S₁ →+* S₂) (p : R) :
@[simp]
theorem mv_polynomial.constant_coeff_map {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring S₁] (f : R →+* S₁) (φ : R) :
theorem mv_polynomial.constant_coeff_comp_map {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring S₁] (f : R →+* S₁) :
theorem mv_polynomial.support_map_subset {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring S₁] (f : R →+* S₁) (p : R) :
theorem mv_polynomial.support_map_of_injective {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring S₁] (p : R) {f : R →+* S₁} (hf : function.injective f) :
theorem mv_polynomial.C_dvd_iff_map_hom_eq_zero {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring S₁] (q : R →+* S₁) (r : R) (hr : (r' : R), q r' = 0 r r') (φ : R) :
φ = 0
theorem mv_polynomial.map_map_range_eq_iff {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring S₁] (f : R →+* S₁) (g : S₁ R) (hg : g 0 = 0) (φ : S₁) :
hg φ) = φ (d : σ →₀ ), f (g φ)) =
@[simp]
theorem mv_polynomial.map_alg_hom_apply {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [comm_semiring S₁] [comm_semiring S₂] [ S₁] [ S₂] (f : S₁ →ₐ[R] S₂) (ᾰ : S₁) :
=
noncomputable def mv_polynomial.map_alg_hom {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [comm_semiring S₁] [comm_semiring S₂] [ S₁] [ S₂] (f : S₁ →ₐ[R] S₂) :
S₁ →ₐ[R] S₂

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

Equations
@[simp]
theorem mv_polynomial.map_alg_hom_id {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring S₁] [ S₁] :
= 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 S₁] [comm_semiring S₂] [ S₁] [ S₂] (f : S₁ →ₐ[R] S₂) :

### The algebra of multivariate polynomials #

theorem mv_polynomial.algebra_map_apply {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring S₁] [ S₁] (r : R) :
S₁)) r = mv_polynomial.C ( S₁) r)
noncomputable def mv_polynomial.aeval {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring S₁] [ S₁] (f : σ S₁) :
→ₐ[R] S₁

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

Equations
theorem mv_polynomial.aeval_def {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring S₁] [ S₁] (f : σ S₁) (p : R) :
p = f p
theorem mv_polynomial.aeval_eq_eval₂_hom {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring S₁] [ S₁] (f : σ S₁) (p : R) :
p = f) p
@[simp]
theorem mv_polynomial.aeval_X {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring S₁] [ S₁] (f : σ S₁) (s : σ) :
= f s
@[simp]
theorem mv_polynomial.aeval_C {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring S₁] [ S₁] (f : σ S₁) (r : R) :
= S₁) r
theorem mv_polynomial.aeval_unique {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring S₁] [ S₁] (φ : →ₐ[R] S₁) :
theorem mv_polynomial.aeval_X_left {R : Type u} {σ : Type u_1}  :
theorem mv_polynomial.aeval_X_left_apply {R : Type u} {σ : Type u_1} (p : R) :
theorem mv_polynomial.comp_aeval {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring S₁] [ S₁] (f : σ S₁) {B : Type u_2} [ B] (φ : S₁ →ₐ[R] B) :
φ.comp = mv_polynomial.aeval (λ (i : σ), φ (f i))
@[simp]
theorem mv_polynomial.map_aeval {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring S₁] [ S₁] {B : Type u_2} (g : σ S₁) (φ : S₁ →+* B) (p : R) :
φ ( p) = (mv_polynomial.eval₂_hom (φ.comp S₁)) (λ (i : σ), φ (g i))) p
@[simp]
theorem mv_polynomial.eval₂_hom_zero {R : Type u} {S₂ : Type w} {σ : Type u_1} [comm_semiring S₂] (f : R →+* S₂) :
@[simp]
theorem mv_polynomial.eval₂_hom_zero' {R : Type u} {S₂ : Type w} {σ : Type u_1} [comm_semiring S₂] (f : R →+* S₂) :
(λ (_x : σ), 0) =
theorem mv_polynomial.eval₂_hom_zero_apply {R : Type u} {S₂ : Type w} {σ : Type u_1} [comm_semiring S₂] (f : R →+* S₂) (p : R) :
p =
theorem mv_polynomial.eval₂_hom_zero'_apply {R : Type u} {S₂ : Type w} {σ : Type u_1} [comm_semiring S₂] (f : R →+* S₂) (p : R) :
(λ (_x : σ), 0)) p =
@[simp]
theorem mv_polynomial.eval₂_zero_apply {R : Type u} {S₂ : Type w} {σ : Type u_1} [comm_semiring S₂] (f : R →+* S₂) (p : R) :
@[simp]
theorem mv_polynomial.eval₂_zero'_apply {R : Type u} {S₂ : Type w} {σ : Type u_1} [comm_semiring S₂] (f : R →+* S₂) (p : R) :
(λ (_x : σ), 0) p =
@[simp]
theorem mv_polynomial.aeval_zero {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring S₁] [ S₁] (p : R) :
p = S₁)
@[simp]
theorem mv_polynomial.aeval_zero' {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring S₁] [ S₁] (p : R) :
(mv_polynomial.aeval (λ (_x : σ), 0)) p = S₁)
@[simp]
theorem mv_polynomial.eval_zero {R : Type u} {σ : Type u_1}  :
@[simp]
theorem mv_polynomial.eval_zero' {R : Type u} {σ : Type u_1}  :
theorem mv_polynomial.aeval_monomial {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring S₁] [ S₁] (g : σ S₁) (d : σ →₀ ) (r : R) :
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 S₂] (f : R →+* S₂) (g : σ S₂) (φ : R) (h : (d : σ →₀ ), 0 ( (i : σ) (H : i d.support), g i = 0)) :
φ = 0
theorem mv_polynomial.aeval_eq_zero {R : Type u} {S₂ : Type w} {σ : Type u_1} [comm_semiring S₂] [ S₂] (f : σ S₂) (φ : R) (h : (d : σ →₀ ), 0 ( (i : σ) (H : i d.support), f i = 0)) :
φ = 0
theorem mv_polynomial.aeval_sum {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring S₁] [ S₁] (f : σ S₁) {ι : Type u_2} (s : finset ι) (φ : ι ) :
(s.sum (λ (i : ι), φ i)) = s.sum (λ (i : ι), (φ i))
theorem mv_polynomial.aeval_prod {R : Type u} {S₁ : Type v} {σ : Type u_1} [comm_semiring S₁] [ S₁] (f : σ S₁) {ι : Type u_2} (s : finset ι) (φ : ι ) :
(s.prod (λ (i : ι), φ i)) = s.prod (λ (i : ι), (φ i))
theorem algebra.adjoin_range_eq_range_aeval (R : Type u) {S₁ : Type v} {σ : Type u_1} [comm_semiring S₁] [ S₁] (f : σ S₁) :
(set.range f) =
theorem algebra.adjoin_eq_range (R : Type u) {S₁ : Type v} [comm_semiring S₁] [ S₁] (s : set S₁) :
noncomputable def mv_polynomial.aeval_tower {R : Type u} {σ : Type u_1} {S : Type u_2} {A : Type u_3} [ R] [ A] (f : R →ₐ[S] A) (x : σ A) :

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

Equations
@[simp]
theorem mv_polynomial.aeval_tower_X {R : Type u} {σ : Type u_1} {S : Type u_2} {A : Type u_3} [ R] [ A] (g : R →ₐ[S] A) (y : σ A) (i : σ) :
= y i
@[simp]
theorem mv_polynomial.aeval_tower_C {R : Type u} {σ : Type u_1} {S : Type u_2} {A : Type u_3} [ R] [ A] (g : R →ₐ[S] A) (y : σ A) (x : R) :
= g x
@[simp]
theorem mv_polynomial.aeval_tower_comp_C {R : Type u} {σ : Type u_1} {S : Type u_2} {A : Type u_3} [ R] [ A] (g : R →ₐ[S] A) (y : σ A) :
@[simp]
theorem mv_polynomial.aeval_tower_algebra_map {R : Type u} {σ : Type u_1} {S : Type u_2} {A : Type u_3} [ R] [ A] (g : R →ₐ[S] A) (y : σ A) (x : R) :
( R)) x) = g x
@[simp]
theorem mv_polynomial.aeval_tower_comp_algebra_map {R : Type u} {σ : Type u_1} {S : Type u_2} {A : Type u_3} [ R] [ A] (g : R →ₐ[S] A) (y : σ A) :
R)) = g
theorem mv_polynomial.aeval_tower_to_alg_hom {R : Type u} {σ : Type u_1} {S : Type u_2} {A : Type u_3} [ R] [ A] (g : R →ₐ[S] A) (y : σ A) (x : R) :
( R)) x) = g x
@[simp]
theorem mv_polynomial.aeval_tower_comp_to_alg_hom {R : Type u} {σ : Type u_1} {S : Type u_2} {A : Type u_3} [ R] [ A] (g : R →ₐ[S] A) (y : σ A) :
R)) = g
@[simp]
theorem mv_polynomial.aeval_tower_id {σ : Type u_1} {S : Type u_2}  :
@[simp]
theorem mv_polynomial.aeval_tower_of_id {σ : Type u_1} {S : Type u_2} {A : Type u_3} [ A] :
theorem mv_polynomial.eval₂_mem {R : Type u} {σ : Type u_1} {S : Type u_2} {subS : Type u_3} [set_like subS S] [ S] {f : R →+* S} {p : R} {s : subS} (hs : (i : σ →₀ ), i p.support f p) s) {v : σ S} (hv : (i : σ), v i s) :
p s
theorem mv_polynomial.eval_mem {σ : Type u_1} {S : Type u_2} {subS : Type u_3} [set_like subS S] [ S] {p : S} {s : subS} (hs : (i : σ →₀ ), i p.support s) {v : σ S} (hv : (i : σ), v i s) :
p s