# 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 MvPolynomial σ 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* [CommSemiring R] (the coefficients)
• s : σ →₀ ℕ, a function from σ to ℕ which is zero away from a finite set. This will give rise to a monomial in MvPolynomial σ R which mathematicians might call X^s
• a : R
• i : σ, with corresponding monomial X i, often denoted X_i by mathematicians
• p : MvPolynomial σ R

### Definitions #

• MvPolynomial σ 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 MvPolynomial σ 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 MvPolynomial (σ : 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
instance MvPolynomial.decidableEqMvPolynomial {R : Type u} {σ : Type u_1} [] [] [] :
Equations
• MvPolynomial.decidableEqMvPolynomial = Finsupp.decidableEq
instance MvPolynomial.commSemiring {R : Type u} {σ : Type u_1} [] :
Equations
instance MvPolynomial.inhabited {R : Type u} {σ : Type u_1} [] :
Equations
• MvPolynomial.inhabited = { default := 0 }
instance MvPolynomial.distribuMulAction {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [] [] :
Equations
instance MvPolynomial.smulZeroClass {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [] :
Equations
instance MvPolynomial.faithfulSMul {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [] [FaithfulSMul R S₁] :
Equations
instance MvPolynomial.module {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [] [Module R S₁] :
Module R (MvPolynomial σ S₁)
Equations
instance MvPolynomial.isScalarTower {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [] [SMul R S₁] [] [SMulZeroClass S₁ S₂] [IsScalarTower R S₁ S₂] :
IsScalarTower R S₁ (MvPolynomial σ S₂)
Equations
instance MvPolynomial.smulCommClass {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [] [] [SMulZeroClass S₁ S₂] [SMulCommClass R S₁ S₂] :
SMulCommClass R S₁ (MvPolynomial σ S₂)
Equations
instance MvPolynomial.isCentralScalar {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [] [] [] :
Equations
instance MvPolynomial.algebra {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [] [Algebra R S₁] :
Algebra R (MvPolynomial σ S₁)
Equations
instance MvPolynomial.isScalarTower_right {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [DistribSMul R S₁] [IsScalarTower R S₁ S₁] :
Equations
instance MvPolynomial.smulCommClass_right {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [DistribSMul R S₁] [SMulCommClass R S₁ S₁] :
Equations
instance MvPolynomial.unique {R : Type u} {σ : Type u_1} [] [] :

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

Equations
def MvPolynomial.monomial {R : Type u} {σ : Type u_1} [] (s : σ →₀ ) :

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

Equations
Instances For
theorem MvPolynomial.single_eq_monomial {R : Type u} {σ : Type u_1} [] (s : σ →₀ ) (a : R) :
=
theorem MvPolynomial.mul_def {R : Type u} {σ : Type u_1} [] {p : } {q : } :
p * q = Finsupp.sum p fun (m : σ →₀ ) (a : R) => Finsupp.sum q fun (n : σ →₀ ) (b : R) => (MvPolynomial.monomial (m + n)) (a * b)
def MvPolynomial.C {R : Type u} {σ : Type u_1} [] :

C a is the constant polynomial with value a

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem MvPolynomial.algebraMap_eq (R : Type u) (σ : Type u_1) [] :
algebraMap R () = MvPolynomial.C
def MvPolynomial.X {R : Type u} {σ : Type u_1} [] (n : σ) :

X n is the degree 1 monomial $X_n$.

Equations
• = () 1
Instances For
theorem MvPolynomial.monomial_left_injective {R : Type u} {σ : Type u_1} [] {r : R} (hr : r 0) :
Function.Injective fun (s : σ →₀ ) =>
@[simp]
theorem MvPolynomial.monomial_left_inj {R : Type u} {σ : Type u_1} [] {s : σ →₀ } {t : σ →₀ } {r : R} (hr : r 0) :
= s = t
theorem MvPolynomial.C_apply {R : Type u} {σ : Type u_1} {a : R} [] :
MvPolynomial.C a =
theorem MvPolynomial.C_0 {R : Type u} {σ : Type u_1} [] :
MvPolynomial.C 0 = 0
theorem MvPolynomial.C_1 {R : Type u} {σ : Type u_1} [] :
MvPolynomial.C 1 = 1
theorem MvPolynomial.C_mul_monomial {R : Type u} {σ : Type u_1} {a : R} {a' : R} {s : σ →₀ } [] :
MvPolynomial.C a * a' = (a * a')
theorem MvPolynomial.C_add {R : Type u} {σ : Type u_1} {a : R} {a' : R} [] :
MvPolynomial.C (a + a') = MvPolynomial.C a + MvPolynomial.C a'
theorem MvPolynomial.C_mul {R : Type u} {σ : Type u_1} {a : R} {a' : R} [] :
MvPolynomial.C (a * a') = MvPolynomial.C a * MvPolynomial.C a'
theorem MvPolynomial.C_pow {R : Type u} {σ : Type u_1} [] (a : R) (n : ) :
MvPolynomial.C (a ^ n) = MvPolynomial.C a ^ n
theorem MvPolynomial.C_injective (σ : Type u_2) (R : Type u_3) [] :
Function.Injective MvPolynomial.C
theorem MvPolynomial.C_surjective {R : Type u_2} [] (σ : Type u_3) [] :
Function.Surjective MvPolynomial.C
@[simp]
theorem MvPolynomial.C_inj {σ : Type u_2} (R : Type u_3) [] (r : R) (s : R) :
MvPolynomial.C r = MvPolynomial.C s r = s
instance MvPolynomial.nontrivial_of_nontrivial (σ : Type u_2) (R : Type u_3) [] [] :
Equations
instance MvPolynomial.infinite_of_infinite (σ : Type u_2) (R : Type u_3) [] [] :
Equations
instance MvPolynomial.infinite_of_nonempty (σ : Type u_2) (R : Type u_3) [] [] [] :
Equations
theorem MvPolynomial.C_eq_coe_nat {R : Type u} {σ : Type u_1} [] (n : ) :
MvPolynomial.C n = n
theorem MvPolynomial.C_mul' {R : Type u} {σ : Type u_1} {a : R} [] {p : } :
MvPolynomial.C a * p = a p
theorem MvPolynomial.smul_eq_C_mul {R : Type u} {σ : Type u_1} [] (p : ) (a : R) :
a p = MvPolynomial.C a * p
theorem MvPolynomial.C_eq_smul_one {R : Type u} {σ : Type u_1} {a : R} [] :
MvPolynomial.C a = a 1
theorem MvPolynomial.smul_monomial {R : Type u} {σ : Type u_1} {a : R} {s : σ →₀ } [] {S₁ : Type u_2} [] (r : S₁) :
r = (r a)
theorem MvPolynomial.X_injective {R : Type u} {σ : Type u_1} [] [] :
Function.Injective MvPolynomial.X
@[simp]
theorem MvPolynomial.X_inj {R : Type u} {σ : Type u_1} [] [] (m : σ) (n : σ) :
m = n
theorem MvPolynomial.monomial_pow {R : Type u} {σ : Type u_1} {a : R} {e : } {s : σ →₀ } [] :
^ e = (MvPolynomial.monomial (e s)) (a ^ e)
@[simp]
theorem MvPolynomial.monomial_mul {R : Type u} {σ : Type u_1} [] {s : σ →₀ } {s' : σ →₀ } {a : R} {b : R} :
* b = (MvPolynomial.monomial (s + s')) (a * b)

fun s ↦ monomial s 1 as a homomorphism.

Equations
Instances For
@[simp]
theorem MvPolynomial.monomialOneHom_apply {R : Type u} {σ : Type u_1} {s : σ →₀ } [] :
s =
theorem MvPolynomial.X_pow_eq_monomial {R : Type u} {σ : Type u_1} {e : } {n : σ} [] :
= () 1
theorem MvPolynomial.monomial_add_single {R : Type u} {σ : Type u_1} {a : R} {e : } {n : σ} {s : σ →₀ } [] :
theorem MvPolynomial.monomial_single_add {R : Type u} {σ : Type u_1} {a : R} {e : } {n : σ} {s : σ →₀ } [] :
theorem MvPolynomial.C_mul_X_pow_eq_monomial {R : Type u} {σ : Type u_1} [] {s : σ} {a : R} {n : } :
MvPolynomial.C a * = () a
theorem MvPolynomial.C_mul_X_eq_monomial {R : Type u} {σ : Type u_1} [] {s : σ} {a : R} :
MvPolynomial.C a * = () a
theorem MvPolynomial.monomial_zero {R : Type u} {σ : Type u_1} [] {s : σ →₀ } :
= 0
@[simp]
theorem MvPolynomial.monomial_zero' {R : Type u} {σ : Type u_1} [] :
= MvPolynomial.C
@[simp]
theorem MvPolynomial.monomial_eq_zero {R : Type u} {σ : Type u_1} [] {s : σ →₀ } {b : R} :
= 0 b = 0
@[simp]
theorem MvPolynomial.sum_monomial_eq {R : Type u} {σ : Type u_1} [] {A : Type u_2} [] {u : σ →₀ } {r : R} {b : (σ →₀ )RA} (w : b u 0 = 0) :
Finsupp.sum () b = b u r
@[simp]
theorem MvPolynomial.sum_C {R : Type u} {σ : Type u_1} {a : R} [] {A : Type u_2} [] {b : (σ →₀ )RA} (w : b 0 0 = 0) :
Finsupp.sum (MvPolynomial.C a) b = b 0 a
theorem MvPolynomial.monomial_sum_one {R : Type u} {σ : Type u_1} [] {α : Type u_2} (s : ) (f : ασ →₀ ) :
(MvPolynomial.monomial (Finset.sum s fun (i : α) => f i)) 1 = Finset.prod s fun (i : α) => () 1
theorem MvPolynomial.monomial_sum_index {R : Type u} {σ : Type u_1} [] {α : Type u_2} (s : ) (f : ασ →₀ ) (a : R) :
(MvPolynomial.monomial (Finset.sum s fun (i : α) => f i)) a = MvPolynomial.C a * Finset.prod s fun (i : α) => () 1
theorem MvPolynomial.monomial_finsupp_sum_index {R : Type u} {σ : Type u_1} [] {α : Type u_2} {β : Type u_3} [Zero β] (f : α →₀ β) (g : αβσ →₀ ) (a : R) :
() a = MvPolynomial.C a * Finsupp.prod f fun (a : α) (b : β) => (MvPolynomial.monomial (g a b)) 1
theorem MvPolynomial.monomial_eq_monomial_iff {R : Type u} [] {α : Type u_2} (a₁ : α →₀ ) (a₂ : α →₀ ) (b₁ : R) (b₂ : R) :
b₁ = b₂ a₁ = a₂ b₁ = b₂ b₁ = 0 b₂ = 0
theorem MvPolynomial.monomial_eq {R : Type u} {σ : Type u_1} {a : R} {s : σ →₀ } [] :
= MvPolynomial.C a * Finsupp.prod s fun (n : σ) (e : ) =>
theorem MvPolynomial.induction_on_monomial {R : Type u} {σ : Type u_1} [] {M : Prop} (h_C : ∀ (a : R), M (MvPolynomial.C a)) (h_X : ∀ (p : ) (n : σ), M pM ()) (s : σ →₀ ) (a : R) :
M ()
theorem MvPolynomial.induction_on' {R : Type u} {σ : Type u_1} [] {P : Prop} (p : ) (h1 : ∀ (u : σ →₀ ) (a : R), P ()) (h2 : ∀ (p q : ), P pP qP (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 MvPolynomial.induction_on''' {R : Type u} {σ : Type u_1} [] {M : Prop} (p : ) (h_C : ∀ (a : R), M (MvPolynomial.C a)) (h_add_weak : ∀ (a : σ →₀ ) (b : R) (f : (σ →₀ ) →₀ R), af.supportb 0M fM ((let_fun this := ; this) + f)) :
M p

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

theorem MvPolynomial.induction_on'' {R : Type u} {σ : Type u_1} [] {M : Prop} (p : ) (h_C : ∀ (a : R), M (MvPolynomial.C a)) (h_add_weak : ∀ (a : σ →₀ ) (b : R) (f : (σ →₀ ) →₀ R), af.supportb 0M fM ()M ((let_fun this := ; this) + f)) (h_X : ∀ (p : ) (n : σ), M pM ()) :
M p

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

theorem MvPolynomial.induction_on {R : Type u} {σ : Type u_1} [] {M : Prop} (p : ) (h_C : ∀ (a : R), M (MvPolynomial.C a)) (h_add : ∀ (p q : ), M pM qM (p + q)) (h_X : ∀ (p : ) (n : σ), M pM ()) :
M p

Analog of Polynomial.induction_on.

theorem MvPolynomial.ringHom_ext {R : Type u} {σ : Type u_1} [] {A : Type u_2} [] {f : →+* A} {g : →+* A} (hC : ∀ (r : R), f (MvPolynomial.C r) = g (MvPolynomial.C r)) (hX : ∀ (i : σ), f () = g ()) :
f = g
theorem MvPolynomial.ringHom_ext' {R : Type u} {σ : Type u_1} [] {A : Type u_2} [] {f : →+* A} {g : →+* A} (hC : RingHom.comp f MvPolynomial.C = RingHom.comp g MvPolynomial.C) (hX : ∀ (i : σ), f () = g ()) :
f = g

See note [partially-applied ext lemmas].

theorem MvPolynomial.hom_eq_hom {R : Type u} {S₂ : Type w} {σ : Type u_1} [] [Semiring S₂] (f : →+* S₂) (g : →+* S₂) (hC : RingHom.comp f MvPolynomial.C = RingHom.comp g MvPolynomial.C) (hX : ∀ (n : σ), f () = g ()) (p : ) :
f p = g p
theorem MvPolynomial.is_id {R : Type u} {σ : Type u_1} [] (f : →+* ) (hC : RingHom.comp f MvPolynomial.C = MvPolynomial.C) (hX : ∀ (n : σ), f () = ) (p : ) :
f p = p
theorem MvPolynomial.algHom_ext' {R : Type u} {σ : Type u_1} [] {A : Type u_2} {B : Type u_3} [] [] [Algebra R A] [Algebra R B] {f : →ₐ[R] B} {g : →ₐ[R] B} (h₁ : AlgHom.comp f () = AlgHom.comp g ()) (h₂ : ∀ (i : σ), f () = g ()) :
f = g
theorem MvPolynomial.algHom_ext {R : Type u} {σ : Type u_1} [] {A : Type u_2} [] [Algebra R A] {f : →ₐ[R] A} {g : →ₐ[R] A} (hf : ∀ (i : σ), f () = g ()) :
f = g
@[simp]
theorem MvPolynomial.algHom_C {R : Type u} {σ : Type u_1} [] (f : →ₐ[R] ) (r : R) :
f (MvPolynomial.C r) = MvPolynomial.C r
@[simp]
theorem MvPolynomial.adjoin_range_X {R : Type u} {σ : Type u_1} [] :
theorem MvPolynomial.linearMap_ext {R : Type u} {σ : Type u_1} [] {M : Type u_2} [] [Module R M] {f : →ₗ[R] M} {g : →ₗ[R] M} (h : ∀ (s : σ →₀ ), = ) :
f = g
def MvPolynomial.support {R : Type u} {σ : Type u_1} [] (p : ) :

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

Equations
• = p.support
Instances For
theorem MvPolynomial.finsupp_support_eq_support {R : Type u} {σ : Type u_1} [] (p : ) :
p.support =
theorem MvPolynomial.support_monomial {R : Type u} {σ : Type u_1} {a : R} {s : σ →₀ } [] [h : Decidable (a = 0)] :
= if a = 0 then else {s}
theorem MvPolynomial.support_monomial_subset {R : Type u} {σ : Type u_1} {a : R} {s : σ →₀ } [] :
{s}
theorem MvPolynomial.support_add {R : Type u} {σ : Type u_1} [] {p : } {q : } [] :
theorem MvPolynomial.support_X {R : Type u} {σ : Type u_1} {n : σ} [] [] :
theorem MvPolynomial.support_X_pow {R : Type u} {σ : Type u_1} [] [] (s : σ) (n : ) :
= {}
@[simp]
theorem MvPolynomial.support_zero {R : Type u} {σ : Type u_1} [] :
theorem MvPolynomial.support_smul {R : Type u} {σ : Type u_1} [] {S₁ : Type u_2} [] {a : S₁} {f : } :
theorem MvPolynomial.support_sum {R : Type u} {σ : Type u_1} [] {α : Type u_2} [] {s : } {f : α} :
MvPolynomial.support (Finset.sum s fun (x : α) => f x) Finset.biUnion s fun (x : α) => MvPolynomial.support (f x)
def MvPolynomial.coeff {R : Type u} {σ : Type u_1} [] (m : σ →₀ ) (p : ) :
R

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

Equations
• = p m
Instances For
@[simp]
theorem MvPolynomial.mem_support_iff {R : Type u} {σ : Type u_1} [] {p : } {m : σ →₀ } :
0
theorem MvPolynomial.not_mem_support_iff {R : Type u} {σ : Type u_1} [] {p : } {m : σ →₀ } :
= 0
theorem MvPolynomial.sum_def {R : Type u} {σ : Type u_1} [] {A : Type u_2} [] {p : } {b : (σ →₀ )RA} :
= Finset.sum fun (m : σ →₀ ) => b m ()
theorem MvPolynomial.support_mul {R : Type u} {σ : Type u_1} [] [] (p : ) (q : ) :
theorem MvPolynomial.ext {R : Type u} {σ : Type u_1} [] (p : ) (q : ) :
(∀ (m : σ →₀ ), )p = q
theorem MvPolynomial.ext_iff {R : Type u} {σ : Type u_1} [] (p : ) (q : ) :
p = q ∀ (m : σ →₀ ),
@[simp]
theorem MvPolynomial.coeff_add {R : Type u} {σ : Type u_1} [] (m : σ →₀ ) (p : ) (q : ) :
@[simp]
theorem MvPolynomial.coeff_smul {R : Type u} {σ : Type u_1} [] {S₁ : Type u_2} [] (m : σ →₀ ) (C : S₁) (p : ) :
@[simp]
theorem MvPolynomial.coeff_zero {R : Type u} {σ : Type u_1} [] (m : σ →₀ ) :
= 0
@[simp]
theorem MvPolynomial.coeff_zero_X {R : Type u} {σ : Type u_1} [] (i : σ) :
@[simp]
theorem MvPolynomial.coeffAddMonoidHom_apply {R : Type u} {σ : Type u_1} [] (m : σ →₀ ) (p : ) :
def MvPolynomial.coeffAddMonoidHom {R : Type u} {σ : Type u_1} [] (m : σ →₀ ) :
→+ R

MvPolynomial.coeff m but promoted to an AddMonoidHom.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem MvPolynomial.coeff_sum {R : Type u} {σ : Type u_1} [] {X : Type u_2} (s : ) (f : X) (m : σ →₀ ) :
MvPolynomial.coeff m (Finset.sum s fun (x : X) => f x) = Finset.sum s fun (x : X) => MvPolynomial.coeff m (f x)
theorem MvPolynomial.monic_monomial_eq {R : Type u} {σ : Type u_1} [] (m : σ →₀ ) :
= Finsupp.prod m fun (n : σ) (e : ) =>
@[simp]
theorem MvPolynomial.coeff_monomial {R : Type u} {σ : Type u_1} [] [] (m : σ →₀ ) (n : σ →₀ ) (a : R) :
= if n = m then a else 0
@[simp]
theorem MvPolynomial.coeff_C {R : Type u} {σ : Type u_1} [] [] (m : σ →₀ ) (a : R) :
MvPolynomial.coeff m (MvPolynomial.C a) = if 0 = m then a else 0
theorem MvPolynomial.eq_C_of_isEmpty {R : Type u} {σ : Type u_1} [] [] (p : ) :
p = MvPolynomial.C ()
theorem MvPolynomial.coeff_one {R : Type u} {σ : Type u_1} [] [] (m : σ →₀ ) :
= if 0 = m then 1 else 0
@[simp]
theorem MvPolynomial.coeff_zero_C {R : Type u} {σ : Type u_1} [] (a : R) :
MvPolynomial.coeff 0 (MvPolynomial.C a) = a
@[simp]
theorem MvPolynomial.coeff_zero_one {R : Type u} {σ : Type u_1} [] :
= 1
theorem MvPolynomial.coeff_X_pow {R : Type u} {σ : Type u_1} [] [] (i : σ) (m : σ →₀ ) (k : ) :
= if = m then 1 else 0
theorem MvPolynomial.coeff_X' {R : Type u} {σ : Type u_1} [] [] (i : σ) (m : σ →₀ ) :
= if = m then 1 else 0
@[simp]
theorem MvPolynomial.coeff_X {R : Type u} {σ : Type u_1} [] (i : σ) :
= 1
@[simp]
theorem MvPolynomial.coeff_C_mul {R : Type u} {σ : Type u_1} [] (m : σ →₀ ) (a : R) (p : ) :
MvPolynomial.coeff m (MvPolynomial.C a * p) = a *
theorem MvPolynomial.coeff_mul {R : Type u} {σ : Type u_1} [] [] (p : ) (q : ) (n : σ →₀ ) :
MvPolynomial.coeff n (p * q) = Finset.sum fun (x : (σ →₀ ) × (σ →₀ )) => *
@[simp]
theorem MvPolynomial.coeff_mul_monomial {R : Type u} {σ : Type u_1} [] (m : σ →₀ ) (s : σ →₀ ) (r : R) (p : ) :
MvPolynomial.coeff (m + s) (p * ) = * r
@[simp]
theorem MvPolynomial.coeff_monomial_mul {R : Type u} {σ : Type u_1} [] (m : σ →₀ ) (s : σ →₀ ) (r : R) (p : ) :
MvPolynomial.coeff (s + m) ( * p) = r *
@[simp]
theorem MvPolynomial.coeff_mul_X {R : Type u} {σ : Type u_1} [] (m : σ →₀ ) (s : σ) (p : ) :
@[simp]
theorem MvPolynomial.coeff_X_mul {R : Type u} {σ : Type u_1} [] (m : σ →₀ ) (s : σ) (p : ) :
@[simp]
theorem MvPolynomial.support_mul_X {R : Type u} {σ : Type u_1} [] (s : σ) (p : ) :
@[simp]
theorem MvPolynomial.support_X_mul {R : Type u} {σ : Type u_1} [] (s : σ) (p : ) :
@[simp]
theorem MvPolynomial.support_smul_eq {R : Type u} {σ : Type u_1} [] {S₁ : Type u_2} [Semiring S₁] [Module S₁ R] [] {a : S₁} (h : a 0) (p : ) :
theorem MvPolynomial.support_sdiff_support_subset_support_add {R : Type u} {σ : Type u_1} [] [] (p : ) (q : ) :
theorem MvPolynomial.support_symmDiff_support_subset_support_add {R : Type u} {σ : Type u_1} [] [] (p : ) (q : ) :
theorem MvPolynomial.coeff_mul_monomial' {R : Type u} {σ : Type u_1} [] (m : σ →₀ ) (s : σ →₀ ) (r : R) (p : ) :
MvPolynomial.coeff m (p * ) = if s m then MvPolynomial.coeff (m - s) p * r else 0
theorem MvPolynomial.coeff_monomial_mul' {R : Type u} {σ : Type u_1} [] (m : σ →₀ ) (s : σ →₀ ) (r : R) (p : ) :
MvPolynomial.coeff m ( * p) = if s m then r * MvPolynomial.coeff (m - s) p else 0
theorem MvPolynomial.coeff_mul_X' {R : Type u} {σ : Type u_1} [] [] (m : σ →₀ ) (s : σ) (p : ) :
= if s m.support then MvPolynomial.coeff (m - ) p else 0
theorem MvPolynomial.coeff_X_mul' {R : Type u} {σ : Type u_1} [] [] (m : σ →₀ ) (s : σ) (p : ) :
= if s m.support then MvPolynomial.coeff (m - ) p else 0
theorem MvPolynomial.eq_zero_iff {R : Type u} {σ : Type u_1} [] {p : } :
p = 0 ∀ (d : σ →₀ ), = 0
theorem MvPolynomial.ne_zero_iff {R : Type u} {σ : Type u_1} [] {p : } :
p 0 ∃ (d : σ →₀ ), 0
@[simp]
theorem MvPolynomial.support_eq_empty {R : Type u} {σ : Type u_1} [] {p : } :
p = 0
theorem MvPolynomial.exists_coeff_ne_zero {R : Type u} {σ : Type u_1} [] {p : } (h : p 0) :
∃ (d : σ →₀ ), 0
theorem MvPolynomial.C_dvd_iff_dvd_coeff {R : Type u} {σ : Type u_1} [] (r : R) (φ : ) :
MvPolynomial.C r φ ∀ (i : σ →₀ ), r
@[simp]
theorem MvPolynomial.isRegular_X {R : Type u} {σ : Type u_1} {n : σ} [] :
@[simp]
theorem MvPolynomial.isRegular_X_pow {R : Type u} {σ : Type u_1} {n : σ} [] (k : ) :
@[simp]
theorem MvPolynomial.isRegular_prod_X {R : Type u} {σ : Type u_1} [] (s : ) :
IsRegular (Finset.prod s fun (n : σ) => )
def MvPolynomial.constantCoeff {R : Type u} {σ : Type u_1} [] :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem MvPolynomial.constantCoeff_eq {R : Type u} {σ : Type u_1} [] :
MvPolynomial.constantCoeff =
@[simp]
theorem MvPolynomial.constantCoeff_C {R : Type u} (σ : Type u_1) [] (r : R) :
MvPolynomial.constantCoeff (MvPolynomial.C r) = r
@[simp]
theorem MvPolynomial.constantCoeff_X (R : Type u) {σ : Type u_1} [] (i : σ) :
MvPolynomial.constantCoeff () = 0
@[simp]
theorem MvPolynomial.constantCoeff_smul {S₁ : Type v} {σ : Type u_1} [] {R : Type u_2} [] (a : R) (f : MvPolynomial σ S₁) :
MvPolynomial.constantCoeff (a f) = a MvPolynomial.constantCoeff f
theorem MvPolynomial.constantCoeff_monomial {R : Type u} {σ : Type u_1} [] [] (d : σ →₀ ) (r : R) :
MvPolynomial.constantCoeff () = if d = 0 then r else 0
@[simp]
theorem MvPolynomial.constantCoeff_comp_C (R : Type u) (σ : Type u_1) [] :
RingHom.comp MvPolynomial.constantCoeff MvPolynomial.C =
@[simp]
theorem MvPolynomial.constantCoeff_comp_algebraMap (R : Type u) (σ : Type u_1) [] :
RingHom.comp MvPolynomial.constantCoeff (algebraMap R ()) =
@[simp]
theorem MvPolynomial.support_sum_monomial_coeff {R : Type u} {σ : Type u_1} [] (p : ) :
(Finset.sum fun (v : σ →₀ ) => ()) = p
theorem MvPolynomial.as_sum {R : Type u} {σ : Type u_1} [] (p : ) :
p = Finset.sum fun (v : σ →₀ ) => ()
def MvPolynomial.eval₂ {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [] (f : R →+* S₁) (g : σS₁) (p : ) :
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
Instances For
theorem MvPolynomial.eval₂_eq {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [] (g : R →+* S₁) (X : σS₁) (f : ) :
= Finset.sum fun (d : σ →₀ ) => g () * Finset.prod d.support fun (i : σ) => X i ^ d i
theorem MvPolynomial.eval₂_eq' {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [] [] (g : R →+* S₁) (X : σS₁) (f : ) :
= Finset.sum fun (d : σ →₀ ) => g () * Finset.prod Finset.univ fun (i : σ) => X i ^ d i
@[simp]
theorem MvPolynomial.eval₂_zero {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [] (f : R →+* S₁) (g : σS₁) :
= 0
@[simp]
theorem MvPolynomial.eval₂_add {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [] {p : } {q : } (f : R →+* S₁) (g : σS₁) :
@[simp]
theorem MvPolynomial.eval₂_monomial {R : Type u} {S₁ : Type v} {σ : Type u_1} {a : R} {s : σ →₀ } [] [] (f : R →+* S₁) (g : σS₁) :
MvPolynomial.eval₂ f g () = f a * Finsupp.prod s fun (n : σ) (e : ) => g n ^ e
@[simp]
theorem MvPolynomial.eval₂_C {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [] (f : R →+* S₁) (g : σS₁) (a : R) :
MvPolynomial.eval₂ f g (MvPolynomial.C a) = f a
@[simp]
theorem MvPolynomial.eval₂_one {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [] (f : R →+* S₁) (g : σS₁) :
= 1
@[simp]
theorem MvPolynomial.eval₂_X {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [] (f : R →+* S₁) (g : σS₁) (n : σ) :
= g n
theorem MvPolynomial.eval₂_mul_monomial {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [] {p : } (f : R →+* S₁) (g : σS₁) {s : σ →₀ } {a : R} :
MvPolynomial.eval₂ f g (p * ) = * f a * Finsupp.prod s fun (n : σ) (e : ) => g n ^ e
theorem MvPolynomial.eval₂_mul_C {R : Type u} {S₁ : Type v} {σ : Type u_1} {a : R} [] [] {p : } (f : R →+* S₁) (g : σS₁) :
MvPolynomial.eval₂ f g (p * MvPolynomial.C a) = * f a
@[simp]
theorem MvPolynomial.eval₂_mul {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [] {q : } (f : R →+* S₁) (g : σS₁) {p : } :
@[simp]
theorem MvPolynomial.eval₂_pow {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [] (f : R →+* S₁) (g : σS₁) {p : } {n : } :
def MvPolynomial.eval₂Hom {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [] (f : R →+* S₁) (g : σS₁) :
→+* S₁

MvPolynomial.eval₂ as a RingHom.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem MvPolynomial.coe_eval₂Hom {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [] (f : R →+* S₁) (g : σS₁) :
() =
theorem MvPolynomial.eval₂Hom_congr {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [] {f₁ : R →+* S₁} {f₂ : R →+* S₁} {g₁ : σS₁} {g₂ : σS₁} {p₁ : } {p₂ : } :
f₁ = f₂g₁ = g₂p₁ = p₂() p₁ = () p₂
@[simp]
theorem MvPolynomial.eval₂Hom_C {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [] (f : R →+* S₁) (g : σS₁) (r : R) :
() (MvPolynomial.C r) = f r
@[simp]
theorem MvPolynomial.eval₂Hom_X' {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [] (f : R →+* S₁) (g : σS₁) (i : σ) :
() () = g i
@[simp]
theorem MvPolynomial.comp_eval₂Hom {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [] [] [] (f : R →+* S₁) (g : σS₁) (φ : S₁ →+* S₂) :
= MvPolynomial.eval₂Hom () fun (i : σ) => φ (g i)
theorem MvPolynomial.map_eval₂Hom {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [] [] [] (f : R →+* S₁) (g : σS₁) (φ : S₁ →+* S₂) (p : ) :
φ (() p) = (MvPolynomial.eval₂Hom () fun (i : σ) => φ (g i)) p
theorem MvPolynomial.eval₂Hom_monomial {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [] (f : R →+* S₁) (g : σS₁) (d : σ →₀ ) (r : R) :
() () = f r * Finsupp.prod d fun (i : σ) (k : ) => g i ^ k
theorem MvPolynomial.eval₂_comp_left {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [] {S₂ : Type u_2} [] (k : S₁ →+* S₂) (f : R →+* S₁) (g : σS₁) (p : ) :
k () = MvPolynomial.eval₂ () (k g) p
@[simp]
theorem MvPolynomial.eval₂_eta {R : Type u} {σ : Type u_1} [] (p : ) :
MvPolynomial.eval₂ MvPolynomial.C MvPolynomial.X p = p
theorem MvPolynomial.eval₂_congr {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [] {p : } (f : R →+* S₁) (g₁ : σS₁) (g₂ : σS₁) (h : ∀ {i : σ} {c : σ →₀ }, i c.support 0g₁ i = g₂ i) :
=
@[simp]
theorem MvPolynomial.eval₂_sum {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [] [] (f : R →+* S₁) (g : σS₁) (s : Finset S₂) (p : S₂) :
MvPolynomial.eval₂ f g (Finset.sum s fun (x : S₂) => p x) = Finset.sum s fun (x : S₂) => MvPolynomial.eval₂ f g (p x)
@[simp]
theorem MvPolynomial.eval₂_prod {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [] [] (f : R →+* S₁) (g : σS₁) (s : Finset S₂) (p : S₂) :
MvPolynomial.eval₂ f g (Finset.prod s fun (x : S₂) => p x) = Finset.prod s fun (x : S₂) => MvPolynomial.eval₂ f g (p x)
theorem MvPolynomial.eval₂_assoc {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [] [] (f : R →+* S₁) (g : σS₁) (q : S₂) (p : MvPolynomial S₂ R) :
MvPolynomial.eval₂ f (fun (t : S₂) => MvPolynomial.eval₂ f g (q t)) p = MvPolynomial.eval₂ f g (MvPolynomial.eval₂ MvPolynomial.C q p)
def MvPolynomial.eval {R : Type u} {σ : Type u_1} [] (f : σR) :

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

Equations
Instances For
theorem MvPolynomial.eval_eq {R : Type u} {σ : Type u_1} [] (X : σR) (f : ) :
f = Finset.sum fun (d : σ →₀ ) => * Finset.prod d.support fun (i : σ) => X i ^ d i
theorem MvPolynomial.eval_eq' {R : Type u} {σ : Type u_1} [] [] (X : σR) (f : ) :
f = Finset.sum fun (d : σ →₀ ) => * Finset.prod Finset.univ fun (i : σ) => X i ^ d i
theorem MvPolynomial.eval_monomial {R : Type u} {σ : Type u_1} {a : R} {s : σ →₀ } [] {f : σR} :
() = a * Finsupp.prod s fun (n : σ) (e : ) => f n ^ e
@[simp]
theorem MvPolynomial.eval_C {R : Type u} {σ : Type u_1} [] {f : σR} (a : R) :
(MvPolynomial.C a) = a
@[simp]
theorem MvPolynomial.eval_X {R : Type u} {σ : Type u_1} [] {f : σR} (n : σ) :
() = f n
@[simp]
theorem MvPolynomial.smul_eval {R : Type u} {σ : Type u_1} [] (x : σR) (p : ) (s : R) :
(s p) = s * p
theorem MvPolynomial.eval_add {R : Type u} {σ : Type u_1} [] {p : } {q : } {f : σR} :
(p + q) = p + q
theorem MvPolynomial.eval_mul {R : Type u} {σ : Type u_1} [] {p : } {q : } {f : σR} :
(p * q) = p * q
theorem MvPolynomial.eval_pow {R : Type u} {σ : Type u_1} [] {p : } {f : σR} (n : ) :
(p ^ n) = p ^ n
theorem MvPolynomial.eval_sum {R : Type u} {σ : Type u_1} [] {ι : Type u_2} (s : ) (f : ι) (g : σR) :
(Finset.sum s fun (i : ι) => f i) = Finset.sum s fun (i : ι) => (f i)
theorem MvPolynomial.eval_prod {R : Type u} {σ : Type u_1} [] {ι : Type u_2} (s : ) (f : ι) (g : σR) :
(Finset.prod s fun (i : ι) => f i) = Finset.prod s fun (i : ι) => (f i)
theorem MvPolynomial.eval_assoc {R : Type u} {σ : Type u_1} [] {τ : Type u_2} (f : σ) (g : τR) (p : ) :
(MvPolynomial.eval ( f)) p = (MvPolynomial.eval₂ MvPolynomial.C f p)
@[simp]
theorem MvPolynomial.eval₂_id {R : Type u} {σ : Type u_1} [] {g : σR} (p : ) :
= p
theorem MvPolynomial.eval_eval₂ {R : Type u} {σ : Type u_1} {S : Type u_2} {τ : Type u_3} {x : τS} [] [] (f : R →+* ) (g : σ) (p : ) :
() = MvPolynomial.eval₂ () (fun (s : σ) => (g s)) p
def MvPolynomial.map {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [] (f : R →+* S₁) :

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

Equations
Instances For
@[simp]
theorem MvPolynomial.map_monomial {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [] (f : R →+* S₁) (s : σ →₀ ) (a : R) :
() () = (f a)
@[simp]
theorem MvPolynomial.map_C {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [] (f : R →+* S₁) (a : R) :
() (MvPolynomial.C a) = MvPolynomial.C (f a)
@[simp]
theorem MvPolynomial.map_X {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [] (f : R →+* S₁) (n : σ) :
theorem MvPolynomial.map_id {R : Type u} {σ : Type u_1} [] (p : ) :
() p = p
theorem MvPolynomial.map_map {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [] [] (f : R →+* S₁) [] (g : S₁ →+* S₂) (p : ) :
() (() p) = () p
theorem MvPolynomial.eval₂_eq_eval_map {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [] (f : R →+* S₁) (g : σS₁) (p : ) :
= (() p)
theorem MvPolynomial.eval₂_comp_right {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [] {S₂ : Type u_2} [] (k : S₁ →+* S₂) (f : R →+* S₁) (g : σS₁) (p : ) :
k () = MvPolynomial.eval₂ k (k g) (() p)
theorem MvPolynomial.map_eval₂ {R : Type u} {S₁ : Type v} {S₂ : Type w} {S₃ : Type x} [] [] (f : R →+* S₁) (g : S₂MvPolynomial S₃ R) (p : MvPolynomial S₂ R) :
() (MvPolynomial.eval₂ MvPolynomial.C g p) = MvPolynomial.eval₂ MvPolynomial.C (() g) (() p)
theorem MvPolynomial.coeff_map {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [] (f : R →+* S₁) (p : ) (m : σ →₀ ) :
MvPolynomial.coeff m (() p) = f ()
theorem MvPolynomial.map_injective {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [] (f : R →+* S₁) (hf : ) :
theorem MvPolynomial.map_surjective {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [] (f : R →+* S₁) (hf : ) :
theorem MvPolynomial.map_leftInverse {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [] {f : R →+* S₁} {g : S₁ →+* R} (hf : ) :

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

theorem MvPolynomial.map_rightInverse {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [] {f : R →+* S₁} {g : S₁ →+* R} (hf : ) :

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

@[simp]
theorem MvPolynomial.eval_map {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [] (f : R →+* S₁) (g : σS₁) (p : ) :
(() p) =
@[simp]
theorem MvPolynomial.eval₂_map {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [] [] [] (f : R →+* S₁) (g : σS₂) (φ : S₁ →+* S₂) (p : ) :
@[simp]
theorem MvPolynomial.eval₂Hom_map_hom {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [] [] [] (f : R →+* S₁) (g : σS₂) (φ : S₁ →+* S₂) (p : ) :
() (() p) = () p
@[simp]
theorem MvPolynomial.constantCoeff_map {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [] (f : R →+* S₁) (φ : ) :
MvPolynomial.constantCoeff (() φ) = f (MvPolynomial.constantCoeff φ)
theorem MvPolynomial.constantCoeff_comp_map {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [] (f : R →+* S₁) :
RingHom.comp MvPolynomial.constantCoeff () = RingHom.comp f MvPolynomial.constantCoeff
theorem MvPolynomial.support_map_subset {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [] (f : R →+* S₁) (p : ) :
theorem MvPolynomial.support_map_of_injective {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [] (p : ) {f : R →+* S₁} (hf : ) :
theorem MvPolynomial.C_dvd_iff_map_hom_eq_zero {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [] (q : R →+* S₁) (r : R) (hr : ∀ (r' : R), q r' = 0 r r') (φ : ) :
MvPolynomial.C r φ () φ = 0
theorem MvPolynomial.map_mapRange_eq_iff {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [] (f : R →+* S₁) (g : S₁R) (hg : g 0 = 0) (φ : MvPolynomial σ S₁) :
() (Finsupp.mapRange g hg φ) = φ ∀ (d : σ →₀ ), f (g ()) =
@[simp]
theorem MvPolynomial.mapAlgHom_apply {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [] [] [] [Algebra R S₁] [Algebra R S₂] (f : S₁ →ₐ[R] S₂) (p : MvPolynomial σ S₁) :
= MvPolynomial.eval₂ (RingHom.comp MvPolynomial.C f) MvPolynomial.X p
def MvPolynomial.mapAlgHom {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [] [] [] [Algebra R S₁] [Algebra R S₂] (f : S₁ →ₐ[R] S₂) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem MvPolynomial.mapAlgHom_id {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [] [Algebra R S₁] :
= AlgHom.id R (MvPolynomial σ S₁)
@[simp]
theorem MvPolynomial.mapAlgHom_coe_ringHom {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [] [] [] [Algebra R S₁] [Algebra R S₂] (f : S₁ →ₐ[R] S₂) :

### The algebra of multivariate polynomials #

theorem MvPolynomial.algebraMap_apply {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [] [Algebra R S₁] (r : R) :
(algebraMap R (MvPolynomial σ S₁)) r = MvPolynomial.C ((algebraMap R S₁) r)
def MvPolynomial.aeval {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [] [Algebra R 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
• One or more equations did not get rendered due to their size.
Instances For
theorem MvPolynomial.aeval_def {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [] [Algebra R S₁] (f : σS₁) (p : ) :
theorem MvPolynomial.aeval_eq_eval₂Hom {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [] [Algebra R S₁] (f : σS₁) (p : ) :
@[simp]
theorem MvPolynomial.aeval_X {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [] [Algebra R S₁] (f : σS₁) (s : σ) :
() = f s
@[simp]
theorem MvPolynomial.aeval_C {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [] [Algebra R S₁] (f : σS₁) (r : R) :
(MvPolynomial.C r) = (algebraMap R S₁) r
theorem MvPolynomial.aeval_unique {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [] [Algebra R S₁] (φ : →ₐ[R] S₁) :
φ = MvPolynomial.aeval (φ MvPolynomial.X)
theorem MvPolynomial.aeval_X_left {R : Type u} {σ : Type u_1} [] :
MvPolynomial.aeval MvPolynomial.X = AlgHom.id R ()
theorem MvPolynomial.aeval_X_left_apply {R : Type u} {σ : Type u_1} [] (p : ) :
(MvPolynomial.aeval MvPolynomial.X) p = p
theorem MvPolynomial.comp_aeval {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [] [Algebra R S₁] (f : σS₁) {B : Type u_2} [] [Algebra R B] (φ : S₁ →ₐ[R] B) :
= MvPolynomial.aeval fun (i : σ) => φ (f i)
@[simp]
theorem MvPolynomial.map_aeval {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [] [Algebra R S₁] {B : Type u_2} [] (g : σS₁) (φ : S₁ →+* B) (p : ) :
φ ( p) = (MvPolynomial.eval₂Hom (RingHom.comp φ (algebraMap R S₁)) fun (i : σ) => φ (g i)) p
@[simp]
theorem MvPolynomial.eval₂Hom_zero {R : Type u} {S₂ : Type w} {σ : Type u_1} [] [] (f : R →+* S₂) :
= RingHom.comp f MvPolynomial.constantCoeff
@[simp]
theorem MvPolynomial.eval₂Hom_zero' {R : Type u} {S₂ : Type w} {σ : Type u_1} [] [] (f : R →+* S₂) :
(MvPolynomial.eval₂Hom f fun (x : σ) => 0) = RingHom.comp f MvPolynomial.constantCoeff
theorem MvPolynomial.eval₂Hom_zero_apply {R : Type u} {S₂ : Type w} {σ : Type u_1} [] [] (f : R →+* S₂) (p : ) :
() p = f (MvPolynomial.constantCoeff p)
theorem MvPolynomial.eval₂Hom_zero'_apply {R : Type u} {S₂ : Type w} {σ : Type u_1} [] [] (f : R →+* S₂) (p : ) :
(MvPolynomial.eval₂Hom f fun (x : σ) => 0) p = f (MvPolynomial.constantCoeff p)
@[simp]
theorem MvPolynomial.eval₂_zero_apply {R : Type u} {S₂ : Type w} {σ : Type u_1} [] [] (f : R →+* S₂) (p : ) :
= f (MvPolynomial.constantCoeff p)
@[simp]
theorem MvPolynomial.eval₂_zero'_apply {R : Type u} {S₂ : Type w} {σ : Type u_1} [] [] (f : R →+* S₂) (p : ) :
MvPolynomial.eval₂ f (fun (x : σ) => 0) p = f (MvPolynomial.constantCoeff p)
@[simp]
theorem MvPolynomial.aeval_zero {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [] [Algebra R S₁] (p : ) :
p = (algebraMap R S₁) (MvPolynomial.constantCoeff p)
@[simp]
theorem MvPolynomial.aeval_zero' {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [] [Algebra R S₁] (p : ) :
(MvPolynomial.aeval fun (x : σ) => 0) p = (algebraMap R S₁) (MvPolynomial.constantCoeff p)
@[simp]
theorem MvPolynomial.eval_zero {R : Type u} {σ : Type u_1} [] :
= MvPolynomial.constantCoeff
@[simp]
theorem MvPolynomial.eval_zero' {R : Type u} {σ : Type u_1} [] :
(MvPolynomial.eval fun (x : σ) => 0) = MvPolynomial.constantCoeff
theorem MvPolynomial.aeval_monomial {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [] [Algebra R S₁] (g : σS₁) (d : σ →₀ ) (r : R) :
() = (algebraMap R S₁) r * Finsupp.prod d fun (i : σ) (k : ) => g i ^ k
theorem MvPolynomial.eval₂Hom_eq_zero {R : Type u} {S₂ : Type w} {σ : Type u_1} [] [] (f : R →+* S₂) (g : σS₂) (φ : ) (h : ∀ (d : σ →₀ ), 0∃ i ∈ d.support, g i = 0) :
() φ = 0
theorem MvPolynomial.aeval_eq_zero {R : Type u} {S₂ : Type w} {σ : Type u_1} [] [] [Algebra R S₂] (f : σS₂) (φ : ) (h : ∀ (d : σ →₀ ), 0∃ i ∈ d.support, f i = 0) :
φ = 0
theorem MvPolynomial.aeval_sum {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [] [Algebra R S₁] (f : σS₁) {ι : Type u_2} (s : ) (φ : ι) :
(Finset.sum s fun (i : ι) => φ i) = Finset.sum s fun (i : ι) => (φ i)
theorem MvPolynomial.aeval_prod {R : Type u} {S₁ : Type v} {σ : Type u_1} [] [] [Algebra R S₁] (f : σS₁) {ι : Type u_2} (s : ) (φ : ι) :
(Finset.prod s fun (i : ι) => φ i) = Finset.prod s fun (i : ι) => (φ i)
theorem Algebra.adjoin_range_eq_range_aeval (R : Type u) {S₁ : Type v} {σ : Type u_1} [] [] [Algebra R S₁] (f : σS₁) :
theorem Algebra.adjoin_eq_range (R : Type u) {S₁ : Type v} [] [] [Algebra R S₁] (s : Set S₁) :
def MvPolynomial.aevalTower {R : Type u} {σ : Type u_1} [] {S : Type u_2} {A : Type u_3} [] [] [Algebra S R] [Algebra S A] (f : R →ₐ[S] A) (X : σA) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem MvPolynomial.aevalTower_X {R : Type u} {σ : Type u_1} [] {S : Type u_2} {A : Type u_3} [] [] [Algebra S R] [Algebra S A] (g : R →ₐ[S] A) (y : σA) (i : σ) :
() () = y i
@[simp]
theorem MvPolynomial.aevalTower_C {R : Type u} {σ : Type u_1} [] {S : Type u_2} {A : Type u_3} [] [] [Algebra S R] [Algebra S A] (g : R →ₐ[S] A) (y : σA) (x : R) :
() (MvPolynomial.C x) = g x
@[simp]
theorem MvPolynomial.aevalTower_comp_C {R : Type u} {σ : Type u_1} [] {S : Type u_2} {A : Type u_3} [] [] [Algebra S R] [Algebra S A] (g : R →ₐ[S] A) (y : σA) :
RingHom.comp (()) MvPolynomial.C = g
@[simp]
theorem MvPolynomial.aevalTower_algebraMap {R : Type u} {σ : Type u_1} [] {S : Type u_2} {A : Type u_3} [] [] [Algebra S R] [Algebra S A] (g : R →ₐ[S] A) (y : σA) (x : R) :
() ((algebraMap R ()) x) = g x
@[simp]
theorem MvPolynomial.aevalTower_comp_algebraMap {R : Type u} {σ : Type u_1} [] {S : Type u_2} {A : Type u_3} [] [] [Algebra S R] [Algebra S A] (g : R →ₐ[S] A) (y : σA) :
RingHom.comp (()) (algebraMap R ()) = g
theorem MvPolynomial.aevalTower_toAlgHom {R : Type u} {σ : Type u_1} [] {S : Type u_2} {A : Type u_3} [] [] [Algebra S R] [Algebra S A] (g : R →ₐ[S] A) (y : σA) (x : R) :
() (() x) = g x
@[simp]
theorem MvPolynomial.aevalTower_comp_toAlgHom {R : Type u} {σ : Type u_1} [] {S : Type u_2} {A : Type u_3} [] [] [Algebra S R] [Algebra S A] (g : R →ₐ[S] A) (y : σA) :
AlgHom.comp () () = g
@[simp]
theorem MvPolynomial.aevalTower_id {σ : Type u_1} {S : Type u_2} [] :
= MvPolynomial.aeval
@[simp]
theorem MvPolynomial.aevalTower_ofId {σ : Type u_1} {S : Type u_2} {A : Type u_3} [] [] [Algebra S A] :
= MvPolynomial.aeval
theorem MvPolynomial.eval₂_mem {R : Type u} {σ : Type u_1} [] {S : Type u_2} {subS : Type u_3} [] [SetLike subS S] [SubsemiringClass subS S] {f : R →+* S} {p : } {s : subS} (hs : i, f () s) {v : σS} (hv : ∀ (i : σ), v i s) :
s
theorem MvPolynomial.eval_mem {σ : Type u_1} {S : Type u_2} {subS : Type u_3} [] [SetLike subS S] [SubsemiringClass subS S] {p : } {s : subS} (hs : i, s) {v : σS} (hv : ∀ (i : σ), v i s) :
p s