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) [CommSemiring R] : Type (max u_1 u_2)

Multivariate polynomial, where σ is the index set of the variables and R is the coefficient ring

Equations

• MvPolynomial σ R = AddMonoidAlgebra R (σ →₀ ℕ)

instance MvPolynomial.decidableEqMvPolynomial {R : Type u} {σ : Type u_1} [CommSemiring R] [DecidableEq σ] [DecidableEq R] : DecidableEq (MvPolynomial σ R)

Equations

• MvPolynomial.decidableEqMvPolynomial = Finsupp.instDecidableEq

instance MvPolynomial.commSemiring {R : Type u} {σ : Type u_1} [CommSemiring R] : CommSemiring (MvPolynomial σ R)

Equations

• MvPolynomial.commSemiring = AddMonoidAlgebra.commSemiring

instance MvPolynomial.inhabited {R : Type u} {σ : Type u_1} [CommSemiring R] : Inhabited (MvPolynomial σ R)

Equations

• MvPolynomial.inhabited = { default := 0 }

instance MvPolynomial.distribuMulAction {R : Type u} {S₁ : Type v} {σ : Type u_1} [Monoid R] [CommSemiring S₁] [DistribMulAction R S₁] : DistribMulAction R (MvPolynomial σ S₁)

Equations

• MvPolynomial.distribuMulAction = AddMonoidAlgebra.distribMulAction

instance MvPolynomial.smulZeroClass {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring S₁] [SMulZeroClass R S₁] : SMulZeroClass R (MvPolynomial σ S₁)

Equations

• MvPolynomial.smulZeroClass = AddMonoidAlgebra.smulZeroClass

instance MvPolynomial.faithfulSMul {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring S₁] [SMulZeroClass R S₁] [FaithfulSMul R S₁] : FaithfulSMul R (MvPolynomial σ S₁)

Equations

• ⋯ = ⋯

instance MvPolynomial.module {R : Type u} {S₁ : Type v} {σ : Type u_1} [Semiring R] [CommSemiring S₁] [Module R S₁] : Module R (MvPolynomial σ S₁)

Equations

• MvPolynomial.module = AddMonoidAlgebra.module

instance MvPolynomial.isScalarTower {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [CommSemiring S₂] [SMul R S₁] [SMulZeroClass 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} [CommSemiring S₂] [SMulZeroClass R S₂] [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} [CommSemiring S₁] [SMulZeroClass R S₁] [SMulZeroClass Rᵐᵒᵖ S₁] [IsCentralScalar R S₁] : IsCentralScalar R (MvPolynomial σ S₁)

Equations

• ⋯ = ⋯

instance MvPolynomial.algebra {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] : Algebra R (MvPolynomial σ S₁)

Equations

• MvPolynomial.algebra = AddMonoidAlgebra.algebra

instance MvPolynomial.isScalarTower_right {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring S₁] [DistribSMul R S₁] [IsScalarTower R S₁ S₁] : IsScalarTower R (MvPolynomial σ S₁) (MvPolynomial σ S₁)

Equations

• ⋯ = ⋯

instance MvPolynomial.smulCommClass_right {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring S₁] [DistribSMul R S₁] [SMulCommClass R S₁ S₁] : SMulCommClass R (MvPolynomial σ S₁) (MvPolynomial σ S₁)

Equations

• ⋯ = ⋯

instance MvPolynomial.unique {R : Type u} {σ : Type u_1} [CommSemiring R] [Subsingleton R] : Unique (MvPolynomial σ R)

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

Equations

• MvPolynomial.unique = AddMonoidAlgebra.unique

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

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

Equations

• MvPolynomial.monomial s = Finsupp.lsingle s

theorem MvPolynomial.single_eq_monomial {R : Type u} {σ : Type u_1} [CommSemiring R] (s : σ →₀ ℕ) (a : R) : Finsupp.single s a = (MvPolynomial.monomial s) a

theorem MvPolynomial.mul_def {R : Type u} {σ : Type u_1} [CommSemiring R] {p : MvPolynomial σ R} {q : MvPolynomial σ R} : 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} [CommSemiring R] : R →+* MvPolynomial σ R

C a is the constant polynomial with value a

Equations

• One or more equations did not get rendered due to their size.

theorem MvPolynomial.algebraMap_eq (R : Type u) (σ : Type u_1) [CommSemiring R] : algebraMap R (MvPolynomial σ R) = MvPolynomial.C

def MvPolynomial.X {R : Type u} {σ : Type u_1} [CommSemiring R] (n : σ) : MvPolynomial σ R

X n is the degree 1 monomial $X_n$.

Equations

• MvPolynomial.X n = (MvPolynomial.monomial (Finsupp.single n 1)) 1

theorem MvPolynomial.monomial_left_injective {R : Type u} {σ : Type u_1} [CommSemiring R] {r : R} (hr : r ≠ 0) : Function.Injective fun (s : σ →₀ ℕ) => (MvPolynomial.monomial s) r

@[simp]

theorem MvPolynomial.monomial_left_inj {R : Type u} {σ : Type u_1} [CommSemiring R] {s : σ →₀ ℕ} {t : σ →₀ ℕ} {r : R} (hr : r ≠ 0) : (MvPolynomial.monomial s) r = (MvPolynomial.monomial t) r ↔ s = t

theorem MvPolynomial.C_apply {R : Type u} {σ : Type u_1} {a : R} [CommSemiring R] : MvPolynomial.C a = (MvPolynomial.monomial 0) a

theorem MvPolynomial.C_0 {R : Type u} {σ : Type u_1} [CommSemiring R] : MvPolynomial.C 0 = 0

theorem MvPolynomial.C_1 {R : Type u} {σ : Type u_1} [CommSemiring R] : MvPolynomial.C 1 = 1

