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.

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₁)

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₂)

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₂)

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₁)

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₁)

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₁)

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 = AddMonoidAlgebra.lsingle s

theorem MvPolynomial.one_def {R : Type u} {σ : Type u_1} [CommSemiring R] : 1 = (monomial 0) 1

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

theorem MvPolynomial.mul_def {R : Type u} {σ : Type u_1} [CommSemiring R] {p q : MvPolynomial σ R} : p * q = Finsupp.sum p fun (m : σ →₀ ℕ) (a : R) => Finsupp.sum q fun (n : σ →₀ ℕ) (b : R) => (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

• MvPolynomial.C = { toFun := ⇑(MvPolynomial.monomial 0), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem MvPolynomial.algebraMap_eq (R : Type u) (σ : Type u_1) [CommSemiring R] : algebraMap R (MvPolynomial σ R) = 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 : σ →₀ ℕ) => (monomial s) r

@[simp]

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

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

@[simp]

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

@[simp]

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

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

@[simp]

theorem MvPolynomial.C_add {R : Type u} {σ : Type u_1} {a a' : R} [CommSemiring R] : C (a + a') = C a + C a'

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

theorem MvPolynomial.C_ne_zero {R : Type u} {σ : Type u_1} {a : R} [CommSemiring R] : C a ≠ 0 ↔ a ≠ 0

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

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

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

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

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

theorem MvPolynomial.C_eq_smul_one {R : Type u} {σ : Type u_1} {a : R} [CommSemiring R] : 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 • (monomial s) a = (monomial s) (r • a)

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

@[simp]

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

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

@[simp]

theorem MvPolynomial.monomial_mul {R : Type u} {σ : Type u_1} [CommSemiring R] {s s' : σ →₀ ℕ} {a b : R} : (monomial s) a * (monomial s') b = (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] : (monomialOneHom R σ) s = (monomial s) 1

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

theorem MvPolynomial.monomial_eq_zero {R : Type u} {σ : Type u_1} [CommSemiring R] {s : σ →₀ ℕ} {b : R} : (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 ((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 (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 : α → σ →₀ ℕ) : (monomial (∑ i ∈ s, f i)) 1 = ∏ i ∈ s, (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) : (monomial (∑ i ∈ s, f i)) a = C a * ∏ i ∈ s, (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) : (monomial (f.sum g)) a = C a * f.prod fun (a : α) (b : β) => (monomial (g a b)) 1

theorem MvPolynomial.monomial_eq_monomial_iff {R : Type u} [CommSemiring R] {α : Type u_2} (a₁ a₂ : α →₀ ℕ) (b₁ b₂ : R) : (monomial a₁) b₁ = (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] : (monomial s) a = C a * s.prod fun (n : σ) (e : ℕ) => X n ^ e

@[simp]

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

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

theorem MvPolynomial.induction_on' {R : Type u} {σ : Type u_1} [CommSemiring R] {P : MvPolynomial σ R → Prop} (p : MvPolynomial σ R) (monomial : ∀ (u : σ →₀ ℕ) (a : R), P ((monomial u) a)) (add : ∀ (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.monomial_add_induction_on {R : Type u} {σ : Type u_1} [CommSemiring R] {motive : MvPolynomial σ R → Prop} (p : MvPolynomial σ R) (C : ∀ (a : R), motive (C a)) (monomial_add : ∀ (a : σ →₀ ℕ) (b : R) (f : MvPolynomial σ R), a ∉ f.support → b ≠ 0 → motive f → motive ((monomial a) b + f)) : motive p

Similar to MvPolynomial.induction_on but only a weak form of h_add is required. In particular, this version only requires us to show that motive is closed under addition of nontrivial monomials not present in the support.

@[deprecated MvPolynomial.monomial_add_induction_on (since := "2025-03-11")]

theorem MvPolynomial.induction_on''' {R : Type u} {σ : Type u_1} [CommSemiring R] {motive : MvPolynomial σ R → Prop} (p : MvPolynomial σ R) (C : ∀ (a : R), motive (C a)) (monomial_add : ∀ (a : σ →₀ ℕ) (b : R) (f : MvPolynomial σ R), a ∉ f.support → b ≠ 0 → motive f → motive ((monomial a) b + f)) : motive p

Alias of MvPolynomial.monomial_add_induction_on.

---

Similar to MvPolynomial.induction_on but only a weak form of h_add is required. In particular, this version only requires us to show that motive is closed under addition of nontrivial monomials not present in the support.

theorem MvPolynomial.induction_on'' {R : Type u} {σ : Type u_1} [CommSemiring R] {motive : MvPolynomial σ R → Prop} (p : MvPolynomial σ R) (C : ∀ (a : R), motive (C a)) (monomial_add : ∀ (a : σ →₀ ℕ) (b : R) (f : MvPolynomial σ R), a ∉ f.support → b ≠ 0 → motive f → motive ((monomial a) b) → motive ((monomial a) b + f)) (mul_X : ∀ (p : MvPolynomial σ R) (n : σ), motive p → motive (p * X n)) : motive p

Similar to MvPolynomial.induction_on but only a yet weaker form of h_add is required. In particular, this version only requires us to show that motive is closed under addition of monomials not present in the support for which motive is already known to hold.

theorem MvPolynomial.induction_on {R : Type u} {σ : Type u_1} [CommSemiring R] {motive : MvPolynomial σ R → Prop} (p : MvPolynomial σ R) (C : ∀ (a : R), motive (C a)) (add : ∀ (p q : MvPolynomial σ R), motive p → motive q → motive (p + q)) (mul_X : ∀ (p : MvPolynomial σ R) (n : σ), motive p → motive (p * X n)) : motive p

Analog of Polynomial.induction_on. If a property holds for any constant polynomial and is preserved under addition and multiplication by variables then it holds for all multivariate polynomials.

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

theorem MvPolynomial.ringHom_ext' {R : Type u} {σ : Type u_1} [CommSemiring R] {A : Type u_2} [Semiring A] {f g : MvPolynomial σ R →+* A} (hC : f.comp C = g.comp C) (hX : ∀ (i : σ), f (X i) = g (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 g : MvPolynomial σ R →+* S₂) (hC : f.comp C = g.comp C) (hX : ∀ (n : σ), f (X n) = g (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 : f.comp C = C) (hX : ∀ (n : σ), f (X n) = 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 g : MvPolynomial σ A →ₐ[R] B} (h₁ : f.comp (IsScalarTower.toAlgHom R A (MvPolynomial σ A)) = g.comp (IsScalarTower.toAlgHom R A (MvPolynomial σ A))) (h₂ : ∀ (i : σ), f (X i) = g (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 g : MvPolynomial σ R →ₐ[R] A} (hf : ∀ (i : σ), f (X i) = g (X i)) : f = g

@[simp]

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

@[simp]

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

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

• p.support = p.support

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

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

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

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

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

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

@[simp]

theorem MvPolynomial.support_zero {R : Type u} {σ : Type u_1} [CommSemiring R] : 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} : (a • f).support ⊆ f.support

theorem MvPolynomial.support_sum {R : Type u} {σ : Type u_1} [CommSemiring R] {α : Type u_2} [DecidableEq σ] {s : Finset α} {f : α → MvPolynomial σ R} : (∑ x ∈ s, f x).support ⊆ s.biUnion fun (x : α) => (f x).support

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 ∈ p.support ↔ coeff m p ≠ 0

theorem MvPolynomial.not_mem_support_iff {R : Type u} {σ : Type u_1} [CommSemiring R] {p : MvPolynomial σ R} {m : σ →₀ ℕ} : m ∉ p.support ↔ 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 = ∑ m ∈ p.support, b m (coeff m p)

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

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

@[simp]

theorem MvPolynomial.coeff_add {R : Type u} {σ : Type u_1} [CommSemiring R] (m : σ →₀ ℕ) (p q : MvPolynomial σ R) : coeff m (p + q) = coeff m p + 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) : coeff m (C • p) = C • coeff m p

@[simp]

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

@[simp]

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

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 = { toFun := MvPolynomial.coeff m, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

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

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

MvPolynomial.coeff m but promoted to a LinearMap.

Equations

• MvPolynomial.lcoeff R m = { toFun := MvPolynomial.coeff m, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

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

theorem MvPolynomial.coeff_sum {R : Type u} {σ : Type u_1} [CommSemiring R] {X : Type u_2} (s : Finset X) (f : X → MvPolynomial σ R) (m : σ →₀ ℕ) : coeff m (∑ x ∈ s, f x) = ∑ x ∈ s, coeff m (f x)

theorem MvPolynomial.monic_monomial_eq {R : Type u} {σ : Type u_1} [CommSemiring R] (m : σ →₀ ℕ) : (monomial m) 1 = m.prod fun (n : σ) (e : ℕ) => X n ^ e

@[simp]

theorem MvPolynomial.coeff_monomial {R : Type u} {σ : Type u_1} [CommSemiring R] [DecidableEq σ] (m n : σ →₀ ℕ) (a : R) : coeff m ((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) : coeff m (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 = C (coeff 0 p)

theorem MvPolynomial.coeff_one {R : Type u} {σ : Type u_1} [CommSemiring R] [DecidableEq σ] (m : σ →₀ ℕ) : 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) : coeff 0 (C a) = a

@[simp]

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

theorem MvPolynomial.coeff_X_pow {R : Type u} {σ : Type u_1} [CommSemiring R] [DecidableEq σ] (i : σ) (m : σ →₀ ℕ) (k : ℕ) : coeff m (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 : σ →₀ ℕ) : coeff m (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 : σ) : coeff (Finsupp.single i 1) (X i) = 1

@[simp]

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

theorem MvPolynomial.coeff_mul {R : Type u} {σ : Type u_1} [CommSemiring R] [DecidableEq σ] (p q : MvPolynomial σ R) (n : σ →₀ ℕ) : coeff n (p * q) = ∑ x ∈ Finset.antidiagonal n, coeff x.1 p * 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) : coeff (m + s) (p * (monomial s) r) = 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) : coeff (s + m) ((monomial s) r * p) = r * coeff m p

@[simp]

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

@[simp]

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

theorem MvPolynomial.coeff_single_X_pow {R : Type u} {σ : Type u_1} [CommSemiring R] [DecidableEq σ] (s s' : σ) (n n' : ℕ) : coeff (Finsupp.single s' n') (X s ^ n) = if s = s' ∧ n = n' ∨ n = 0 ∧ n' = 0 then 1 else 0

@[simp]

theorem MvPolynomial.coeff_single_X {R : Type u} {σ : Type u_1} [CommSemiring R] [DecidableEq σ] (s s' : σ) (n : ℕ) : coeff (Finsupp.single s' n) (X s) = if n = 1 ∧ s = s' then 1 else 0

@[simp]

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

@[simp]

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

@[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) : (a • p).support = p.support

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

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

theorem MvPolynomial.coeff_mul_monomial' {R : Type u} {σ : Type u_1} [CommSemiring R] (m s : σ →₀ ℕ) (r : R) (p : MvPolynomial σ R) : coeff m (p * (monomial s) r) = if s ≤ m then 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) : coeff m ((monomial s) r * p) = if s ≤ m then r * 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) : coeff m (p * X s) = if s ∈ m.support then 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) : coeff m (X s * p) = if s ∈ m.support then 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 : σ →₀ ℕ), coeff d p = 0

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

@[simp]

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

@[simp]

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

@[simp]

theorem MvPolynomial.support_nonempty {R : Type u} {σ : Type u_1} [CommSemiring R] {p : MvPolynomial σ R} : p.support.Nonempty ↔ p ≠ 0

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

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

@[simp]

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

@[simp]

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

@[simp]

theorem MvPolynomial.isRegular_prod_X {R : Type u} {σ : Type u_1} [CommSemiring R] (s : Finset σ) : IsRegular (∏ n ∈ s, X n)

def MvPolynomial.coeffs {R : Type u} {σ : Type u_1} [CommSemiring R] (p : MvPolynomial σ R) : Finset R

The finset of nonzero coefficients of a multivariate polynomial.

Equations

• p.coeffs = Finset.image (fun (m : σ →₀ ℕ) => MvPolynomial.coeff m p) p.support

@[simp]

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

theorem MvPolynomial.coeffs_one {R : Type u} {σ : Type u_1} [CommSemiring R] : coeffs 1 ⊆ {1}

theorem MvPolynomial.coeffs_eq_empty_of_subsingleton {R : Type u} {σ : Type u_1} [CommSemiring R] [Subsingleton R] (p : MvPolynomial σ R) : p.coeffs = ∅

@[simp]

theorem MvPolynomial.coeffs_one_of_nontrivial {R : Type u} {σ : Type u_1} [CommSemiring R] [Nontrivial R] : coeffs 1 = {1}

theorem MvPolynomial.mem_coeffs_iff {R : Type u} {σ : Type u_1} [CommSemiring R] {p : MvPolynomial σ R} {c : R} : c ∈ p.coeffs ↔ ∃ n ∈ p.support, c = coeff n p

theorem MvPolynomial.coeff_mem_coeffs {R : Type u} {σ : Type u_1} [CommSemiring R] {p : MvPolynomial σ R} (m : σ →₀ ℕ) (h : coeff m p ≠ 0) : coeff m p ∈ p.coeffs

theorem MvPolynomial.zero_not_mem_coeffs {R : Type u} {σ : Type u_1} [CommSemiring R] (p : MvPolynomial σ R) : 0 ∉ p.coeffs

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 = { toFun := MvPolynomial.coeff 0, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

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

@[simp]

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

@[simp]

theorem MvPolynomial.constantCoeff_X (R : Type u) {σ : Type u_1} [CommSemiring R] (i : σ) : constantCoeff (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₁) : constantCoeff (a • f) = a • constantCoeff f

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

@[simp]

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

theorem MvPolynomial.constantCoeff_comp_algebraMap (R : Type u) (σ : Type u_1) [CommSemiring R] : constantCoeff.comp (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) : ∑ v ∈ p.support, (monomial v) (coeff v p) = p

theorem MvPolynomial.as_sum {R : Type u} {σ : Type u_1} [CommSemiring R] (p : MvPolynomial σ R) : p = ∑ v ∈ p.support, (monomial v) (coeff v p)

def MvPolynomial.coeffsIn {R : Type u_2} {S : Type u_3} (σ : Type u_4) [CommSemiring R] [CommSemiring S] [Module R S] (M : Submodule R S) : Submodule R (MvPolynomial σ S)

The R-submodule of multivariate polynomials whose coefficients lie in a R-submodule M.

Equations

• MvPolynomial.coeffsIn σ M = { carrier := {p : MvPolynomial σ S | ∀ (i : σ →₀ ℕ), MvPolynomial.coeff i p ∈ M}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[simp]

theorem MvPolynomial.coe_coeffsIn {R : Type u_2} {S : Type u_3} (σ : Type u_4) [CommSemiring R] [CommSemiring S] [Module R S] (M : Submodule R S) : ↑(coeffsIn σ M) = {p : MvPolynomial σ S | ∀ (i : σ →₀ ℕ), coeff i p ∈ M}

theorem MvPolynomial.mem_coeffsIn {R : Type u_2} {S : Type u_3} {σ : Type u_4} [CommSemiring R] [CommSemiring S] [Module R S] {M : Submodule R S} {p : MvPolynomial σ S} : p ∈ coeffsIn σ M ↔ ∀ (i : σ →₀ ℕ), coeff i p ∈ M

@[simp]

theorem MvPolynomial.monomial_mem_coeffsIn {R : Type u_2} {S : Type u_3} {σ : Type u_4} [CommSemiring R] [CommSemiring S] [Module R S] {M : Submodule R S} {i : σ →₀ ℕ} {x : S} : (monomial i) x ∈ coeffsIn σ M ↔ x ∈ M

@[simp]

theorem MvPolynomial.C_mem_coeffsIn {R : Type u_2} {S : Type u_3} {σ : Type u_4} [CommSemiring R] [CommSemiring S] [Module R S] {M : Submodule R S} {x : S} : C x ∈ coeffsIn σ M ↔ x ∈ M

@[simp]

theorem MvPolynomial.one_coeffsIn {R : Type u_2} {S : Type u_3} {σ : Type u_4} [CommSemiring R] [CommSemiring S] [Module R S] {M : Submodule R S} : 1 ∈ coeffsIn σ M ↔ 1 ∈ M

@[simp]

theorem MvPolynomial.mul_monomial_mem_coeffsIn {R : Type u_2} {S : Type u_3} {σ : Type u_4} [CommSemiring R] [CommSemiring S] [Module R S] {M : Submodule R S} {p : MvPolynomial σ S} {i : σ →₀ ℕ} : p * (monomial i) 1 ∈ coeffsIn σ M ↔ p ∈ coeffsIn σ M

@[simp]

theorem MvPolynomial.monomial_mul_mem_coeffsIn {R : Type u_2} {S : Type u_3} {σ : Type u_4} [CommSemiring R] [CommSemiring S] [Module R S] {M : Submodule R S} {p : MvPolynomial σ S} {i : σ →₀ ℕ} : (monomial i) 1 * p ∈ coeffsIn σ M ↔ p ∈ coeffsIn σ M

@[simp]

theorem MvPolynomial.mul_X_mem_coeffsIn {R : Type u_2} {S : Type u_3} {σ : Type u_4} [CommSemiring R] [CommSemiring S] [Module R S] {M : Submodule R S} {p : MvPolynomial σ S} {s : σ} : p * X s ∈ coeffsIn σ M ↔ p ∈ coeffsIn σ M

@[simp]

theorem MvPolynomial.X_mul_mem_coeffsIn {R : Type u_2} {S : Type u_3} {σ : Type u_4} [CommSemiring R] [CommSemiring S] [Module R S] {M : Submodule R S} {p : MvPolynomial σ S} {s : σ} : X s * p ∈ coeffsIn σ M ↔ p ∈ coeffsIn σ M

theorem MvPolynomial.coeffsIn_eq_span_monomial {R : Type u_2} {S : Type u_3} {σ : Type u_4} [CommSemiring R] [CommSemiring S] [Module R S] (M : Submodule R S) : coeffsIn σ M = Submodule.span R {x : MvPolynomial σ S | ∃ m ∈ M, ∃ (i : σ →₀ ℕ), (monomial i) m = x}

theorem MvPolynomial.coeffsIn_le {R : Type u_2} {S : Type u_3} {σ : Type u_4} [CommSemiring R] [CommSemiring S] [Module R S] {M : Submodule R S} {N : Submodule R (MvPolynomial σ S)} : coeffsIn σ M ≤ N ↔ ∀ m ∈ M, ∀ (i : σ →₀ ℕ), (monomial i) m ∈ N

theorem MvPolynomial.coeffsIn_mul {R : Type u_2} {S : Type u_3} {σ : Type u_4} [CommSemiring R] [CommSemiring S] [Algebra R S] (M N : Submodule R S) : coeffsIn σ (M * N) = coeffsIn σ M * coeffsIn σ N

theorem MvPolynomial.coeffsIn_pow {R : Type u_2} {S : Type u_3} {σ : Type u_4} [CommSemiring R] [CommSemiring S] [Algebra R S] {n : ℕ} : n ≠ 0 → ∀ (M : Submodule R S), coeffsIn σ (M ^ n) = coeffsIn σ M ^ n

theorem MvPolynomial.le_coeffsIn_pow {R : Type u_2} {S : Type u_3} {σ : Type u_4} [CommSemiring R] [CommSemiring S] [Algebra R S] {M : Submodule R S} {n : ℕ} : coeffsIn σ M ^ n ≤ coeffsIn σ (M ^ n)