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.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] {M : MvPolynomial σ R → Prop} (h_C : ∀ (a : R), M (C a)) (h_X : ∀ (p : MvPolynomial σ R) (n : σ), M p → M (p * X n)) (s : σ →₀ ℕ) (a : R) : M ((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 ((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 (C a)) (h_add_weak : ∀ (a : σ →₀ ℕ) (b : R) (f : (σ →₀ ℕ) →₀ R), a ∉ f.support → b ≠ 0 → M f → M ((let_fun this := (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 (C a)) (h_add_weak : ∀ (a : σ →₀ ℕ) (b : R) (f : (σ →₀ ℕ) →₀ R), a ∉ f.support → b ≠ 0 → M f → M ((monomial a) b) → M ((let_fun this := (monomial a) b; this) + f)) (h_X : ∀ (p : MvPolynomial σ R) (n : σ), M p → M (p * 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 (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 * 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 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)