theorem MvPolynomial.C_mul_monomial {R : Type u} {σ : Type u_1} {a : R} {a' : R} {s : σ →₀ ℕ} [CommSemiring R] : MvPolynomial.C a * (MvPolynomial.monomial s) a' = (MvPolynomial.monomial s) (a * a')

theorem MvPolynomial.C_add {R : Type u} {σ : Type u_1} {a : R} {a' : R} [CommSemiring 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} [CommSemiring R] : MvPolynomial.C (a * a') = MvPolynomial.C a * MvPolynomial.C a'

theorem MvPolynomial.C_pow {R : Type u} {σ : Type u_1} [CommSemiring R] (a : R) (n : ℕ) : MvPolynomial.C (a ^ n) = MvPolynomial.C a ^ n

theorem MvPolynomial.C_injective (σ : Type u_2) (R : Type u_3) [CommSemiring R] : Function.Injective ⇑MvPolynomial.C

theorem MvPolynomial.C_surjective {R : Type u_2} [CommSemiring R] (σ : Type u_3) [IsEmpty σ] : Function.Surjective ⇑MvPolynomial.C

@[simp]

theorem MvPolynomial.C_inj {σ : Type u_2} (R : Type u_3) [CommSemiring R] (r : R) (s : R) : MvPolynomial.C r = MvPolynomial.C s ↔ r = s

instance MvPolynomial.nontrivial_of_nontrivial (σ : Type u_2) (R : Type u_3) [CommSemiring R] [Nontrivial R] : Nontrivial (MvPolynomial σ R)

Equations

• ⋯ = ⋯

instance MvPolynomial.infinite_of_infinite (σ : Type u_2) (R : Type u_3) [CommSemiring R] [Infinite R] : Infinite (MvPolynomial σ R)

Equations

• ⋯ = ⋯

instance MvPolynomial.infinite_of_nonempty (σ : Type u_2) (R : Type u_3) [Nonempty σ] [CommSemiring R] [Nontrivial R] : Infinite (MvPolynomial σ R)

Equations

• ⋯ = ⋯

theorem MvPolynomial.C_eq_coe_nat {R : Type u} {σ : Type u_1} [CommSemiring R] (n : ℕ) : MvPolynomial.C ↑n = ↑n

theorem MvPolynomial.C_mul' {R : Type u} {σ : Type u_1} {a : R} [CommSemiring R] {p : MvPolynomial σ R} : MvPolynomial.C a * p = a • p

theorem MvPolynomial.smul_eq_C_mul {R : Type u} {σ : Type u_1} [CommSemiring R] (p : MvPolynomial σ R) (a : R) : a • p = MvPolynomial.C a * p

theorem MvPolynomial.C_eq_smul_one {R : Type u} {σ : Type u_1} {a : R} [CommSemiring R] : MvPolynomial.C a = a • 1

theorem MvPolynomial.smul_monomial {R : Type u} {σ : Type u_1} {a : R} {s : σ →₀ ℕ} [CommSemiring R] {S₁ : Type u_2} [SMulZeroClass S₁ R] (r : S₁) : r • (MvPolynomial.monomial s) a = (MvPolynomial.monomial s) (r • a)

theorem MvPolynomial.X_injective {R : Type u} {σ : Type u_1} [CommSemiring R] [Nontrivial R] : Function.Injective MvPolynomial.X

@[simp]

theorem MvPolynomial.X_inj {R : Type u} {σ : Type u_1} [CommSemiring R] [Nontrivial R] (m : σ) (n : σ) : MvPolynomial.X m = MvPolynomial.X n ↔ m = n

theorem MvPolynomial.monomial_pow {R : Type u} {σ : Type u_1} {a : R} {e : ℕ} {s : σ →₀ ℕ} [CommSemiring R] : (MvPolynomial.monomial s) a ^ e = (MvPolynomial.monomial (e • s)) (a ^ e)

@[simp]

theorem MvPolynomial.monomial_mul {R : Type u} {σ : Type u_1} [CommSemiring R] {s : σ →₀ ℕ} {s' : σ →₀ ℕ} {a : R} {b : R} : (MvPolynomial.monomial s) a * (MvPolynomial.monomial s') b = (MvPolynomial.monomial (s + s')) (a * b)

def MvPolynomial.monomialOneHom (R : Type u) (σ : Type u_1) [CommSemiring R] : Multiplicative (σ →₀ ℕ) →* MvPolynomial σ R

fun s ↦ monomial s 1 as a homomorphism.

Equations

• MvPolynomial.monomialOneHom R σ = AddMonoidAlgebra.of R (σ →₀ ℕ)

@[simp]

theorem MvPolynomial.monomialOneHom_apply {R : Type u} {σ : Type u_1} {s : σ →₀ ℕ} [CommSemiring R] : (MvPolynomial.monomialOneHom R σ) s = (MvPolynomial.monomial s) 1

theorem MvPolynomial.X_pow_eq_monomial {R : Type u} {σ : Type u_1} {e : ℕ} {n : σ} [CommSemiring R] : MvPolynomial.X n ^ e = (MvPolynomial.monomial (Finsupp.single n e)) 1

theorem MvPolynomial.monomial_add_single {R : Type u} {σ : Type u_1} {a : R} {e : ℕ} {n : σ} {s : σ →₀ ℕ} [CommSemiring R] : (MvPolynomial.monomial (s + Finsupp.single n e)) a = (MvPolynomial.monomial s) a * MvPolynomial.X n ^ e

theorem MvPolynomial.monomial_single_add {R : Type u} {σ : Type u_1} {a : R} {e : ℕ} {n : σ} {s : σ →₀ ℕ} [CommSemiring R] : (MvPolynomial.monomial (Finsupp.single n e + s)) a = MvPolynomial.X n ^ e * (MvPolynomial.monomial s) a

theorem MvPolynomial.C_mul_X_pow_eq_monomial {R : Type u} {σ : Type u_1} [CommSemiring R] {s : σ} {a : R} {n : ℕ} : MvPolynomial.C a * MvPolynomial.X s ^ n = (MvPolynomial.monomial (Finsupp.single s n)) a

theorem MvPolynomial.C_mul_X_eq_monomial {R : Type u} {σ : Type u_1} [CommSemiring R] {s : σ} {a : R} : MvPolynomial.C a * MvPolynomial.X s = (MvPolynomial.monomial (Finsupp.single s 1)) a

theorem MvPolynomial.monomial_zero {R : Type u} {σ : Type u_1} [CommSemiring R] {s : σ →₀ ℕ} : (MvPolynomial.monomial s) 0 = 0

@[simp]

theorem MvPolynomial.monomial_zero' {R : Type u} {σ : Type u_1} [CommSemiring R] : ⇑(MvPolynomial.monomial 0) = ⇑MvPolynomial.C

@[simp]

theorem MvPolynomial.monomial_eq_zero {R : Type u} {σ : Type u_1} [CommSemiring R] {s : σ →₀ ℕ} {b : R} : (MvPolynomial.monomial s) b = 0 ↔ b = 0

@[simp]

theorem MvPolynomial.sum_monomial_eq {R : Type u} {σ : Type u_1} [CommSemiring R] {A : Type u_2} [AddCommMonoid A] {u : σ →₀ ℕ} {r : R} {b : (σ →₀ ℕ) → R → A} (w : b u 0 = 0) : Finsupp.sum ((MvPolynomial.monomial u) r) b = b u r

@[simp]

theorem MvPolynomial.sum_C {R : Type u} {σ : Type u_1} {a : R} [CommSemiring R] {A : Type u_2} [AddCommMonoid A] {b : (σ →₀ ℕ) → R → A} (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} [CommSemiring R] {α : Type u_2} (s : Finset α) (f : α → σ →₀ ℕ) : (MvPolynomial.monomial (Finset.sum s fun (i : α) => f i)) 1 = Finset.prod s fun (i : α) => (MvPolynomial.monomial (f i)) 1

theorem MvPolynomial.monomial_sum_index {R : Type u} {σ : Type u_1} [CommSemiring R] {α : Type u_2} (s : Finset α) (f : α → σ →₀ ℕ) (a : R) : (MvPolynomial.monomial (Finset.sum s fun (i : α) => f i)) a = MvPolynomial.C a * Finset.prod s fun (i : α) => (MvPolynomial.monomial (f i)) 1

theorem MvPolynomial.monomial_finsupp_sum_index {R : Type u} {σ : Type u_1} [CommSemiring R] {α : Type u_2} {β : Type u_3} [Zero β] (f : α →₀ β) (g : α → β → σ →₀ ℕ) (a : R) : (MvPolynomial.monomial (Finsupp.sum f g)) 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} [CommSemiring R] {α : Type u_2} (a₁ : α →₀ ℕ) (a₂ : α →₀ ℕ) (b₁ : R) (b₂ : R) : (MvPolynomial.monomial a₁) b₁ = (MvPolynomial.monomial a₂) b₂ ↔ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0

theorem MvPolynomial.monomial_eq {R : Type u} {σ : Type u_1} {a : R} {s : σ →₀ ℕ} [CommSemiring R] : (MvPolynomial.monomial s) a = MvPolynomial.C a * Finsupp.prod s fun (n : σ) (e : ℕ) => MvPolynomial.X n ^ e

@[simp]

theorem MvPolynomial.prod_X_pow_eq_monomial {R : Type u} {σ : Type u_1} {s : σ →₀ ℕ} [CommSemiring R] : (Finset.prod s.support fun (x : σ) => MvPolynomial.X x ^ s x) = (MvPolynomial.monomial s) 1

theorem MvPolynomial.induction_on_monomial {R : Type u} {σ : Type u_1} [CommSemiring R] {M : MvPolynomial σ R → Prop} (h_C : ∀ (a : R), M (MvPolynomial.C a)) (h_X : ∀ (p : MvPolynomial σ R) (n : σ), M p → M (p * MvPolynomial.X n)) (s : σ →₀ ℕ) (a : R) : M ((MvPolynomial.monomial s) a)

theorem MvPolynomial.induction_on' {R : Type u} {σ : Type u_1} [CommSemiring R] {P : MvPolynomial σ R → Prop} (p : MvPolynomial σ R) (h1 : ∀ (u : σ →₀ ℕ) (a : R), P ((MvPolynomial.monomial u) a)) (h2 : ∀ (p q : MvPolynomial σ 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 MvPolynomial.induction_on''' {R : Type u} {σ : Type u_1} [CommSemiring R] {M : MvPolynomial σ R → Prop} (p : MvPolynomial σ R) (h_C : ∀ (a : R), M (MvPolynomial.C a)) (h_add_weak : ∀ (a : σ →₀ ℕ) (b : R) (f : (σ →₀ ℕ) →₀ R), a ∉ f.support → b ≠ 0 → M f → M ((let_fun this := (MvPolynomial.monomial a) b; 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} [CommSemiring R] {M : MvPolynomial σ R → Prop} (p : MvPolynomial σ R) (h_C : ∀ (a : R), M (MvPolynomial.C a)) (h_add_weak : ∀ (a : σ →₀ ℕ) (b : R) (f : (σ →₀ ℕ) →₀ R), a ∉ f.support → b ≠ 0 → M f → M ((MvPolynomial.monomial a) b) → M ((let_fun this := (MvPolynomial.monomial a) b; this) + f)) (h_X : ∀ (p : MvPolynomial σ R) (n : σ), M p → M (p * MvPolynomial.X n)) : 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} [CommSemiring R] {M : MvPolynomial σ R → Prop} (p : MvPolynomial σ R) (h_C : ∀ (a : R), M (MvPolynomial.C a)) (h_add : ∀ (p q : MvPolynomial σ R), M p → M q → M (p + q)) (h_X : ∀ (p : MvPolynomial σ R) (n : σ), M p → M (p * MvPolynomial.X n)) : M p

Analog of Polynomial.induction_on.

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

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

See note [partially-applied ext lemmas].

theorem MvPolynomial.hom_eq_hom {R : Type u} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [Semiring S₂] (f : MvPolynomial σ R →+* S₂) (g : MvPolynomial σ R →+* S₂) (hC : RingHom.comp f MvPolynomial.C = RingHom.comp g MvPolynomial.C) (hX : ∀ (n : σ), f (MvPolynomial.X n) = g (MvPolynomial.X n)) (p : MvPolynomial σ R) : f p = g p

theorem MvPolynomial.is_id {R : Type u} {σ : Type u_1} [CommSemiring R] (f : MvPolynomial σ R →+* MvPolynomial σ R) (hC : RingHom.comp f MvPolynomial.C = MvPolynomial.C) (hX : ∀ (n : σ), f (MvPolynomial.X n) = MvPolynomial.X n) (p : MvPolynomial σ R) : f p = p

theorem MvPolynomial.algHom_ext' {R : Type u} {σ : Type u_1} [CommSemiring R] {A : Type u_2} {B : Type u_3} [CommSemiring A] [CommSemiring B] [Algebra R A] [Algebra R B] {f : MvPolynomial σ A →ₐ[R] B} {g : MvPolynomial σ A →ₐ[R] B} (h₁ : AlgHom.comp f (IsScalarTower.toAlgHom R A (MvPolynomial σ A)) = AlgHom.comp g (IsScalarTower.toAlgHom R A (MvPolynomial σ A))) (h₂ : ∀ (i : σ), f (MvPolynomial.X i) = g (MvPolynomial.X i)) : f = g

theorem MvPolynomial.algHom_ext {R : Type u} {σ : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] [Algebra R A] {f : MvPolynomial σ R →ₐ[R] A} {g : MvPolynomial σ R →ₐ[R] A} (hf : ∀ (i : σ), f (MvPolynomial.X i) = g (MvPolynomial.X i)) : f = g

@[simp]

theorem MvPolynomial.algHom_C {R : Type u} {σ : Type u_1} [CommSemiring R] {τ : Type u_2} (f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R) (r : R) : f (MvPolynomial.C r) = MvPolynomial.C r

@[simp]

theorem MvPolynomial.adjoin_range_X {R : Type u} {σ : Type u_1} [CommSemiring R] : Algebra.adjoin R (Set.range MvPolynomial.X) = ⊤

theorem MvPolynomial.linearMap_ext {R : Type u} {σ : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {f : MvPolynomial σ R →ₗ[R] M} {g : MvPolynomial σ R →ₗ[R] M} (h : ∀ (s : σ →₀ ℕ), f ∘ₗ MvPolynomial.monomial s = g ∘ₗ MvPolynomial.monomial s) : f = g

def MvPolynomial.support {R : Type u} {σ : Type u_1} [CommSemiring R] (p : MvPolynomial σ R) : Finset (σ →₀ ℕ)

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

Equations

• MvPolynomial.support p = p.support

theorem MvPolynomial.finsupp_support_eq_support {R : Type u} {σ : Type u_1} [CommSemiring R] (p : MvPolynomial σ R) : p.support = MvPolynomial.support p

theorem MvPolynomial.support_monomial {R : Type u} {σ : Type u_1} {a : R} {s : σ →₀ ℕ} [CommSemiring R] [h : Decidable (a = 0)] : MvPolynomial.support ((MvPolynomial.monomial s) a) = if a = 0 then ∅ else {s}

theorem MvPolynomial.support_monomial_subset {R : Type u} {σ : Type u_1} {a : R} {s : σ →₀ ℕ} [CommSemiring R] : MvPolynomial.support ((MvPolynomial.monomial s) a) ⊆ {s}

theorem MvPolynomial.support_add {R : Type u} {σ : Type u_1} [CommSemiring R] {p : MvPolynomial σ R} {q : MvPolynomial σ R} [DecidableEq σ] : MvPolynomial.support (p + q) ⊆ MvPolynomial.support p ∪ MvPolynomial.support q

theorem MvPolynomial.support_X {R : Type u} {σ : Type u_1} {n : σ} [CommSemiring R] [Nontrivial R] : MvPolynomial.support (MvPolynomial.X n) = {Finsupp.single n 1}

theorem MvPolynomial.support_X_pow {R : Type u} {σ : Type u_1} [CommSemiring R] [Nontrivial R] (s : σ) (n : ℕ) : MvPolynomial.support (MvPolynomial.X s ^ n) = {Finsupp.single s n}

@[simp]

theorem MvPolynomial.support_zero {R : Type u} {σ : Type u_1} [CommSemiring R] : MvPolynomial.support 0 = ∅

theorem MvPolynomial.support_smul {R : Type u} {σ : Type u_1} [CommSemiring R] {S₁ : Type u_2} [SMulZeroClass S₁ R] {a : S₁} {f : MvPolynomial σ R} : MvPolynomial.support (a • f) ⊆ MvPolynomial.support f

theorem MvPolynomial.support_sum {R : Type u} {σ : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq σ] {s : Finset α} {f : α → MvPolynomial σ R} : 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} [CommSemiring R] (m : σ →₀ ℕ) (p : MvPolynomial σ R) : R

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

Equations

• MvPolynomial.coeff m p = p m

@[simp]

theorem MvPolynomial.mem_support_iff {R : Type u} {σ : Type u_1} [CommSemiring R] {p : MvPolynomial σ R} {m : σ →₀ ℕ} : m ∈ MvPolynomial.support p ↔ MvPolynomial.coeff m p ≠ 0

theorem MvPolynomial.not_mem_support_iff {R : Type u} {σ : Type u_1} [CommSemiring R] {p : MvPolynomial σ R} {m : σ →₀ ℕ} : m ∉ MvPolynomial.support p ↔ MvPolynomial.coeff m p = 0

theorem MvPolynomial.sum_def {R : Type u} {σ : Type u_1} [CommSemiring R] {A : Type u_2} [AddCommMonoid A] {p : MvPolynomial σ R} {b : (σ →₀ ℕ) → R → A} : Finsupp.sum p b = Finset.sum (MvPolynomial.support p) fun (m : σ →₀ ℕ) => b m (MvPolynomial.coeff m p)

theorem MvPolynomial.support_mul {R : Type u} {σ : Type u_1} [CommSemiring R] [DecidableEq σ] (p : MvPolynomial σ R) (q : MvPolynomial σ R) : MvPolynomial.support (p * q) ⊆ MvPolynomial.support p + MvPolynomial.support q

theorem MvPolynomial.ext {R : Type u} {σ : Type u_1} [CommSemiring R] (p : MvPolynomial σ R) (q : MvPolynomial σ R) : (∀ (m : σ →₀ ℕ), MvPolynomial.coeff m p = MvPolynomial.coeff m q) → p = q

theorem MvPolynomial.ext_iff {R : Type u} {σ : Type u_1} [CommSemiring R] (p : MvPolynomial σ R) (q : MvPolynomial σ R) : p = q ↔ ∀ (m : σ →₀ ℕ), MvPolynomial.coeff m p = MvPolynomial.coeff m q

@[simp]

theorem MvPolynomial.coeff_add {R : Type u} {σ : Type u_1} [CommSemiring R] (m : σ →₀ ℕ) (p : MvPolynomial σ R) (q : MvPolynomial σ R) : MvPolynomial.coeff m (p + q) = MvPolynomial.coeff m p + MvPolynomial.coeff m q

@[simp]

theorem MvPolynomial.coeff_smul {R : Type u} {σ : Type u_1} [CommSemiring R] {S₁ : Type u_2} [SMulZeroClass S₁ R] (m : σ →₀ ℕ) (C : S₁) (p : MvPolynomial σ R) : MvPolynomial.coeff m (C • p) = C • MvPolynomial.coeff m p

@[simp]

theorem MvPolynomial.coeff_zero {R : Type u} {σ : Type u_1} [CommSemiring R] (m : σ →₀ ℕ) : MvPolynomial.coeff m 0 = 0

@[simp]

theorem MvPolynomial.coeff_zero_X {R : Type u} {σ : Type u_1} [CommSemiring R] (i : σ) : MvPolynomial.coeff 0 (MvPolynomial.X i) = 0

@[simp]

theorem MvPolynomial.coeffAddMonoidHom_apply {R : Type u} {σ : Type u_1} [CommSemiring R] (m : σ →₀ ℕ) (p : MvPolynomial σ R) : (MvPolynomial.coeffAddMonoidHom m) p = MvPolynomial.coeff m p

def MvPolynomial.coeffAddMonoidHom {R : Type u} {σ : Type u_1} [CommSemiring R] (m : σ →₀ ℕ) : MvPolynomial σ R →+ R

MvPolynomial.coeff m but promoted to an AddMonoidHom.

Equations

• MvPolynomial.coeffAddMonoidHom m = { toZeroHom := { toFun := MvPolynomial.coeff m, map_zero' := ⋯ }, map_add' := ⋯ }

theorem MvPolynomial.coeff_sum {R : Type u} {σ : Type u_1} [CommSemiring R] {X : Type u_2} (s : Finset X) (f : X → MvPolynomial σ R) (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} [CommSemiring R] (m : σ →₀ ℕ) : (MvPolynomial.monomial m) 1 = Finsupp.prod m fun (n : σ) (e : ℕ) => MvPolynomial.X n ^ e

@[simp]

theorem MvPolynomial.coeff_monomial {R : Type u} {σ : Type u_1} [CommSemiring R] [DecidableEq σ] (m : σ →₀ ℕ) (n : σ →₀ ℕ) (a : R) : MvPolynomial.coeff m ((MvPolynomial.monomial n) a) = if n = m then a else 0

@[simp]

theorem MvPolynomial.coeff_C {R : Type u} {σ : Type u_1} [CommSemiring R] [DecidableEq σ] (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} [CommSemiring R] [IsEmpty σ] (p : MvPolynomial σ R) : p = MvPolynomial.C (MvPolynomial.coeff 0 p)

theorem MvPolynomial.coeff_one {R : Type u} {σ : Type u_1} [CommSemiring R] [DecidableEq σ] (m : σ →₀ ℕ) : MvPolynomial.coeff m 1 = if 0 = m then 1 else 0

@[simp]

theorem MvPolynomial.coeff_zero_C {R : Type u} {σ : Type u_1} [CommSemiring R] (a : R) : MvPolynomial.coeff 0 (MvPolynomial.C a) = a

@[simp]

theorem MvPolynomial.coeff_zero_one {R : Type u} {σ : Type u_1} [CommSemiring R] : MvPolynomial.coeff 0 1 = 1

theorem MvPolynomial.coeff_X_pow {R : Type u} {σ : Type u_1} [CommSemiring R] [DecidableEq σ] (i : σ) (m : σ →₀ ℕ) (k : ℕ) : MvPolynomial.coeff m (MvPolynomial.X i ^ k) = if Finsupp.single i k = m then 1 else 0

theorem MvPolynomial.coeff_X' {R : Type u} {σ : Type u_1} [CommSemiring R] [DecidableEq σ] (i : σ) (m : σ →₀ ℕ) : MvPolynomial.coeff m (MvPolynomial.X i) = if Finsupp.single i 1 = m then 1 else 0

@[simp]

theorem MvPolynomial.coeff_X {R : Type u} {σ : Type u_1} [CommSemiring R] (i : σ) : MvPolynomial.coeff (Finsupp.single i 1) (MvPolynomial.X i) = 1

@[simp]

theorem MvPolynomial.coeff_C_mul {R : Type u} {σ : Type u_1} [CommSemiring R] (m : σ →₀ ℕ) (a : R) (p : MvPolynomial σ R) : MvPolynomial.coeff m (MvPolynomial.C a * p) = a * MvPolynomial.coeff m p

theorem MvPolynomial.coeff_mul {R : Type u} {σ : Type u_1} [CommSemiring R] [DecidableEq σ] (p : MvPolynomial σ R) (q : MvPolynomial σ R) (n : σ →₀ ℕ) : MvPolynomial.coeff n (p * q) = Finset.sum (Finset.antidiagonal n) fun (x : (σ →₀ ℕ) × (σ →₀ ℕ)) => MvPolynomial.coeff x.1 p * MvPolynomial.coeff x.2 q

@[simp]

theorem MvPolynomial.coeff_mul_monomial {R : Type u} {σ : Type u_1} [CommSemiring R] (m : σ →₀ ℕ) (s : σ →₀ ℕ) (r : R) (p : MvPolynomial σ R) : MvPolynomial.coeff (m + s) (p * (MvPolynomial.monomial s) r) = MvPolynomial.coeff m p * r

@[simp]

theorem MvPolynomial.coeff_monomial_mul {R : Type u} {σ : Type u_1} [CommSemiring R] (m : σ →₀ ℕ) (s : σ →₀ ℕ) (r : R) (p : MvPolynomial σ R) : MvPolynomial.coeff (s + m) ((MvPolynomial.monomial s) r * p) = r * MvPolynomial.coeff m p

@[simp]

theorem MvPolynomial.coeff_mul_X {R : Type u} {σ : Type u_1} [CommSemiring R] (m : σ →₀ ℕ) (s : σ) (p : MvPolynomial σ R) : MvPolynomial.coeff (m + Finsupp.single s 1) (p * MvPolynomial.X s) = MvPolynomial.coeff m p

@[simp]

theorem MvPolynomial.coeff_X_mul {R : Type u} {σ : Type u_1} [CommSemiring R] (m : σ →₀ ℕ) (s : σ) (p : MvPolynomial σ R) : MvPolynomial.coeff (Finsupp.single s 1 + m) (MvPolynomial.X s * p) = MvPolynomial.coeff m p

@[simp]

theorem MvPolynomial.support_mul_X {R : Type u} {σ : Type u_1} [CommSemiring R] (s : σ) (p : MvPolynomial σ R) : MvPolynomial.support (p * MvPolynomial.X s) = Finset.map (addRightEmbedding (Finsupp.single s 1)) (MvPolynomial.support p)

@[simp]

theorem MvPolynomial.support_X_mul {R : Type u} {σ : Type u_1} [CommSemiring R] (s : σ) (p : MvPolynomial σ R) : MvPolynomial.support (MvPolynomial.X s * p) = Finset.map (addLeftEmbedding (Finsupp.single s 1)) (MvPolynomial.support p)

@[simp]

theorem MvPolynomial.support_smul_eq {R : Type u} {σ : Type u_1} [CommSemiring R] {S₁ : Type u_2} [Semiring S₁] [Module S₁ R] [NoZeroSMulDivisors S₁ R] {a : S₁} (h : a ≠ 0) (p : MvPolynomial σ R) : MvPolynomial.support (a • p) = MvPolynomial.support p

theorem MvPolynomial.support_sdiff_support_subset_support_add {R : Type u} {σ : Type u_1} [CommSemiring R] [DecidableEq σ] (p : MvPolynomial σ R) (q : MvPolynomial σ R) : MvPolynomial.support p \ MvPolynomial.support q ⊆ MvPolynomial.support (p + q)

theorem MvPolynomial.support_symmDiff_support_subset_support_add {R : Type u} {σ : Type u_1} [CommSemiring R] [DecidableEq σ] (p : MvPolynomial σ R) (q : MvPolynomial σ R) : symmDiff (MvPolynomial.support p) (MvPolynomial.support q) ⊆ MvPolynomial.support (p + q)

theorem MvPolynomial.coeff_mul_monomial' {R : Type u} {σ : Type u_1} [CommSemiring R] (m : σ →₀ ℕ) (s : σ →₀ ℕ) (r : R) (p : MvPolynomial σ R) : MvPolynomial.coeff m (p * (MvPolynomial.monomial s) r) = if s ≤ m then MvPolynomial.coeff (m - s) p * r else 0

theorem MvPolynomial.coeff_monomial_mul' {R : Type u} {σ : Type u_1} [CommSemiring R] (m : σ →₀ ℕ) (s : σ →₀ ℕ) (r : R) (p : MvPolynomial σ R) : MvPolynomial.coeff m ((MvPolynomial.monomial s) r * p) = if s ≤ m then r * MvPolynomial.coeff (m - s) p else 0

theorem MvPolynomial.coeff_mul_X' {R : Type u} {σ : Type u_1} [CommSemiring R] [DecidableEq σ] (m : σ →₀ ℕ) (s : σ) (p : MvPolynomial σ R) : MvPolynomial.coeff m (p * MvPolynomial.X s) = if s ∈ m.support then MvPolynomial.coeff (m - Finsupp.single s 1) p else 0

theorem MvPolynomial.coeff_X_mul' {R : Type u} {σ : Type u_1} [CommSemiring R] [DecidableEq σ] (m : σ →₀ ℕ) (s : σ) (p : MvPolynomial σ R) : MvPolynomial.coeff m (MvPolynomial.X s * p) = if s ∈ m.support then MvPolynomial.coeff (m - Finsupp.single s 1) p else 0

theorem MvPolynomial.eq_zero_iff {R : Type u} {σ : Type u_1} [CommSemiring R] {p : MvPolynomial σ R} : p = 0 ↔ ∀ (d : σ →₀ ℕ), MvPolynomial.coeff d p = 0

theorem MvPolynomial.ne_zero_iff {R : Type u} {σ : Type u_1} [CommSemiring R] {p : MvPolynomial σ R} : p ≠ 0 ↔ ∃ (d : σ →₀ ℕ), MvPolynomial.coeff d p ≠ 0

@[simp]

theorem MvPolynomial.X_ne_zero {R : Type u} {σ : Type u_1} [CommSemiring R] [Nontrivial R] (s : σ) : MvPolynomial.X s ≠ 0

@[simp]

theorem MvPolynomial.support_eq_empty {R : Type u} {σ : Type u_1} [CommSemiring R] {p : MvPolynomial σ R} : MvPolynomial.support p = ∅ ↔ p = 0

theorem MvPolynomial.exists_coeff_ne_zero {R : Type u} {σ : Type u_1} [CommSemiring R] {p : MvPolynomial σ R} (h : p ≠ 0) : ∃ (d : σ →₀ ℕ), MvPolynomial.coeff d p ≠ 0

theorem MvPolynomial.C_dvd_iff_dvd_coeff {R : Type u} {σ : Type u_1} [CommSemiring R] (r : R) (φ : MvPolynomial σ R) : MvPolynomial.C r ∣ φ ↔ ∀ (i : σ →₀ ℕ), r ∣ MvPolynomial.coeff i φ

@[simp]

theorem MvPolynomial.isRegular_X {R : Type u} {σ : Type u_1} {n : σ} [CommSemiring R] : IsRegular (MvPolynomial.X n)

@[simp]

theorem MvPolynomial.isRegular_X_pow {R : Type u} {σ : Type u_1} {n : σ} [CommSemiring R] (k : ℕ) : IsRegular (MvPolynomial.X n ^ k)

@[simp]

theorem MvPolynomial.isRegular_prod_X {R : Type u} {σ : Type u_1} [CommSemiring R] (s : Finset σ) : IsRegular (Finset.prod s fun (n : σ) => MvPolynomial.X n)

def MvPolynomial.constantCoeff {R : Type u} {σ : Type u_1} [CommSemiring R] : MvPolynomial σ R →+* R

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

Equations

• MvPolynomial.constantCoeff = { toMonoidHom := { toOneHom := { toFun := MvPolynomial.coeff 0, map_one' := ⋯ }, map_mul' := ⋯ }, map_zero' := ⋯, map_add' := ⋯ }

theorem MvPolynomial.constantCoeff_eq {R : Type u} {σ : Type u_1} [CommSemiring R] : ⇑MvPolynomial.constantCoeff = MvPolynomial.coeff 0

@[simp]

theorem MvPolynomial.constantCoeff_C {R : Type u} (σ : Type u_1) [CommSemiring R] (r : R) : MvPolynomial.constantCoeff (MvPolynomial.C r) = r

@[simp]

theorem MvPolynomial.constantCoeff_X (R : Type u) {σ : Type u_1} [CommSemiring R] (i : σ) : MvPolynomial.constantCoeff (MvPolynomial.X i) = 0

@[simp]

theorem MvPolynomial.constantCoeff_smul {S₁ : Type v} {σ : Type u_1} [CommSemiring S₁] {R : Type u_2} [SMulZeroClass R S₁] (a : R) (f : MvPolynomial σ S₁) : MvPolynomial.constantCoeff (a • f) = a • MvPolynomial.constantCoeff f

theorem MvPolynomial.constantCoeff_monomial {R : Type u} {σ : Type u_1} [CommSemiring R] [DecidableEq σ] (d : σ →₀ ℕ) (r : R) : MvPolynomial.constantCoeff ((MvPolynomial.monomial d) r) = if d = 0 then r else 0

@[simp]

theorem MvPolynomial.constantCoeff_comp_C (R : Type u) (σ : Type u_1) [CommSemiring R] : RingHom.comp MvPolynomial.constantCoeff MvPolynomial.C = RingHom.id R

@[simp]

theorem MvPolynomial.constantCoeff_comp_algebraMap (R : Type u) (σ : Type u_1) [CommSemiring R] : RingHom.comp MvPolynomial.constantCoeff (algebraMap R (MvPolynomial σ R)) = RingHom.id R

@[simp]

theorem MvPolynomial.support_sum_monomial_coeff {R : Type u} {σ : Type u_1} [CommSemiring R] (p : MvPolynomial σ R) : (Finset.sum (MvPolynomial.support p) fun (v : σ →₀ ℕ) => (MvPolynomial.monomial v) (MvPolynomial.coeff v p)) = p

theorem MvPolynomial.as_sum {R : Type u} {σ : Type u_1} [CommSemiring R] (p : MvPolynomial σ R) : p = Finset.sum (MvPolynomial.support p) fun (v : σ →₀ ℕ) => (MvPolynomial.monomial v) (MvPolynomial.coeff v p)

def MvPolynomial.eval₂ {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σ → S₁) (p : MvPolynomial σ 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

• MvPolynomial.eval₂ f g p = Finsupp.sum p fun (s : σ →₀ ℕ) (a : R) => f a * Finsupp.prod s fun (n : σ) (e : ℕ) => g n ^ e

theorem MvPolynomial.eval₂_eq {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (g : R →+* S₁) (X : σ → S₁) (f : MvPolynomial σ R) : MvPolynomial.eval₂ g X f = Finset.sum (MvPolynomial.support f) fun (d : σ →₀ ℕ) => g (MvPolynomial.coeff d f) * Finset.prod d.support fun (i : σ) => X i ^ d i

theorem MvPolynomial.eval₂_eq' {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [Fintype σ] (g : R →+* S₁) (X : σ → S₁) (f : MvPolynomial σ R) : MvPolynomial.eval₂ g X f = Finset.sum (MvPolynomial.support f) fun (d : σ →₀ ℕ) => g (MvPolynomial.coeff d f) * Finset.prod Finset.univ fun (i : σ) => X i ^ d i

@[simp]

theorem MvPolynomial.eval₂_zero {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σ → S₁) : MvPolynomial.eval₂ f g 0 = 0

@[simp]

theorem MvPolynomial.eval₂_add {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] {p : MvPolynomial σ R} {q : MvPolynomial σ R} (f : R →+* S₁) (g : σ → S₁) : MvPolynomial.eval₂ f g (p + q) = MvPolynomial.eval₂ f g p + MvPolynomial.eval₂ f g q

@[simp]

theorem MvPolynomial.eval₂_monomial {R : Type u} {S₁ : Type v} {σ : Type u_1} {a : R} {s : σ →₀ ℕ} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σ → S₁) : MvPolynomial.eval₂ f g ((MvPolynomial.monomial s) a) = 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} [CommSemiring R] [CommSemiring S₁] (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} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σ → S₁) : MvPolynomial.eval₂ f g 1 = 1

@[simp]

theorem MvPolynomial.eval₂_X {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σ → S₁) (n : σ) : MvPolynomial.eval₂ f g (MvPolynomial.X n) = g n

theorem MvPolynomial.eval₂_mul_monomial {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] {p : MvPolynomial σ R} (f : R →+* S₁) (g : σ → S₁) {s : σ →₀ ℕ} {a : R} : MvPolynomial.eval₂ f g (p * (MvPolynomial.monomial s) a) = 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} [CommSemiring R] [CommSemiring S₁] {p : MvPolynomial σ R} (f : R →+* S₁) (g : σ → S₁) : MvPolynomial.eval₂ f g (p * MvPolynomial.C a) = MvPolynomial.eval₂ f g p * f a

@[simp]

theorem MvPolynomial.eval₂_mul {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] {q : MvPolynomial σ R} (f : R →+* S₁) (g : σ → S₁) {p : MvPolynomial σ R} : MvPolynomial.eval₂ f g (p * q) = MvPolynomial.eval₂ f g p * MvPolynomial.eval₂ f g q

@[simp]

theorem MvPolynomial.eval₂_pow {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σ → S₁) {p : MvPolynomial σ R} {n : ℕ} : MvPolynomial.eval₂ f g (p ^ n) = MvPolynomial.eval₂ f g p ^ n

def MvPolynomial.eval₂Hom {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σ → S₁) : MvPolynomial σ R →+* S₁

MvPolynomial.eval₂ as a RingHom.

Equations

• MvPolynomial.eval₂Hom f g = { toMonoidHom := { toOneHom := { toFun := MvPolynomial.eval₂ f g, map_one' := ⋯ }, map_mul' := ⋯ }, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem MvPolynomial.coe_eval₂Hom {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σ → S₁) : ⇑(MvPolynomial.eval₂Hom f g) = MvPolynomial.eval₂ f g

theorem MvPolynomial.eval₂Hom_congr {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] {f₁ : R →+* S₁} {f₂ : R →+* S₁} {g₁ : σ → S₁} {g₂ : σ → S₁} {p₁ : MvPolynomial σ R} {p₂ : MvPolynomial σ R} : f₁ = f₂ → g₁ = g₂ → p₁ = p₂ → (MvPolynomial.eval₂Hom f₁ g₁) p₁ = (MvPolynomial.eval₂Hom f₂ g₂) p₂

@[simp]

theorem MvPolynomial.eval₂Hom_C {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σ → S₁) (r : R) : (MvPolynomial.eval₂Hom f g) (MvPolynomial.C r) = f r

@[simp]

theorem MvPolynomial.eval₂Hom_X' {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σ → S₁) (i : σ) : (MvPolynomial.eval₂Hom f g) (MvPolynomial.X i) = g i

@[simp]

theorem MvPolynomial.comp_eval₂Hom {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [CommSemiring S₂] (f : R →+* S₁) (g : σ → S₁) (φ : S₁ →+* S₂) : RingHom.comp φ (MvPolynomial.eval₂Hom f g) = MvPolynomial.eval₂Hom (RingHom.comp φ f) fun (i : σ) => φ (g i)

theorem MvPolynomial.map_eval₂Hom {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [CommSemiring S₂] (f : R →+* S₁) (g : σ → S₁) (φ : S₁ →+* S₂) (p : MvPolynomial σ R) : φ ((MvPolynomial.eval₂Hom f g) p) = (MvPolynomial.eval₂Hom (RingHom.comp φ f) fun (i : σ) => φ (g i)) p

theorem MvPolynomial.eval₂Hom_monomial {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σ → S₁) (d : σ →₀ ℕ) (r : R) : (MvPolynomial.eval₂Hom f g) ((MvPolynomial.monomial d) 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} [CommSemiring R] [CommSemiring S₁] {S₂ : Type u_2} [CommSemiring S₂] (k : S₁ →+* S₂) (f : R →+* S₁) (g : σ → S₁) (p : MvPolynomial σ R) : k (MvPolynomial.eval₂ f g p) = MvPolynomial.eval₂ (RingHom.comp k f) (⇑k ∘ g) p

@[simp]

theorem MvPolynomial.eval₂_eta {R : Type u} {σ : Type u_1} [CommSemiring R] (p : MvPolynomial σ R) : MvPolynomial.eval₂ MvPolynomial.C MvPolynomial.X p = p

theorem MvPolynomial.eval₂_congr {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] {p : MvPolynomial σ R} (f : R →+* S₁) (g₁ : σ → S₁) (g₂ : σ → S₁) (h : ∀ {i : σ} {c : σ →₀ ℕ}, i ∈ c.support → MvPolynomial.coeff c p ≠ 0 → g₁ i = g₂ i) : MvPolynomial.eval₂ f g₁ p = MvPolynomial.eval₂ f g₂ p

@[simp]

theorem MvPolynomial.eval₂_sum {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σ → S₁) (s : Finset S₂) (p : S₂ → MvPolynomial σ R) : 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} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σ → S₁) (s : Finset S₂) (p : S₂ → MvPolynomial σ R) : 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} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σ → S₁) (q : S₂ → MvPolynomial σ R) (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} [CommSemiring R] (f : σ → R) : MvPolynomial σ R →+* R

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

Equations

• MvPolynomial.eval f = MvPolynomial.eval₂Hom (RingHom.id R) f

theorem MvPolynomial.eval_eq {R : Type u} {σ : Type u_1} [CommSemiring R] (X : σ → R) (f : MvPolynomial σ R) : (MvPolynomial.eval X) f = Finset.sum (MvPolynomial.support f) fun (d : σ →₀ ℕ) => MvPolynomial.coeff d f * Finset.prod d.support fun (i : σ) => X i ^ d i

theorem MvPolynomial.eval_eq' {R : Type u} {σ : Type u_1} [CommSemiring R] [Fintype σ] (X : σ → R) (f : MvPolynomial σ R) : (MvPolynomial.eval X) f = Finset.sum (MvPolynomial.support f) fun (d : σ →₀ ℕ) => MvPolynomial.coeff d f * Finset.prod Finset.univ fun (i : σ) => X i ^ d i

theorem MvPolynomial.eval_monomial {R : Type u} {σ : Type u_1} {a : R} {s : σ →₀ ℕ} [CommSemiring R] {f : σ → R} : (MvPolynomial.eval f) ((MvPolynomial.monomial s) a) = a * Finsupp.prod s fun (n : σ) (e : ℕ) => f n ^ e

@[simp]

theorem MvPolynomial.eval_C {R : Type u} {σ : Type u_1} [CommSemiring R] {f : σ → R} (a : R) : (MvPolynomial.eval f) (MvPolynomial.C a) = a

@[simp]

theorem MvPolynomial.eval_X {R : Type u} {σ : Type u_1} [CommSemiring R] {f : σ → R} (n : σ) : (MvPolynomial.eval f) (MvPolynomial.X n) = f n

@[simp]

theorem MvPolynomial.smul_eval {R : Type u} {σ : Type u_1} [CommSemiring R] (x : σ → R) (p : MvPolynomial σ R) (s : R) : (MvPolynomial.eval x) (s • p) = s * (MvPolynomial.eval x) p

theorem MvPolynomial.eval_add {R : Type u} {σ : Type u_1} [CommSemiring R] {p : MvPolynomial σ R} {q : MvPolynomial σ R} {f : σ → R} : (MvPolynomial.eval f) (p + q) = (MvPolynomial.eval f) p + (MvPolynomial.eval f) q

theorem MvPolynomial.eval_mul {R : Type u} {σ : Type u_1} [CommSemiring R] {p : MvPolynomial σ R} {q : MvPolynomial σ R} {f : σ → R} : (MvPolynomial.eval f) (p * q) = (MvPolynomial.eval f) p * (MvPolynomial.eval f) q

theorem MvPolynomial.eval_pow {R : Type u} {σ : Type u_1} [CommSemiring R] {p : MvPolynomial σ R} {f : σ → R} (n : ℕ) : (MvPolynomial.eval f) (p ^ n) = (MvPolynomial.eval f) p ^ n

theorem MvPolynomial.eval_sum {R : Type u} {σ : Type u_1} [CommSemiring R] {ι : Type u_2} (s : Finset ι) (f : ι → MvPolynomial σ R) (g : σ → R) : (MvPolynomial.eval g) (Finset.sum s fun (i : ι) => f i) = Finset.sum s fun (i : ι) => (MvPolynomial.eval g) (f i)

theorem MvPolynomial.eval_prod {R : Type u} {σ : Type u_1} [CommSemiring R] {ι : Type u_2} (s : Finset ι) (f : ι → MvPolynomial σ R) (g : σ → R) : (MvPolynomial.eval g) (Finset.prod s fun (i : ι) => f i) = Finset.prod s fun (i : ι) => (MvPolynomial.eval g) (f i)

theorem MvPolynomial.eval_assoc {R : Type u} {σ : Type u_1} [CommSemiring R] {τ : Type u_2} (f : σ → MvPolynomial τ R) (g : τ → R) (p : MvPolynomial σ R) : (MvPolynomial.eval (⇑(MvPolynomial.eval g) ∘ f)) p = (MvPolynomial.eval g) (MvPolynomial.eval₂ MvPolynomial.C f p)

@[simp]

theorem MvPolynomial.eval₂_id {R : Type u} {σ : Type u_1} [CommSemiring R] {g : σ → R} (p : MvPolynomial σ R) : MvPolynomial.eval₂ (RingHom.id R) g p = (MvPolynomial.eval g) p

theorem MvPolynomial.eval_eval₂ {R : Type u} {σ : Type u_1} {S : Type u_2} {τ : Type u_3} {x : τ → S} [CommSemiring R] [CommSemiring S] (f : R →+* MvPolynomial τ S) (g : σ → MvPolynomial τ S) (p : MvPolynomial σ R) : (MvPolynomial.eval x) (MvPolynomial.eval₂ f g p) = MvPolynomial.eval₂ (RingHom.comp (MvPolynomial.eval x) f) (fun (s : σ) => (MvPolynomial.eval x) (g s)) p

def MvPolynomial.map {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) : MvPolynomial σ R →+* MvPolynomial σ S₁

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

Equations

• MvPolynomial.map f = MvPolynomial.eval₂Hom (RingHom.comp MvPolynomial.C f) MvPolynomial.X

@[simp]

theorem MvPolynomial.map_monomial {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (s : σ →₀ ℕ) (a : R) : (MvPolynomial.map f) ((MvPolynomial.monomial s) a) = (MvPolynomial.monomial s) (f a)

@[simp]

theorem MvPolynomial.map_C {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (a : R) : (MvPolynomial.map f) (MvPolynomial.C a) = MvPolynomial.C (f a)

@[simp]

theorem MvPolynomial.map_X {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (n : σ) : (MvPolynomial.map f) (MvPolynomial.X n) = MvPolynomial.X n

theorem MvPolynomial.map_id {R : Type u} {σ : Type u_1} [CommSemiring R] (p : MvPolynomial σ R) : (MvPolynomial.map (RingHom.id R)) p = p

theorem MvPolynomial.map_map {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) [CommSemiring S₂] (g : S₁ →+* S₂) (p : MvPolynomial σ R) : (MvPolynomial.map g) ((MvPolynomial.map f) p) = (MvPolynomial.map (RingHom.comp g f)) p

theorem MvPolynomial.eval₂_eq_eval_map {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σ → S₁) (p : MvPolynomial σ R) : MvPolynomial.eval₂ f g p = (MvPolynomial.eval g) ((MvPolynomial.map f) p)

theorem MvPolynomial.eval₂_comp_right {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] {S₂ : Type u_2} [CommSemiring S₂] (k : S₁ →+* S₂) (f : R →+* S₁) (g : σ → S₁) (p : MvPolynomial σ R) : k (MvPolynomial.eval₂ f g p) = MvPolynomial.eval₂ k (⇑k ∘ g) ((MvPolynomial.map f) p)

theorem MvPolynomial.map_eval₂ {R : Type u} {S₁ : Type v} {S₂ : Type w} {S₃ : Type x} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : S₂ → MvPolynomial S₃ R) (p : MvPolynomial S₂ R) : (MvPolynomial.map f) (MvPolynomial.eval₂ MvPolynomial.C g p) = MvPolynomial.eval₂ MvPolynomial.C (⇑(MvPolynomial.map f) ∘ g) ((MvPolynomial.map f) p)

theorem MvPolynomial.coeff_map {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (p : MvPolynomial σ R) (m : σ →₀ ℕ) : MvPolynomial.coeff m ((MvPolynomial.map f) p) = f (MvPolynomial.coeff m p)

theorem MvPolynomial.map_injective {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (hf : Function.Injective ⇑f) : Function.Injective ⇑(MvPolynomial.map f)

theorem MvPolynomial.map_surjective {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (hf : Function.Surjective ⇑f) : Function.Surjective ⇑(MvPolynomial.map f)

theorem MvPolynomial.map_leftInverse {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] {f : R →+* S₁} {g : S₁ →+* R} (hf : Function.LeftInverse ⇑f ⇑g) : Function.LeftInverse ⇑(MvPolynomial.map f) ⇑(MvPolynomial.map g)

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} [CommSemiring R] [CommSemiring S₁] {f : R →+* S₁} {g : S₁ →+* R} (hf : Function.RightInverse ⇑f ⇑g) : Function.RightInverse ⇑(MvPolynomial.map f) ⇑(MvPolynomial.map g)

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} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : σ → S₁) (p : MvPolynomial σ R) : (MvPolynomial.eval g) ((MvPolynomial.map f) p) = MvPolynomial.eval₂ f g p

@[simp]

theorem MvPolynomial.eval₂_map {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [CommSemiring S₂] (f : R →+* S₁) (g : σ → S₂) (φ : S₁ →+* S₂) (p : MvPolynomial σ R) : MvPolynomial.eval₂ φ g ((MvPolynomial.map f) p) = MvPolynomial.eval₂ (RingHom.comp φ f) g p

@[simp]

theorem MvPolynomial.eval₂Hom_map_hom {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [CommSemiring S₂] (f : R →+* S₁) (g : σ → S₂) (φ : S₁ →+* S₂) (p : MvPolynomial σ R) : (MvPolynomial.eval₂Hom φ g) ((MvPolynomial.map f) p) = (MvPolynomial.eval₂Hom (RingHom.comp φ f) g) p

@[simp]

theorem MvPolynomial.constantCoeff_map {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (φ : MvPolynomial σ R) : MvPolynomial.constantCoeff ((MvPolynomial.map f) φ) = f (MvPolynomial.constantCoeff φ)

theorem MvPolynomial.constantCoeff_comp_map {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) : RingHom.comp MvPolynomial.constantCoeff (MvPolynomial.map f) = RingHom.comp f MvPolynomial.constantCoeff

theorem MvPolynomial.support_map_subset {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (p : MvPolynomial σ R) : MvPolynomial.support ((MvPolynomial.map f) p) ⊆ MvPolynomial.support p

theorem MvPolynomial.support_map_of_injective {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (p : MvPolynomial σ R) {f : R →+* S₁} (hf : Function.Injective ⇑f) : MvPolynomial.support ((MvPolynomial.map f) p) = MvPolynomial.support p

theorem MvPolynomial.C_dvd_iff_map_hom_eq_zero {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (q : R →+* S₁) (r : R) (hr : ∀ (r' : R), q r' = 0 ↔ r ∣ r') (φ : MvPolynomial σ R) : MvPolynomial.C r ∣ φ ↔ (MvPolynomial.map q) φ = 0

theorem MvPolynomial.map_mapRange_eq_iff {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] (f : R →+* S₁) (g : S₁ → R) (hg : g 0 = 0) (φ : MvPolynomial σ S₁) : (MvPolynomial.map f) (Finsupp.mapRange g hg φ) = φ ↔ ∀ (d : σ →₀ ℕ), f (g (MvPolynomial.coeff d φ)) = MvPolynomial.coeff d φ

@[simp]

theorem MvPolynomial.mapAlgHom_apply {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [CommSemiring S₂] [Algebra R S₁] [Algebra R S₂] (f : S₁ →ₐ[R] S₂) (p : MvPolynomial σ S₁) : (MvPolynomial.mapAlgHom f) p = 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} [CommSemiring R] [CommSemiring S₁] [CommSemiring S₂] [Algebra R S₁] [Algebra R S₂] (f : S₁ →ₐ[R] S₂) : MvPolynomial σ S₁ →ₐ[R] MvPolynomial σ S₂

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

Equations

• MvPolynomial.mapAlgHom f = let __src := MvPolynomial.map ↑f; { toRingHom := __src, commutes' := ⋯ }

@[simp]

theorem MvPolynomial.mapAlgHom_id {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] : MvPolynomial.mapAlgHom (AlgHom.id 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} [CommSemiring R] [CommSemiring S₁] [CommSemiring S₂] [Algebra R S₁] [Algebra R S₂] (f : S₁ →ₐ[R] S₂) : ↑(MvPolynomial.mapAlgHom f) = MvPolynomial.map ↑f

The algebra of multivariate polynomials

theorem MvPolynomial.algebraMap_apply {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [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} [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] (f : σ → S₁) : MvPolynomial σ 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

• MvPolynomial.aeval f = let __src := MvPolynomial.eval₂Hom (algebraMap R S₁) f; { toRingHom := __src, commutes' := ⋯ }

theorem MvPolynomial.aeval_def {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] (f : σ → S₁) (p : MvPolynomial σ R) : (MvPolynomial.aeval f) p = MvPolynomial.eval₂ (algebraMap R S₁) f p

theorem MvPolynomial.aeval_eq_eval₂Hom {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] (f : σ → S₁) (p : MvPolynomial σ R) : (MvPolynomial.aeval f) p = (MvPolynomial.eval₂Hom (algebraMap R S₁) f) p

@[simp]

theorem MvPolynomial.aeval_X {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] (f : σ → S₁) (s : σ) : (MvPolynomial.aeval f) (MvPolynomial.X s) = f s

@[simp]

theorem MvPolynomial.aeval_C {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] (f : σ → S₁) (r : R) : (MvPolynomial.aeval f) (MvPolynomial.C r) = (algebraMap R S₁) r

theorem MvPolynomial.aeval_unique {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] (φ : MvPolynomial σ R →ₐ[R] S₁) : φ = MvPolynomial.aeval (⇑φ ∘ MvPolynomial.X)

theorem MvPolynomial.aeval_X_left {R : Type u} {σ : Type u_1} [CommSemiring R] : MvPolynomial.aeval MvPolynomial.X = AlgHom.id R (MvPolynomial σ R)

theorem MvPolynomial.aeval_X_left_apply {R : Type u} {σ : Type u_1} [CommSemiring R] (p : MvPolynomial σ R) : (MvPolynomial.aeval MvPolynomial.X) p = p

theorem MvPolynomial.comp_aeval {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] (f : σ → S₁) {B : Type u_2} [CommSemiring B] [Algebra R B] (φ : S₁ →ₐ[R] B) : AlgHom.comp φ (MvPolynomial.aeval f) = MvPolynomial.aeval fun (i : σ) => φ (f i)

@[simp]

theorem MvPolynomial.map_aeval {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] {B : Type u_2} [CommSemiring B] (g : σ → S₁) (φ : S₁ →+* B) (p : MvPolynomial σ R) : φ ((MvPolynomial.aeval g) 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} [CommSemiring R] [CommSemiring S₂] (f : R →+* S₂) : MvPolynomial.eval₂Hom f 0 = RingHom.comp f MvPolynomial.constantCoeff

@[simp]

theorem MvPolynomial.eval₂Hom_zero' {R : Type u} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₂] (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} [CommSemiring R] [CommSemiring S₂] (f : R →+* S₂) (p : MvPolynomial σ R) : (MvPolynomial.eval₂Hom f 0) p = f (MvPolynomial.constantCoeff p)

theorem MvPolynomial.eval₂Hom_zero'_apply {R : Type u} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₂] (f : R →+* S₂) (p : MvPolynomial σ R) : (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} [CommSemiring R] [CommSemiring S₂] (f : R →+* S₂) (p : MvPolynomial σ R) : MvPolynomial.eval₂ f 0 p = f (MvPolynomial.constantCoeff p)

@[simp]

theorem MvPolynomial.eval₂_zero'_apply {R : Type u} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₂] (f : R →+* S₂) (p : MvPolynomial σ R) : 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} [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] (p : MvPolynomial σ R) : (MvPolynomial.aeval 0) p = (algebraMap R S₁) (MvPolynomial.constantCoeff p)

@[simp]

theorem MvPolynomial.aeval_zero' {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] (p : MvPolynomial σ R) : (MvPolynomial.aeval fun (x : σ) => 0) p = (algebraMap R S₁) (MvPolynomial.constantCoeff p)

@[simp]

theorem MvPolynomial.eval_zero {R : Type u} {σ : Type u_1} [CommSemiring R] : MvPolynomial.eval 0 = MvPolynomial.constantCoeff

@[simp]

theorem MvPolynomial.eval_zero' {R : Type u} {σ : Type u_1} [CommSemiring R] : (MvPolynomial.eval fun (x : σ) => 0) = MvPolynomial.constantCoeff

theorem MvPolynomial.aeval_monomial {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] (g : σ → S₁) (d : σ →₀ ℕ) (r : R) : (MvPolynomial.aeval g) ((MvPolynomial.monomial d) 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} [CommSemiring R] [CommSemiring S₂] (f : R →+* S₂) (g : σ → S₂) (φ : MvPolynomial σ R) (h : ∀ (d : σ →₀ ℕ), MvPolynomial.coeff d φ ≠ 0 → ∃ i ∈ d.support, g i = 0) : (MvPolynomial.eval₂Hom f g) φ = 0

theorem MvPolynomial.aeval_eq_zero {R : Type u} {S₂ : Type w} {σ : Type u_1} [CommSemiring R] [CommSemiring S₂] [Algebra R S₂] (f : σ → S₂) (φ : MvPolynomial σ R) (h : ∀ (d : σ →₀ ℕ), MvPolynomial.coeff d φ ≠ 0 → ∃ i ∈ d.support, f i = 0) : (MvPolynomial.aeval f) φ = 0

theorem MvPolynomial.aeval_sum {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] (f : σ → S₁) {ι : Type u_2} (s : Finset ι) (φ : ι → MvPolynomial σ R) : (MvPolynomial.aeval f) (Finset.sum s fun (i : ι) => φ i) = Finset.sum s fun (i : ι) => (MvPolynomial.aeval f) (φ i)

theorem MvPolynomial.aeval_prod {R : Type u} {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] (f : σ → S₁) {ι : Type u_2} (s : Finset ι) (φ : ι → MvPolynomial σ R) : (MvPolynomial.aeval f) (Finset.prod s fun (i : ι) => φ i) = Finset.prod s fun (i : ι) => (MvPolynomial.aeval f) (φ i)

theorem Algebra.adjoin_range_eq_range_aeval (R : Type u) {S₁ : Type v} {σ : Type u_1} [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] (f : σ → S₁) : Algebra.adjoin R (Set.range f) = AlgHom.range (MvPolynomial.aeval f)

theorem Algebra.adjoin_eq_range (R : Type u) {S₁ : Type v} [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] (s : Set S₁) : Algebra.adjoin R s = AlgHom.range (MvPolynomial.aeval Subtype.val)

def MvPolynomial.aevalTower {R : Type u} {σ : Type u_1} [CommSemiring R] {S : Type u_2} {A : Type u_3} [CommSemiring S] [CommSemiring A] [Algebra S R] [Algebra S A] (f : R →ₐ[S] A) (X : σ → A) : MvPolynomial σ R →ₐ[S] A

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

Equations

• MvPolynomial.aevalTower f X = let __src := MvPolynomial.eval₂Hom (↑f) X; { toRingHom := __src, commutes' := ⋯ }

@[simp]

theorem MvPolynomial.aevalTower_X {R : Type u} {σ : Type u_1} [CommSemiring R] {S : Type u_2} {A : Type u_3} [CommSemiring S] [CommSemiring A] [Algebra S R] [Algebra S A] (g : R →ₐ[S] A) (y : σ → A) (i : σ) : (MvPolynomial.aevalTower g y) (MvPolynomial.X i) = y i

@[simp]

theorem MvPolynomial.aevalTower_C {R : Type u} {σ : Type u_1} [CommSemiring R] {S : Type u_2} {A : Type u_3} [CommSemiring S] [CommSemiring A] [Algebra S R] [Algebra S A] (g : R →ₐ[S] A) (y : σ → A) (x : R) : (MvPolynomial.aevalTower g y) (MvPolynomial.C x) = g x

@[simp]

theorem MvPolynomial.aevalTower_comp_C {R : Type u} {σ : Type u_1} [CommSemiring R] {S : Type u_2} {A : Type u_3} [CommSemiring S] [CommSemiring A] [Algebra S R] [Algebra S A] (g : R →ₐ[S] A) (y : σ → A) : RingHom.comp (↑(MvPolynomial.aevalTower g y)) MvPolynomial.C = ↑g

@[simp]

theorem MvPolynomial.aevalTower_algebraMap {R : Type u} {σ : Type u_1} [CommSemiring R] {S : Type u_2} {A : Type u_3} [CommSemiring S] [CommSemiring A] [Algebra S R] [Algebra S A] (g : R →ₐ[S] A) (y : σ → A) (x : R) : (MvPolynomial.aevalTower g y) ((algebraMap R (MvPolynomial σ R)) x) = g x

@[simp]

theorem MvPolynomial.aevalTower_comp_algebraMap {R : Type u} {σ : Type u_1} [CommSemiring R] {S : Type u_2} {A : Type u_3} [CommSemiring S] [CommSemiring A] [Algebra S R] [Algebra S A] (g : R →ₐ[S] A) (y : σ → A) : RingHom.comp (↑(MvPolynomial.aevalTower g y)) (algebraMap R (MvPolynomial σ R)) = ↑g

theorem MvPolynomial.aevalTower_toAlgHom {R : Type u} {σ : Type u_1} [CommSemiring R] {S : Type u_2} {A : Type u_3} [CommSemiring S] [CommSemiring A] [Algebra S R] [Algebra S A] (g : R →ₐ[S] A) (y : σ → A) (x : R) : (MvPolynomial.aevalTower g y) ((IsScalarTower.toAlgHom S R (MvPolynomial σ R)) x) = g x

@[simp]

theorem MvPolynomial.aevalTower_comp_toAlgHom {R : Type u} {σ : Type u_1} [CommSemiring R] {S : Type u_2} {A : Type u_3} [CommSemiring S] [CommSemiring A] [Algebra S R] [Algebra S A] (g : R →ₐ[S] A) (y : σ → A) : AlgHom.comp (MvPolynomial.aevalTower g y) (IsScalarTower.toAlgHom S R (MvPolynomial σ R)) = g

@[simp]

theorem MvPolynomial.aevalTower_id {σ : Type u_1} {S : Type u_2} [CommSemiring S] : MvPolynomial.aevalTower (AlgHom.id S S) = MvPolynomial.aeval

@[simp]

theorem MvPolynomial.aevalTower_ofId {σ : Type u_1} {S : Type u_2} {A : Type u_3} [CommSemiring S] [CommSemiring A] [Algebra S A] : MvPolynomial.aevalTower (Algebra.ofId S A) = MvPolynomial.aeval

theorem MvPolynomial.eval₂_mem {R : Type u} {σ : Type u_1} [CommSemiring R] {S : Type u_2} {subS : Type u_3} [CommSemiring S] [SetLike subS S] [SubsemiringClass subS S] {f : R →+* S} {p : MvPolynomial σ R} {s : subS} (hs : ∀ i ∈ MvPolynomial.support p, f (MvPolynomial.coeff i p) ∈ s) {v : σ → S} (hv : ∀ (i : σ), v i ∈ s) : MvPolynomial.eval₂ f v p ∈ s

theorem MvPolynomial.eval_mem {σ : Type u_1} {S : Type u_2} {subS : Type u_3} [CommSemiring S] [SetLike subS S] [SubsemiringClass subS S] {p : MvPolynomial σ S} {s : subS} (hs : ∀ i ∈ MvPolynomial.support p, MvPolynomial.coeff i p ∈ s) {v : σ → S} (hv : ∀ (i : σ), v i ∈ s) : (MvPolynomial.eval v) p ∈ s