Mathlib.Algebra.MvPolynomial.Basic

MvPolynomial definition

(σ : Type*) (R : Type*) [CommSemiring R]

Full source

/-- Multivariate polynomial, where `σ` is the index set of the variables and
  `R` is the coefficient ring -/
def MvPolynomial (σ : Type*) (R : Type*) [CommSemiring R] :=
  AddMonoidAlgebra R (σ →₀ ℕ)

Multivariate Polynomial Ring

Informal description

The type of multivariate polynomials with variables indexed by a type $\sigma$ and coefficients in a commutative semiring $R$. A polynomial is represented as a finitely supported function from monomials (given by $\sigma \to \mathbb{N}$) to coefficients in $R$.

MvPolynomial.decidableEqMvPolynomial instance

[CommSemiring R] [DecidableEq σ] [DecidableEq R] : DecidableEq (MvPolynomial σ R)

Full source

instance decidableEqMvPolynomial [CommSemiring R] [DecidableEq σ] [DecidableEq R] :
    DecidableEq (MvPolynomial σ R) :=
  Finsupp.instDecidableEq

Decidable Equality for Multivariate Polynomials

Informal description

For any commutative semiring $R$ and any type $\sigma$ with decidable equality, the type of multivariate polynomials $MvPolynomial(\sigma, R)$ has decidable equality when $R$ also has decidable equality.

MvPolynomial.commSemiring instance

[CommSemiring R] : CommSemiring (MvPolynomial σ R)

Full source

instance commSemiring [CommSemiring R] : CommSemiring (MvPolynomial σ R) :=
  AddMonoidAlgebra.commSemiring

Commutative Semiring Structure on Multivariate Polynomials

Informal description

For any commutative semiring $R$ and any type $\sigma$, the ring of multivariate polynomials $R[X_i : i \in \sigma]$ is a commutative semiring.

MvPolynomial.inhabited instance

[CommSemiring R] : Inhabited (MvPolynomial σ R)

Full source

instance inhabited [CommSemiring R] : Inhabited (MvPolynomial σ R) :=
  ⟨0⟩

Inhabitedness of Multivariate Polynomial Rings

Informal description

For any commutative semiring $R$ and any type $\sigma$, the ring of multivariate polynomials $R[X_i : i \in \sigma]$ is inhabited.

MvPolynomial.distribuMulAction instance

[Monoid R] [CommSemiring S₁] [DistribMulAction R S₁] : DistribMulAction R (MvPolynomial σ S₁)

Full source

instance distribuMulAction [Monoid R] [CommSemiring S₁] [DistribMulAction R S₁] :
    DistribMulAction R (MvPolynomial σ S₁) :=
  AddMonoidAlgebra.distribMulAction

Distributive Multiplicative Action on Multivariate Polynomials

Informal description

For any monoid $R$ and commutative semiring $S₁$ with a distributive multiplicative action of $R$ on $S₁$, the multivariate polynomial ring $S₁[X_i : i \in \sigma]$ inherits a distributive multiplicative action from $R$.

MvPolynomial.smulZeroClass instance

[CommSemiring S₁] [SMulZeroClass R S₁] : SMulZeroClass R (MvPolynomial σ S₁)

Full source

instance smulZeroClass [CommSemiring S₁] [SMulZeroClass R S₁] :
    SMulZeroClass R (MvPolynomial σ S₁) :=
  AddMonoidAlgebra.smulZeroClass

Scalar Multiplication on Multivariate Polynomials Preserves Zero

Informal description

For any commutative semiring $S₁$ and any type $\sigma$, the ring of multivariate polynomials $S₁[X_i : i \in \sigma]$ has a scalar multiplication structure that is compatible with the zero polynomial, i.e., $r \cdot 0 = 0$ for any scalar $r$ in $R$.

MvPolynomial.faithfulSMul instance

[CommSemiring S₁] [SMulZeroClass R S₁] [FaithfulSMul R S₁] : FaithfulSMul R (MvPolynomial σ S₁)

Full source

instance faithfulSMul [CommSemiring S₁] [SMulZeroClass R S₁] [FaithfulSMul R S₁] :
    FaithfulSMul R (MvPolynomial σ S₁) :=
  AddMonoidAlgebra.faithfulSMul

Faithful Scalar Multiplication on Multivariate Polynomials

Informal description

For any commutative semiring $S₁$, type $\sigma$, and scalar multiplication action of $R$ on $S₁$ that is faithful (i.e., distinct elements of $R$ act differently on $S₁$), the induced scalar multiplication action of $R$ on the multivariate polynomial ring $S₁[X_i : i \in \sigma]$ is also faithful.

MvPolynomial.module instance

[Semiring R] [CommSemiring S₁] [Module R S₁] : Module R (MvPolynomial σ S₁)

Full source

instance module [Semiring R] [CommSemiring S₁] [Module R S₁] : Module R (MvPolynomial σ S₁) :=
  AddMonoidAlgebra.module

Module Structure on Multivariate Polynomials

Informal description

For any semiring $R$ and commutative semiring $S₁$ with an $R$-module structure, the ring of multivariate polynomials $S₁[X_i : i \in \sigma]$ is also an $R$-module, where the scalar multiplication is defined coefficient-wise.

MvPolynomial.isScalarTower instance

 [CommSemiring S₂] [SMul R S₁] [SMulZeroClass R S₂] [SMulZeroClass S₁ S₂] [IsScalarTower R S₁ S₂] :
  IsScalarTower R S₁ (MvPolynomial σ S₂)

Full source

instance isScalarTower [CommSemiring S₂] [SMul R S₁] [SMulZeroClass R S₂] [SMulZeroClass S₁ S₂]
    [IsScalarTower R S₁ S₂] : IsScalarTower R S₁ (MvPolynomial σ S₂) :=
  AddMonoidAlgebra.isScalarTower

Scalar Multiplication Tower Property for Multivariate Polynomials

Informal description

For any commutative semiring $S₂$, and any scalar multiplication operations between $R$ and $S₁$, $R$ and $S₂$, and $S₁$ and $S₂$ that satisfy the tower property (i.e., $(r \cdot s₁) \cdot s₂ = r \cdot (s₁ \cdot s₂)$ for all $r \in R$, $s₁ \in S₁$, $s₂ \in S₂$), the ring of multivariate polynomials $S₂[X_i : i \in \sigma]$ also satisfies the tower property with respect to the scalar multiplications induced by $R$ and $S₁$.

MvPolynomial.smulCommClass instance

 [CommSemiring S₂] [SMulZeroClass R S₂] [SMulZeroClass S₁ S₂] [SMulCommClass R S₁ S₂] :
  SMulCommClass R S₁ (MvPolynomial σ S₂)

Full source

instance smulCommClass [CommSemiring S₂] [SMulZeroClass R S₂] [SMulZeroClass S₁ S₂]
    [SMulCommClass R S₁ S₂] : SMulCommClass R S₁ (MvPolynomial σ S₂) :=
  AddMonoidAlgebra.smulCommClass

Commutativity of Scalar Multiplication on Multivariate Polynomials

Informal description

For any commutative semiring $S₂$ and any type $\sigma$, if $R$ and $S₁$ are types with scalar multiplication structures on $S₂$ that commute with each other (i.e., $r \cdot (s \cdot a) = s \cdot (r \cdot a)$ for all $r \in R$, $s \in S₁$, and $a \in S₂$), then the scalar multiplications by $R$ and $S₁$ on the multivariate polynomial ring $S₂[X_i : i \in \sigma]$ also commute.

MvPolynomial.isCentralScalar instance

 [CommSemiring S₁] [SMulZeroClass R S₁] [SMulZeroClass Rᵐᵒᵖ S₁] [IsCentralScalar R S₁] :
  IsCentralScalar R (MvPolynomial σ S₁)

Full source

instance isCentralScalar [CommSemiring S₁] [SMulZeroClass R S₁] [SMulZeroClass Rᵐᵒᵖ S₁]
    [IsCentralScalar R S₁] : IsCentralScalar R (MvPolynomial σ S₁) :=
  AddMonoidAlgebra.isCentralScalar

Central Scalar Action on Multivariate Polynomials

Informal description

For any commutative semiring $S₁$ and any type $\sigma$, if $R$ has a scalar multiplication action on $S₁$ that is compatible with zero (i.e., $r \cdot 0 = 0$ for all $r \in R$) and the actions of $R$ and its multiplicative opposite $R^\text{op}$ on $S₁$ coincide, then the same holds for the multivariate polynomial ring $S₁[X_i : i \in \sigma]$. In other words, the scalar multiplication action of $R$ on $S₁[X_i : i \in \sigma]$ is central.

MvPolynomial.algebra instance

[CommSemiring R] [CommSemiring S₁] [Algebra R S₁] : Algebra R (MvPolynomial σ S₁)

Full source

instance algebra [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] :
    Algebra R (MvPolynomial σ S₁) :=
  AddMonoidAlgebra.algebra

$R$-Algebra Structure on Multivariate Polynomials

Informal description

For any commutative semiring $R$ and $S₁$, and any algebra structure $R \to S₁$, the multivariate polynomial ring $S₁[X_i : i \in \sigma]$ is an $R$-algebra.

MvPolynomial.isScalarTower_right instance

 [CommSemiring S₁] [DistribSMul R S₁] [IsScalarTower R S₁ S₁] : IsScalarTower R (MvPolynomial σ S₁) (MvPolynomial σ S₁)

Full source

instance isScalarTower_right [CommSemiring S₁] [DistribSMul R S₁] [IsScalarTower R S₁ S₁] :
    IsScalarTower R (MvPolynomial σ S₁) (MvPolynomial σ S₁) :=
  AddMonoidAlgebra.isScalarTower_self _

Scalar Tower Property for Multivariate Polynomials

Informal description

For any commutative semiring $S₁$ and any type $\sigma$, if $R$ is equipped with a scalar multiplication structure on $S₁$ that forms a scalar tower (i.e., $(r \cdot s) \cdot p = r \cdot (s \cdot p)$ for $r \in R$, $s \in S₁$, $p \in S₁$), then the multivariate polynomial ring $S₁[X_i : i \in \sigma]$ also forms a scalar tower with respect to the same scalar multiplication.

MvPolynomial.smulCommClass_right instance

 [CommSemiring S₁] [DistribSMul R S₁] [SMulCommClass R S₁ S₁] : SMulCommClass R (MvPolynomial σ S₁) (MvPolynomial σ S₁)

Full source

instance smulCommClass_right [CommSemiring S₁] [DistribSMul R S₁] [SMulCommClass R S₁ S₁] :
    SMulCommClass R (MvPolynomial σ S₁) (MvPolynomial σ S₁) :=
  AddMonoidAlgebra.smulCommClass_self _

Commutativity of Scalar Multiplication in Multivariate Polynomial Rings

Informal description

For any commutative semiring $S₁$, type $\sigma$, and scalar multiplication structure $R$ on $S₁$ where the scalar multiplications by $R$ and $S₁$ commute on $S₁$, the scalar multiplications by $R$ and $S₁$ also commute on the multivariate polynomial ring $S₁[X_i : i \in \sigma]$. That is, for any $r \in R$, $s \in S₁$, and polynomial $p \in S₁[X_i : i \in \sigma]$, we have $r \cdot (s \cdot p) = s \cdot (r \cdot p)$.

MvPolynomial.unique instance

[CommSemiring R] [Subsingleton R] : Unique (MvPolynomial σ R)

Full source

/-- If `R` is a subsingleton, then `MvPolynomial σ R` has a unique element -/
instance unique [CommSemiring R] [Subsingleton R] : Unique (MvPolynomial σ R) :=
  AddMonoidAlgebra.unique

Uniqueness of Multivariate Polynomials over Subsingleton Coefficient Ring

Informal description

If $R$ is a commutative semiring with at most one element (i.e., $R$ is a subsingleton), then the multivariate polynomial ring $R[X_i : i \in \sigma]$ has exactly one element.

MvPolynomial.monomial definition

(s : σ →₀ ℕ) : R →ₗ[R] MvPolynomial σ R

Full source

/-- `monomial s a` is the monomial with coefficient `a` and exponents given by `s` -/
def monomial (s : σ →₀ ℕ) : R →ₗ[R] MvPolynomial σ R :=
  AddMonoidAlgebra.lsingle s

Monomial in multivariate polynomial ring

Informal description

For a commutative semiring $R$ and a type $\sigma$, the function `monomial s` maps a coefficient $a \in R$ to the monomial $a X^s$ in the multivariate polynomial ring $R[X_i : i \in \sigma]$, where $s : \sigma \to \mathbb{N}$ is a finitely supported function representing the exponents of the variables in the monomial. This function is linear in the coefficient $a$.

MvPolynomial.one_def theorem

: (1 : MvPolynomial σ R) = monomial 0 1

Full source

theorem one_def : (1 : MvPolynomial σ R) = monomial 0 1 := rfl

Identity in Multivariate Polynomial Ring: $1 = 1 \cdot X^0$

Informal description

The multiplicative identity in the multivariate polynomial ring $R[X_i : i \in \sigma]$ is given by the monomial with coefficient $1$ and the zero exponent vector (i.e., $1 = 1 \cdot X^0$).

MvPolynomial.single_eq_monomial theorem

(s : σ →₀ ℕ) (a : R) : Finsupp.single s a = monomial s a

Full source

theorem single_eq_monomial (s : σ →₀ ℕ) (a : R) : Finsupp.single s a = monomial s a :=
  rfl

Equality of Single Function and Monomial in Multivariate Polynomial Ring

Informal description

For any finitely supported function $s : \sigma \to \mathbb{N}$ representing exponents and any coefficient $a \in R$, the finitely supported function `Finsupp.single s a` is equal to the monomial $a X^s$ in the multivariate polynomial ring $R[X_i : i \in \sigma]$.

MvPolynomial.mul_def theorem

: p * q = p.sum fun m a => q.sum fun n b => monomial (m + n) (a * b)

Full source

theorem mul_def : p * q = p.sum fun m a => q.sum fun n b => monomial (m + n) (a * b) :=
  AddMonoidAlgebra.mul_def

Multiplication Formula for Multivariate Polynomials

Informal description

For any two multivariate polynomials $p$ and $q$ in $R[X_i : i \in \sigma]$, their product $p * q$ is given by the double sum: \[ p * q = \sum_{m} \sum_{n} a_m b_n X^{m + n} \] where $a_m$ is the coefficient of the monomial $X^m$ in $p$, $b_n$ is the coefficient of the monomial $X^n$ in $q$, and $X^{m + n}$ denotes the monomial with exponents given by the pointwise sum of $m$ and $n$.

MvPolynomial.C definition

: R →+* MvPolynomial σ R

Full source

/-- `C a` is the constant polynomial with value `a` -/
def C : R →+* MvPolynomial σ R :=
  { singleZeroRingHom with toFun := monomial 0 }

Constant polynomial embedding

Informal description

The function `C` maps a coefficient $a \in R$ to the constant polynomial $a$ in the multivariate polynomial ring $R[X_i : i \in \sigma]$. This is a ring homomorphism from $R$ to $R[X_i : i \in \sigma]$.

MvPolynomial.algebraMap_eq theorem

: algebraMap R (MvPolynomial σ R) = C

Full source

@[simp]
theorem algebraMap_eq : algebraMap R (MvPolynomial σ R) = C :=
  rfl

Algebra Map Equals Constant Embedding in Multivariate Polynomial Ring

Informal description

The algebra map from a commutative semiring $R$ to the multivariate polynomial ring $R[X_i : i \in \sigma]$ is equal to the constant polynomial embedding $C$.

MvPolynomial.X definition

(n : σ) : MvPolynomial σ R

Full source

/-- `X n` is the degree `1` monomial $X_n$. -/
def X (n : σ) : MvPolynomial σ R :=
  monomial (Finsupp.single n 1) 1

Degree one monomial $X_n$ in multivariate polynomial ring

Informal description

For a given variable index $n \in \sigma$, the function `X n` represents the degree 1 monomial $X_n$ in the multivariate polynomial ring $R[X_i : i \in \sigma]$.

MvPolynomial.monomial_left_injective theorem

{r : R} (hr : r ≠ 0) : Function.Injective fun s : σ →₀ ℕ => monomial s r

Full source

theorem monomial_left_injective {r : R} (hr : r ≠ 0) :
    Function.Injective fun s : σ →₀ ℕ => monomial s r :=
  Finsupp.single_left_injective hr

Injectivity of Monomial Construction with Fixed Nonzero Coefficient

Informal description

For any nonzero coefficient $r$ in a commutative semiring $R$, the function $s \mapsto r X^s$ from finitely supported exponent vectors to multivariate polynomials is injective. That is, if $r X^{s_1} = r X^{s_2}$ for some $s_1, s_2 : \sigma \to \mathbb{N}$, then $s_1 = s_2$.

MvPolynomial.monomial_left_inj theorem

{s t : σ →₀ ℕ} {r : R} (hr : r ≠ 0) : monomial s r = monomial t r ↔ s = t

Full source

@[simp]
theorem monomial_left_inj {s t : σ →₀ ℕ} {r : R} (hr : r ≠ 0) :
    monomialmonomial s r = monomial t r ↔ s = t :=
  Finsupp.single_left_inj hr

Monomial Equality Criterion: $r X^s = r X^t \leftrightarrow s = t$ for $r \neq 0$

Informal description

For any nonzero coefficient $r \in R$ and any exponent functions $s, t : \sigma \to \mathbb{N}$, the monomials $r X^s$ and $r X^t$ in the multivariate polynomial ring $R[X_i : i \in \sigma]$ are equal if and only if $s = t$.

MvPolynomial.C_apply theorem

: (C a : MvPolynomial σ R) = monomial 0 a

Full source

theorem C_apply : (C a : MvPolynomial σ R) = monomial 0 a :=
  rfl

Constant Polynomial as Monomial: $C(a) = a X^0$

Informal description

For any coefficient $a$ in a commutative semiring $R$, the constant polynomial $C(a)$ in the multivariate polynomial ring $R[X_i : i \in \sigma]$ is equal to the monomial $a X^0$, where $0$ denotes the zero function in $\sigma \to \mathbb{N}$.

MvPolynomial.C_0 theorem

: C 0 = (0 : MvPolynomial σ R)

Full source

@[simp]
theorem C_0 : C 0 = (0 : MvPolynomial σ R) := map_zero _

Constant Polynomial Embedding Preserves Zero: $C(0) = 0$

Informal description

The constant polynomial embedding $C$ maps the zero element of $R$ to the zero polynomial in the multivariate polynomial ring $R[X_i : i \in \sigma]$, i.e., $C(0) = 0$.

MvPolynomial.C_1 theorem

: C 1 = (1 : MvPolynomial σ R)

Full source

@[simp]
theorem C_1 : C 1 = (1 : MvPolynomial σ R) :=
  rfl

Constant Embedding Preserves Multiplicative Identity

Informal description

The constant polynomial embedding $C$ maps the multiplicative identity $1 \in R$ to the multiplicative identity $1$ in the multivariate polynomial ring $R[X_i : i \in \sigma]$, i.e., $C(1) = 1$.

MvPolynomial.C_mul_monomial theorem

: C a * monomial s a' = monomial s (a * a')

Full source

theorem C_mul_monomial : C a * monomial s a' = monomial s (a * a') := by
  -- Porting note: this `show` feels like defeq abuse, but I can't find the appropriate lemmas
  show AddMonoidAlgebra.single _ _ * AddMonoidAlgebra.single _ _ = AddMonoidAlgebra.single _ _
  simp [C_apply, single_mul_single]

Multiplication of Constant Polynomial with Monomial: $C(a) \cdot (a' X^s) = (a \cdot a') X^s$

Informal description

For any coefficient $a \in R$ and monomial exponent $s : \sigma \to \mathbb{N}$, the product of the constant polynomial $C(a)$ and the monomial $X^s$ with coefficient $a'$ in the multivariate polynomial ring $R[X_i : i \in \sigma]$ is equal to the monomial $X^s$ with coefficient $a \cdot a'$, i.e., $$ C(a) \cdot (a' X^s) = (a \cdot a') X^s. $$

MvPolynomial.C_add theorem

: (C (a + a') : MvPolynomial σ R) = C a + C a'

Full source

@[simp]
theorem C_add : (C (a + a') : MvPolynomial σ R) = C a + C a' :=
  Finsupp.single_add _ _ _

Additivity of Constant Polynomial Embedding

Informal description

For any coefficients $a, a'$ in a commutative semiring $R$, the constant polynomial embedding $C$ satisfies: \[ C(a + a') = C(a) + C(a') \] in the multivariate polynomial ring $R[X_i : i \in \sigma]$.

MvPolynomial.C_mul theorem

: (C (a * a') : MvPolynomial σ R) = C a * C a'

Full source

@[simp]
theorem C_mul : (C (a * a') : MvPolynomial σ R) = C a * C a' :=
  C_mul_monomial.symm

Multiplicativity of Constant Polynomial Embedding: $C(a \cdot a') = C(a) \cdot C(a')$

Informal description

For any coefficients $a, a'$ in a commutative semiring $R$, the constant polynomial embedding $C$ satisfies: \[ C(a \cdot a') = C(a) \cdot C(a') \] in the multivariate polynomial ring $R[X_i : i \in \sigma]$.

MvPolynomial.C_pow theorem

(a : R) (n : ℕ) : (C (a ^ n) : MvPolynomial σ R) = C a ^ n

Full source

@[simp]
theorem C_pow (a : R) (n : ℕ) : (C (a ^ n) : MvPolynomial σ R) = C a ^ n :=
  map_pow _ _ _

Power Preservation under Constant Polynomial Embedding: $C(a^n) = C(a)^n$

Informal description

For any commutative semiring $R$ and any type $\sigma$, the constant polynomial embedding $C : R \to R[X_i : i \in \sigma]$ preserves powers. Specifically, for any element $a \in R$ and natural number $n$, we have $C(a^n) = (C(a))^n$ in the multivariate polynomial ring $R[X_i : i \in \sigma]$.

MvPolynomial.C_injective theorem

(σ : Type*) (R : Type*) [CommSemiring R] : Function.Injective (C : R → MvPolynomial σ R)

Full source

theorem C_injective (σ : Type*) (R : Type*) [CommSemiring R] :
    Function.Injective (C : R → MvPolynomial σ R) :=
  Finsupp.single_injective _

Injectivity of Constant Polynomial Embedding in Multivariate Polynomial Ring

Informal description

For any commutative semiring $R$ and any type $\sigma$, the constant polynomial embedding $C : R \to R[X_i : i \in \sigma]$ is injective. That is, for any $a, b \in R$, if $C(a) = C(b)$ as polynomials, then $a = b$.

MvPolynomial.C_surjective theorem

{R : Type*} [CommSemiring R] (σ : Type*) [IsEmpty σ] : Function.Surjective (C : R → MvPolynomial σ R)

Full source

theorem C_surjective {R : Type*} [CommSemiring R] (σ : Type*) [IsEmpty σ] :
    Function.Surjective (C : R → MvPolynomial σ R) := by
  refine fun p => ⟨p.toFun 0, Finsupp.ext fun a => ?_⟩
  simp only [C_apply, ← single_eq_monomial, (Finsupp.ext isEmptyElim (α := σ) : a = 0),
    single_eq_same]
  rfl

Surjectivity of Constant Embedding in Multivariate Polynomial Ring over Empty Variables

Informal description

For any commutative semiring $R$ and any empty type $\sigma$, the constant polynomial embedding $C \colon R \to R[X_i : i \in \sigma]$ is surjective. In other words, every polynomial in $R[X_i : i \in \sigma]$ is a constant polynomial when $\sigma$ is empty.

MvPolynomial.C_inj theorem

{σ : Type*} (R : Type*) [CommSemiring R] (r s : R) : (C r : MvPolynomial σ R) = C s ↔ r = s

Full source

@[simp]
theorem C_inj {σ : Type*} (R : Type*) [CommSemiring R] (r s : R) :
    (C r : MvPolynomial σ R) = C s ↔ r = s :=
  (C_injective σ R).eq_iff

Equality of Constant Polynomials in Multivariate Polynomial Ring

Informal description

For any commutative semiring $R$ and any type $\sigma$, the constant polynomials $C(r)$ and $C(s)$ in the multivariate polynomial ring $R[X_i : i \in \sigma]$ are equal if and only if the coefficients $r$ and $s$ in $R$ are equal. That is, $C(r) = C(s) \leftrightarrow r = s$.

MvPolynomial.C_eq_zero theorem

: (C a : MvPolynomial σ R) = 0 ↔ a = 0

Full source

@[simp] lemma C_eq_zero : (C a : MvPolynomial σ R) = 0 ↔ a = 0 := by rw [← map_zero C, C_inj]

Zero Constant Polynomial Equals Zero Coefficient

Informal description

For any element $a$ in a commutative semiring $R$ and any type $\sigma$, the constant polynomial $C(a)$ in the multivariate polynomial ring $R[X_i : i \in \sigma]$ is equal to the zero polynomial if and only if $a$ is equal to zero in $R$. That is, $C(a) = 0 \leftrightarrow a = 0$.

MvPolynomial.C_ne_zero theorem

: (C a : MvPolynomial σ R) ≠ 0 ↔ a ≠ 0

Full source

lemma C_ne_zero : (C a : MvPolynomial σ R) ≠ 0(C a : MvPolynomial σ R) ≠ 0 ↔ a ≠ 0 :=
  C_eq_zero.ne

Nonzero Constant Polynomial Equals Nonzero Coefficient

Informal description

For any element $a$ in a commutative semiring $R$ and any type $\sigma$, the constant polynomial $C(a)$ in the multivariate polynomial ring $R[X_i : i \in \sigma]$ is nonzero if and only if $a$ is nonzero in $R$. That is, $C(a) \neq 0 \leftrightarrow a \neq 0$.

MvPolynomial.nontrivial_of_nontrivial instance

(σ : Type*) (R : Type*) [CommSemiring R] [Nontrivial R] : Nontrivial (MvPolynomial σ R)

Full source

instance nontrivial_of_nontrivial (σ : Type*) (R : Type*) [CommSemiring R] [Nontrivial R] :
    Nontrivial (MvPolynomial σ R) :=
  inferInstanceAs (Nontrivial <| AddMonoidAlgebra R (σ →₀ ℕ))

Nontriviality of Multivariate Polynomial Rings over Nontrivial Semirings

Informal description

For any commutative semiring $R$ and any type $\sigma$, if $R$ is nontrivial (i.e., contains at least two distinct elements), then the multivariate polynomial ring $R[X_i : i \in \sigma]$ is also nontrivial.

MvPolynomial.infinite_of_infinite instance

(σ : Type*) (R : Type*) [CommSemiring R] [Infinite R] : Infinite (MvPolynomial σ R)

Full source

instance infinite_of_infinite (σ : Type*) (R : Type*) [CommSemiring R] [Infinite R] :
    Infinite (MvPolynomial σ R) :=
  Infinite.of_injective C (C_injective _ _)

Infinite Coefficient Semiring Yields Infinite Multivariate Polynomial Ring

Informal description

For any commutative semiring $R$ and any type $\sigma$, if $R$ is infinite, then the multivariate polynomial ring $R[X_i : i \in \sigma]$ is also infinite.

MvPolynomial.infinite_of_nonempty instance

(σ : Type*) (R : Type*) [Nonempty σ] [CommSemiring R] [Nontrivial R] : Infinite (MvPolynomial σ R)

Full source

instance infinite_of_nonempty (σ : Type*) (R : Type*) [Nonempty σ] [CommSemiring R]
    [Nontrivial R] : Infinite (MvPolynomial σ R) :=
  Infinite.of_injective ((fun s : σ →₀ ℕ => monomial s 1) ∘ Finsupp.single (Classical.arbitrary σ))
    <| (monomial_left_injective one_ne_zero).comp (Finsupp.single_injective _)

Infinite Multivariate Polynomial Ring over Nonempty Variables and Nontrivial Semiring

Informal description

For any nonempty type $\sigma$ and any nontrivial commutative semiring $R$, the multivariate polynomial ring $R[X_i : i \in \sigma]$ is infinite.

MvPolynomial.C_eq_coe_nat theorem

(n : ℕ) : (C ↑n : MvPolynomial σ R) = n

Full source

theorem C_eq_coe_nat (n : ℕ) : (C ↑n : MvPolynomial σ R) = n := by
  induction n <;> simp [*]

Constant Polynomial Embedding Preserves Natural Numbers: $C(n) = n$

Informal description

For any natural number $n$, the constant polynomial embedding $C$ maps the canonical image of $n$ in $R$ to the same natural number $n$ in the multivariate polynomial ring $R[X_i : i \in \sigma]$, i.e., $C(n) = n$.

MvPolynomial.C_mul' theorem

: MvPolynomial.C a * p = a • p

Full source

theorem C_mul' : MvPolynomial.C a * p = a • p :=
  (Algebra.smul_def a p).symm

Constant Polynomial Multiplication as Scalar Multiplication: $C(a) \cdot p = a \cdot p$

Informal description

For any coefficient $a$ in a commutative semiring $R$ and any multivariate polynomial $p$ in $R[X_i : i \in \sigma]$, the product of the constant polynomial $a$ and $p$ is equal to the scalar multiplication of $a$ on $p$, i.e., $C(a) \cdot p = a \cdot p$.

MvPolynomial.smul_eq_C_mul theorem

(p : MvPolynomial σ R) (a : R) : a • p = C a * p

Full source

theorem smul_eq_C_mul (p : MvPolynomial σ R) (a : R) : a • p = C a * p :=
  C_mul'.symm

Scalar Multiplication as Constant Polynomial Multiplication: $a \cdot p = C(a) \cdot p$

Informal description

For any multivariate polynomial $p$ in $R[X_i : i \in \sigma]$ and any coefficient $a \in R$, the scalar multiplication $a \cdot p$ is equal to the product of the constant polynomial $C(a)$ and $p$, i.e., $a \cdot p = C(a) \cdot p$.

MvPolynomial.C_eq_smul_one theorem

: (C a : MvPolynomial σ R) = a • (1 : MvPolynomial σ R)

Full source

theorem C_eq_smul_one : (C a : MvPolynomial σ R) = a • (1 : MvPolynomial σ R) := by
  rw [← C_mul', mul_one]

Constant Polynomial as Scalar Multiple of Identity: $C(a) = a \cdot 1$

Informal description

For any coefficient $a$ in a commutative semiring $R$, the constant polynomial $C(a)$ in the multivariate polynomial ring $R[X_i : i \in \sigma]$ is equal to the scalar multiplication of $a$ on the multiplicative identity polynomial $1$, i.e., $C(a) = a \cdot 1$.

MvPolynomial.smul_monomial theorem

{S₁ : Type*} [SMulZeroClass S₁ R] (r : S₁) : r • monomial s a = monomial s (r • a)

Full source

theorem smul_monomial {S₁ : Type*} [SMulZeroClass S₁ R] (r : S₁) :
    r • monomial s a = monomial s (r • a) :=
  Finsupp.smul_single _ _ _

Scalar Multiplication of Monomial: $r \cdot (a X^s) = (r \cdot a) X^s$

Informal description

Let $R$ be a commutative semiring, $\sigma$ a type, and $S₁$ a type with a scalar multiplication action on $R$ that preserves zero. For any scalar $r \in S₁$, any monomial exponent function $s : \sigma \to \mathbb{N}$ with finite support, and any coefficient $a \in R$, the scalar multiple $r \cdot (a X^s)$ is equal to the monomial $(r \cdot a) X^s$. In mathematical notation: $$r \cdot (a X^s) = (r \cdot a) X^s.$$

MvPolynomial.X_injective theorem

[Nontrivial R] : Function.Injective (X : σ → MvPolynomial σ R)

Full source

theorem X_injective [Nontrivial R] : Function.Injective (X : σ → MvPolynomial σ R) :=
  (monomial_left_injective one_ne_zero).comp (Finsupp.single_left_injective one_ne_zero)

Injectivity of Variable Embedding in Multivariate Polynomial Ring: $X_m = X_n \Rightarrow m = n$

Informal description

For a nontrivial commutative semiring $R$ and any type $\sigma$, the function $X \colon \sigma \to R[X_i : i \in \sigma]$ that maps each variable index $n \in \sigma$ to the degree one monomial $X_n$ is injective. In other words, if $X_m = X_n$ in the multivariate polynomial ring, then $m = n$.

MvPolynomial.X_inj theorem

[Nontrivial R] (m n : σ) : X m = (X n : MvPolynomial σ R) ↔ m = n

Full source

@[simp]
theorem X_inj [Nontrivial R] (m n : σ) : XX m = (X n : MvPolynomial σ R) ↔ m = n :=
  X_injective.eq_iff

Injectivity of Variable Monomials: $X_m = X_n \iff m = n$

Informal description

For a nontrivial commutative semiring $R$ and any type $\sigma$, the degree one monomials $X_m$ and $X_n$ in the multivariate polynomial ring $R[X_i : i \in \sigma]$ are equal if and only if $m = n$.

MvPolynomial.monomial_pow theorem

: monomial s a ^ e = monomial (e • s) (a ^ e)

Full source

theorem monomial_pow : monomial s a ^ e = monomial (e • s) (a ^ e) :=
  AddMonoidAlgebra.single_pow e

Power of Monomial in Multivariate Polynomial Ring: $(a X^s)^e = a^e X^{e \cdot s}$

Informal description

For any finitely supported function $s : \sigma \to \mathbb{N}$ representing exponents, any coefficient $a \in R$ in a commutative semiring $R$, and any natural number exponent $e \in \mathbb{N}$, the $e$-th power of the monomial $a X^s$ in the multivariate polynomial ring $R[X_i : i \in \sigma]$ is equal to the monomial $a^e X^{e \cdot s}$, where $e \cdot s$ denotes the pointwise scalar multiplication of $s$ by $e$. In symbols: $$(a X^s)^e = a^e X^{e \cdot s}$$

MvPolynomial.monomial_mul theorem

{s s' : σ →₀ ℕ} {a b : R} : monomial s a * monomial s' b = monomial (s + s') (a * b)

Full source

@[simp]
theorem monomial_mul {s s' : σ →₀ ℕ} {a b : R} :
    monomial s a * monomial s' b = monomial (s + s') (a * b) :=
  AddMonoidAlgebra.single_mul_single

Multiplication of Monomials in Multivariate Polynomial Ring: $(a X^s)(b X^{s'}) = (a b) X^{s + s'}$

Informal description

For any finitely supported functions $s, s' \colon \sigma \to \mathbb{N}$ and any coefficients $a, b \in R$, the product of the monomials $a X^s$ and $b X^{s'}$ in the multivariate polynomial ring $R[X_i : i \in \sigma]$ is equal to the monomial $(a b) X^{s + s'}$.

MvPolynomial.monomialOneHom definition

: Multiplicative (σ →₀ ℕ) →* MvPolynomial σ R

Full source

/-- `fun s ↦ monomial s 1` as a homomorphism. -/
def monomialOneHom : MultiplicativeMultiplicative (σ →₀ ℕ) →* MvPolynomial σ R :=
  AddMonoidAlgebra.of _ _

Monomial to polynomial homomorphism

Informal description

The monoid homomorphism that maps a monomial $s$ (represented as a finitely supported function $\sigma \to \mathbb{N}$ in the multiplicative monoid) to the monomial term $X^s$ in the multivariate polynomial ring $R[X_i : i \in \sigma]$. More precisely, this is the function that takes a monomial $s$ and returns the polynomial $\text{monomial}\,s\,1$, which is the monomial $X^s$ with coefficient $1$.

MvPolynomial.monomialOneHom_apply theorem

: monomialOneHom R σ s = (monomial s 1 : MvPolynomial σ R)

Full source

@[simp]
theorem monomialOneHom_apply : monomialOneHom R σ s = (monomial s 1 : MvPolynomial σ R) :=
  rfl

Monomial Homomorphism Maps to $X^s$

Informal description

For any commutative semiring $R$ and any type $\sigma$, the monoid homomorphism `monomialOneHom` maps a monomial $s$ (represented as a finitely supported function $\sigma \to \mathbb{N}$) to the monomial $X^s$ in the multivariate polynomial ring $R[X_i : i \in \sigma]$. Specifically, $\text{monomialOneHom}\, s = \text{monomial}\, s\, 1$.

MvPolynomial.X_pow_eq_monomial theorem

: X n ^ e = monomial (Finsupp.single n e) (1 : R)

Full source

theorem X_pow_eq_monomial : X n ^ e = monomial (Finsupp.single n e) (1 : R) := by
  simp [X, monomial_pow]

Power of Variable Monomial: $X_n^e = \text{monomial}\, (\text{single}\, n\, e)\, 1$

Informal description

For any commutative semiring $R$, any type $\sigma$, any variable $n \in \sigma$, and any natural number exponent $e \in \mathbb{N}$, the $e$-th power of the degree one monomial $X_n$ in the multivariate polynomial ring $R[X_i : i \in \sigma]$ is equal to the monomial with coefficient $1$ and exponent vector given by the finitely supported function that maps $n$ to $e$ and all other variables to $0$. In symbols: $$X_n^e = \text{monomial}\, (\text{single}\, n\, e)\, 1$$ where $\text{single}\, n\, e$ denotes the function that is $e$ at $n$ and $0$ elsewhere.

MvPolynomial.monomial_add_single theorem

: monomial (s + Finsupp.single n e) a = monomial s a * X n ^ e

Full source

theorem monomial_add_single : monomial (s + Finsupp.single n e) a = monomial s a * X n ^ e := by
  rw [X_pow_eq_monomial, monomial_mul, mul_one]

Monomial Decomposition: $\text{monomial}\, (s + \text{single}\, n\, e)\, a = (\text{monomial}\, s\, a) \cdot X_n^e$

Informal description

For any commutative semiring $R$, any type $\sigma$, any finitely supported function $s \colon \sigma \to \mathbb{N}$, any variable $n \in \sigma$, any exponent $e \in \mathbb{N}$, and any coefficient $a \in R$, the monomial with exponent vector $s + \text{single}\, n\, e$ and coefficient $a$ is equal to the product of the monomial with exponent vector $s$ and coefficient $a$ and the $e$-th power of the degree one monomial $X_n$. In symbols: $$\text{monomial}\, (s + \text{single}\, n\, e)\, a = (\text{monomial}\, s\, a) \cdot X_n^e$$ where $\text{single}\, n\, e$ denotes the function that is $e$ at $n$ and $0$ elsewhere.

MvPolynomial.monomial_single_add theorem

: monomial (Finsupp.single n e + s) a = X n ^ e * monomial s a

Full source

theorem monomial_single_add : monomial (Finsupp.single n e + s) a = X n ^ e * monomial s a := by
  rw [X_pow_eq_monomial, monomial_mul, one_mul]

Monomial Decomposition: $\text{monomial}\, (\text{single}\, n\, e + s)\, a = X_n^e \cdot \text{monomial}\, s\, a$

Informal description

For any commutative semiring $R$, any type $\sigma$, any variable $n \in \sigma$, any natural number $e \in \mathbb{N}$, any finitely supported function $s \colon \sigma \to \mathbb{N}$, and any coefficient $a \in R$, the monomial with exponent vector $\text{single}\, n\, e + s$ and coefficient $a$ is equal to the product of the monomial $X_n^e$ and the monomial with exponent vector $s$ and coefficient $a$. In symbols: $$\text{monomial}\, (\text{single}\, n\, e + s)\, a = X_n^e \cdot \text{monomial}\, s\, a$$ where $\text{single}\, n\, e$ denotes the function that is $e$ at $n$ and $0$ elsewhere.

MvPolynomial.C_mul_X_pow_eq_monomial theorem

{s : σ} {a : R} {n : ℕ} : C a * X s ^ n = monomial (Finsupp.single s n) a

Full source

theorem C_mul_X_pow_eq_monomial {s : σ} {a : R} {n : ℕ} :
    C a * X s ^ n = monomial (Finsupp.single s n) a := by
  rw [← zero_add (Finsupp.single s n), monomial_add_single, C_apply]

Monomial Decomposition: $C(a) \cdot X_s^n = a X_s^n$

Informal description

For any commutative semiring $R$, any variable $s \in \sigma$, any coefficient $a \in R$, and any natural number $n \in \mathbb{N}$, the product of the constant polynomial $C(a)$ and the $n$-th power of the degree one monomial $X_s$ is equal to the monomial with exponent vector $\text{single}\, s\, n$ (which is $n$ at $s$ and $0$ elsewhere) and coefficient $a$. In symbols: $$C(a) \cdot X_s^n = \text{monomial}\, (\text{single}\, s\, n)\, a$$

MvPolynomial.C_mul_X_eq_monomial theorem

{s : σ} {a : R} : C a * X s = monomial (Finsupp.single s 1) a

Full source

theorem C_mul_X_eq_monomial {s : σ} {a : R} : C a * X s = monomial (Finsupp.single s 1) a := by
  rw [← C_mul_X_pow_eq_monomial, pow_one]

Monomial Decomposition: $C(a) \cdot X_s = a X_s$

Informal description

For any commutative semiring $R$, any variable $s \in \sigma$, and any coefficient $a \in R$, the product of the constant polynomial $C(a)$ and the degree one monomial $X_s$ is equal to the monomial with exponent vector $\text{single}\, s\, 1$ (which is $1$ at $s$ and $0$ elsewhere) and coefficient $a$. In symbols: $$C(a) \cdot X_s = \text{monomial}\, (\text{single}\, s\, 1)\, a$$

MvPolynomial.monomial_zero theorem

{s : σ →₀ ℕ} : monomial s (0 : R) = 0

Full source

@[simp]
theorem monomial_zero {s : σ →₀ ℕ} : monomial s (0 : R) = 0 :=
  Finsupp.single_zero _

Zero Coefficient Yields Zero Monomial in Multivariate Polynomials

Informal description

For any finitely supported function $s : \sigma \to \mathbb{N}$ representing exponents of variables, the monomial with coefficient $0$ in the multivariate polynomial ring $R[X_i : i \in \sigma]$ is equal to the zero polynomial, i.e., $\text{monomial}_s(0) = 0$.

MvPolynomial.monomial_zero' theorem

: (monomial (0 : σ →₀ ℕ) : R → MvPolynomial σ R) = C

Full source

@[simp]
theorem monomial_zero' : (monomial (0 : σ →₀ ℕ) : R → MvPolynomial σ R) = C :=
  rfl

Monomial with Zero Exponents Equals Constant Embedding

Informal description

The monomial with zero exponents (i.e., the constant term) in the multivariate polynomial ring $R[X_i : i \in \sigma]$ is equal to the constant polynomial embedding $C : R \to R[X_i : i \in \sigma]$. In other words, for any coefficient $a \in R$, we have $\text{monomial}_0(a) = C(a)$.

MvPolynomial.monomial_eq_zero theorem

{s : σ →₀ ℕ} {b : R} : monomial s b = 0 ↔ b = 0

Full source

@[simp]
theorem monomial_eq_zero {s : σ →₀ ℕ} {b : R} : monomialmonomial s b = 0 ↔ b = 0 :=
  Finsupp.single_eq_zero

Zero Monomial Condition: $b X^s = 0 \leftrightarrow b = 0$

Informal description

For any finitely supported function $s : \sigma \to \mathbb{N}$ and any coefficient $b$ in a commutative semiring $R$, the monomial $b X^s$ in the multivariate polynomial ring $R[X_i : i \in \sigma]$ is equal to the zero polynomial if and only if $b = 0$. In mathematical notation: $$b X^s = 0 \leftrightarrow b = 0$$

MvPolynomial.sum_monomial_eq theorem

 {A : Type*} [AddCommMonoid A] {u : σ →₀ ℕ} {r : R} {b : (σ →₀ ℕ) → R → A} (w : b u 0 = 0) :
  sum (monomial u r) b = b u r

Full source

@[simp]
theorem sum_monomial_eq {A : Type*} [AddCommMonoid A] {u : σ →₀ ℕ} {r : R} {b : (σ →₀ ℕ) → R → A}
    (w : b u 0 = 0) : sum (monomial u r) b = b u r :=
  Finsupp.sum_single_index w

Sum of Monomial Equals Evaluation at Coefficient

Informal description

Let $A$ be an additive commutative monoid, $u : \sigma \to \mathbb{N}$ a finitely supported function representing exponents, $r \in R$ a coefficient, and $b : (\sigma \to \mathbb{N}) \to R \to A$ a function such that $b(u, 0) = 0$. Then the sum of the monomial $rX^u$ evaluated with $b$ equals $b(u, r)$.

MvPolynomial.sum_C theorem

{A : Type*} [AddCommMonoid A] {b : (σ →₀ ℕ) → R → A} (w : b 0 0 = 0) : sum (C a) b = b 0 a

Full source

@[simp]
theorem sum_C {A : Type*} [AddCommMonoid A] {b : (σ →₀ ℕ) → R → A} (w : b 0 0 = 0) :
    sum (C a) b = b 0 a :=
  sum_monomial_eq w

Sum of Constant Polynomial Equals Evaluation at Zero Exponent

Informal description

Let $A$ be an additive commutative monoid, $b \colon (\sigma \to \mathbb{N}) \to R \to A$ a function such that $b(0, 0) = 0$, and $a \in R$ a coefficient. Then the sum of the constant polynomial $a$ evaluated with $b$ equals $b(0, a)$. In symbols: $$\sum (C a) b = b(0, a)$$

MvPolynomial.monomial_sum_one theorem

 {α : Type*} (s : Finset α) (f : α → σ →₀ ℕ) :
  (monomial (∑ i ∈ s, f i) 1 : MvPolynomial σ R) = ∏ i ∈ s, monomial (f i) 1

Full source

theorem monomial_sum_one {α : Type*} (s : Finset α) (f : α → σ →₀ ℕ) :
    (monomial (∑ i ∈ s, f i) 1 : MvPolynomial σ R) = ∏ i ∈ s, monomial (f i) 1 :=
  map_prod (monomialOneHom R σ) (fun i => Multiplicative.ofAdd (f i)) s

Monomial Sum-to-Product Identity for Multivariate Polynomials

Informal description

Let $\alpha$ be a type, $s$ be a finite subset of $\alpha$ (represented as a `Finset`), and $f \colon \alpha \to \sigma \to \mathbb{N}$ be a function assigning to each element of $\alpha$ a monomial exponent vector. Then the monomial with exponent vector $\sum_{i \in s} f(i)$ and coefficient $1$ in the multivariate polynomial ring $R[X_i : i \in \sigma]$ is equal to the product over $i \in s$ of the monomials with exponent vectors $f(i)$ and coefficient $1$. In symbols: $$ \text{monomial}\left(\sum_{i \in s} f(i), 1\right) = \prod_{i \in s} \text{monomial}(f(i), 1). $$

MvPolynomial.monomial_sum_index theorem

 {α : Type*} (s : Finset α) (f : α → σ →₀ ℕ) (a : R) : monomial (∑ i ∈ s, f i) a = C a * ∏ i ∈ s, monomial (f i) 1

Full source

theorem monomial_sum_index {α : Type*} (s : Finset α) (f : α → σ →₀ ℕ) (a : R) :
    monomial (∑ i ∈ s, f i) a = C a * ∏ i ∈ s, monomial (f i) 1 := by
  rw [← monomial_sum_one, C_mul', ← (monomial _).map_smul, smul_eq_mul, mul_one]

Monomial Sum-to-Product Identity with Coefficient in Multivariate Polynomials

Informal description

Let $\alpha$ be a type, $s$ be a finite subset of $\alpha$, $f \colon \alpha \to \sigma \to \mathbb{N}$ be a function assigning to each element of $\alpha$ a monomial exponent vector, and $a \in R$ be a coefficient. Then the monomial with exponent vector $\sum_{i \in s} f(i)$ and coefficient $a$ in the multivariate polynomial ring $R[X_i : i \in \sigma]$ is equal to the product of the constant polynomial $a$ and the product over $i \in s$ of the monomials with exponent vectors $f(i)$ and coefficient $1$. In symbols: $$ \text{monomial}\left(\sum_{i \in s} f(i), a\right) = C(a) \cdot \prod_{i \in s} \text{monomial}(f(i), 1). $$

MvPolynomial.monomial_finsupp_sum_index theorem

 {α β : Type*} [Zero β] (f : α →₀ β) (g : α → β → σ →₀ ℕ) (a : R) :
  monomial (f.sum g) a = C a * f.prod fun a b => monomial (g a b) 1

Full source

theorem monomial_finsupp_sum_index {α β : Type*} [Zero β] (f : α →₀ β) (g : α → β → σ →₀ ℕ)
    (a : R) : monomial (f.sum g) a = C a * f.prod fun a b => monomial (g a b) 1 :=
  monomial_sum_index _ _ _

Monomial Sum-to-Product Identity for Finitely Supported Functions in Multivariate Polynomials

Informal description

Let $\alpha$ and $\beta$ be types with $\beta$ having a zero element. Given a finitely supported function $f \colon \alpha \to \beta$, a function $g \colon \alpha \to \beta \to \sigma \to \mathbb{N}$ assigning monomial exponents, and a coefficient $a \in R$, the monomial with exponent vector $\sum_{x \in \alpha} f(x) \cdot g(x, \cdot)$ and coefficient $a$ in the multivariate polynomial ring $R[X_i : i \in \sigma]$ is equal to the product of the constant polynomial $a$ and the product over the support of $f$ of the monomials with exponent vectors $g(x, f(x))$ and coefficient $1$. In symbols: $$ \text{monomial}\left(\sum_{x \in \alpha} f(x) \cdot g(x, \cdot), a\right) = C(a) \cdot \prod_{x \in \text{supp}(f)} \text{monomial}(g(x, f(x)), 1). $$

MvPolynomial.monomial_eq_monomial_iff theorem

 {α : Type*} (a₁ a₂ : α →₀ ℕ) (b₁ b₂ : R) : monomial a₁ b₁ = monomial a₂ b₂ ↔ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0

Full source

theorem monomial_eq_monomial_iff {α : Type*} (a₁ a₂ : α →₀ ℕ) (b₁ b₂ : R) :
    monomialmonomial a₁ b₁ = monomial a₂ b₂ ↔ a₁ = a₂ ∧ b₁ = b₂ ∨ b₁ = 0 ∧ b₂ = 0 :=
  Finsupp.single_eq_single_iff _ _ _ _

Equality Criterion for Monomials in Multivariate Polynomial Ring

Informal description

For any finitely supported functions $a_1, a_2 : \alpha \to \mathbb{N}$ and any coefficients $b_1, b_2 \in R$, the monomials $b_1 X^{a_1}$ and $b_2 X^{a_2}$ in the multivariate polynomial ring $R[X_i : i \in \alpha]$ are equal if and only if either: 1. $a_1 = a_2$ and $b_1 = b_2$, or 2. $b_1 = 0$ and $b_2 = 0$.

MvPolynomial.monomial_eq theorem

: monomial s a = C a * (s.prod fun n e => X n ^ e : MvPolynomial σ R)

Full source

theorem monomial_eq : monomial s a = C a * (s.prod fun n e => X n ^ e : MvPolynomial σ R) := by
  simp only [X_pow_eq_monomial, ← monomial_finsupp_sum_index, Finsupp.sum_single]

Monomial Decomposition: $a X^s = a \cdot \prod_n X_n^{s(n)}$

Informal description

For any commutative semiring $R$, any type $\sigma$, any finitely supported function $s : \sigma \to \mathbb{N}$, and any coefficient $a \in R$, the monomial $a X^s$ in the multivariate polynomial ring $R[X_i : i \in \sigma]$ can be expressed as the product of the constant polynomial $a$ and the product of the variables $X_n$ raised to their respective exponents $s(n)$. In symbols: $$a X^s = a \cdot \prod_{n \in \sigma} X_n^{s(n)}$$ where the product is taken over the support of $s$.

MvPolynomial.prod_X_pow_eq_monomial theorem

: ∏ x ∈ s.support, X x ^ s x = monomial s (1 : R)

Full source

@[simp]
lemma prod_X_pow_eq_monomial : ∏ x ∈ s.support, X x ^ s x = monomial s (1 : R) := by
  simp only [monomial_eq, map_one, one_mul, Finsupp.prod]

Product of Variables as Monomial: $\prod_x X_x^{s(x)} = X^s$

Informal description

For any finitely supported function $s : \sigma \to \mathbb{N}$ (representing exponents of variables), the product of the variables $X_x$ raised to their respective exponents $s(x)$ over the support of $s$ equals the monomial $1 \cdot X^s$ in the multivariate polynomial ring $R[X_i : i \in \sigma]$. In symbols: $$\prod_{x \in \text{supp}(s)} X_x^{s(x)} = 1 \cdot X^s$$ where $\text{supp}(s)$ denotes the support of $s$ (the finite set where $s(x) \neq 0$).

MvPolynomial.induction_on_monomial theorem

 {motive : MvPolynomial σ R → Prop} (C : ∀ a, motive (C a)) (mul_X : ∀ p n, motive p → motive (p * X n)) :
  ∀ s a, motive (monomial s a)

Full source

@[elab_as_elim]
theorem induction_on_monomial {motive : MvPolynomial σ R → Prop}
    (C : ∀ a, motive (C a))
    (mul_X : ∀ p n, motive p → motive (p * X n)) : ∀ s a, motive (monomial s a) := by
  intro s a
  apply @Finsupp.induction σ ℕ _ _ s
  · show motive (monomial 0 a)
    exact C a
  · intro n e p _hpn _he ih
    have : ∀ e : ℕ, motive (monomial p a * X n ^ e) := by
      intro e
      induction e with
      | zero => simp [ih]
      | succ e e_ih => simp [ih, pow_succ, (mul_assoc _ _ _).symm, mul_X, e_ih]
    simp [add_comm, monomial_add_single, this]

Induction Principle for Monomials in Multivariate Polynomials via Constants and Variable Multiplication

Informal description

Let $R$ be a commutative semiring and $\sigma$ an arbitrary type. Given a property $\text{motive}$ of multivariate polynomials in $R[X_i : i \in \sigma]$, to prove that $\text{motive}(a X^s)$ holds for all monomials $a X^s$ (where $s : \sigma \to \mathbb{N}$ is finitely supported and $a \in R$), it suffices to: 1. Show that $\text{motive}(a)$ holds for all constant polynomials $a \in R$. 2. For any polynomial $p$ and variable $n \in \sigma$, if $\text{motive}(p)$ holds, then $\text{motive}(p \cdot X_n)$ also holds.

MvPolynomial.induction_on' theorem

 {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

Full source

/-- 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. -/
@[elab_as_elim]
theorem induction_on' {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 :=
  Finsupp.induction p
    (suffices P (MvPolynomial.monomial 0 0) by rwa [monomial_zero] at this
    show P (MvPolynomial.monomial 0 0) from monomial 0 0)
    fun _ _ _ _ha _hb hPf => add _ _ (monomial _ _) hPf

Induction Principle for Multivariate Polynomials via Monomials and Addition

Informal description

Let $P$ be a property of multivariate polynomials in $R[X_i : i \in \sigma]$. To prove that $P(p)$ holds for all $p \in R[X_i : i \in \sigma]$, it suffices to: 1. Show that $P$ holds for all monomials, i.e., for any finitely supported function $u : \sigma \to \mathbb{N}$ and any coefficient $a \in R$, the property $P(a X^u)$ holds. 2. Show that $P$ is closed under addition, i.e., for any polynomials $p, q \in R[X_i : i \in \sigma]$, if $P(p)$ and $P(q)$ hold, then $P(p + q)$ also holds.

MvPolynomial.monomial_add_induction_on theorem

 {motive : MvPolynomial σ R → Prop} (p : MvPolynomial σ R) (C : ∀ a, 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

Full source

/--
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.
-/
@[elab_as_elim]
theorem monomial_add_induction_on {motive : MvPolynomial σ R → Prop} (p : MvPolynomial σ R)
    (C : ∀ a, 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 :=
  Finsupp.induction p (C_0.rec <| C 0) monomial_add

Induction Principle for Multivariate Polynomials via Monomial Addition

Informal description

Let $R$ be a commutative semiring and $\sigma$ an arbitrary type. Given a property $\text{motive}$ of multivariate polynomials in $R[X_i : i \in \sigma]$, to prove that $\text{motive}(p)$ holds for all $p \in R[X_i : i \in \sigma]$, it suffices to: 1. Show that $\text{motive}(C(a))$ holds for all constant polynomials $a \in R$. 2. For any monomial $a X^s$ (where $s : \sigma \to \mathbb{N}$ is finitely supported and $a \neq 0$) and polynomial $f$ such that $s \notin \text{support}(f)$, if $\text{motive}(f)$ holds, then $\text{motive}(a X^s + f)$ also holds.

MvPolynomial.induction_on'' theorem

 {motive : MvPolynomial σ R → Prop} (p : MvPolynomial σ R) (C : ∀ a, 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 * MvPolynomial.X n)) : motive p

Full source

/--
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 induction_on'' {motive : MvPolynomial σ R → Prop} (p : MvPolynomial σ R)
    (C : ∀ a, 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 * MvPolynomial.X n)) :
    motive p :=
  monomial_add_induction_on p C fun a b f ha hb hf =>
    monomial_add a b f ha hb hf <| induction_on_monomial C mul_X a b

Induction Principle for Multivariate Polynomials via Constants, Monomial Addition, and Variable Multiplication

Informal description

Let $R$ be a commutative semiring and $\sigma$ an arbitrary type. Given a property $\text{motive}$ of multivariate polynomials in $R[X_i : i \in \sigma]$, to prove that $\text{motive}(p)$ holds for all $p \in R[X_i : i \in \sigma]$, it suffices to: 1. Show that $\text{motive}(C(a))$ holds for all constant polynomials $a \in R$. 2. For any monomial $a X^s$ (where $s : \sigma \to \mathbb{N}$ is finitely supported and $a \neq 0$) and polynomial $f$ such that $s \notin \text{support}(f)$, if $\text{motive}(f)$ and $\text{motive}(a X^s)$ hold, then $\text{motive}(a X^s + f)$ also holds. 3. For any polynomial $p$ and variable $n \in \sigma$, if $\text{motive}(p)$ holds, then $\text{motive}(p \cdot X_n)$ also holds.

MvPolynomial.induction_on theorem

 {motive : MvPolynomial σ R → Prop} (p : MvPolynomial σ R) (C : ∀ a, motive (C a))
  (add : ∀ p q, motive p → motive q → motive (p + q)) (mul_X : ∀ p n, motive p → motive (p * X n)) : motive p

Full source

/--
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.
-/
@[recursor 5]
theorem induction_on {motive : MvPolynomial σ R → Prop} (p : MvPolynomial σ R)
    (C : ∀ a, motive (C a))
    (add : ∀ p q, motive p → motive q → motive (p + q))
    (mul_X : ∀ p n, motive p → motive (p * X n)) : motive p :=
  induction_on'' p C (fun a b f _ha _hb hf hm => add (monomial a b) f hm hf) mul_X

Induction Principle for Multivariate Polynomials via Constants, Addition, and Variable Multiplication

Informal description

Let $R$ be a commutative semiring and $\sigma$ an arbitrary type. Given a property $P$ of multivariate polynomials in $R[X_i : i \in \sigma]$, to prove that $P(p)$ holds for all $p \in R[X_i : i \in \sigma]$, it suffices to: 1. Show that $P(C(a))$ holds for all constant polynomials $a \in R$, 2. For any polynomials $p, q$, if $P(p)$ and $P(q)$ hold, then $P(p + q)$ holds, 3. For any polynomial $p$ and variable $n \in \sigma$, if $P(p)$ holds, then $P(p \cdot X_n)$ holds.

MvPolynomial.ringHom_ext theorem

 {A : Type*} [Semiring A] {f g : MvPolynomial σ R →+* A} (hC : ∀ r, f (C r) = g (C r)) (hX : ∀ i, f (X i) = g (X i)) :
  f = g

Full source

theorem ringHom_ext {A : Type*} [Semiring A] {f g : MvPolynomialMvPolynomial σ R →+* A}
    (hC : ∀ r, f (C r) = g (C r)) (hX : ∀ i, f (X i) = g (X i)) : f = g := by
  refine AddMonoidAlgebra.ringHom_ext' ?_ ?_
  -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): this has high priority, but Lean still chooses `RingHom.ext`, why?
  -- probably because of the type synonym
  · ext x
    exact hC _
  · apply Finsupp.mulHom_ext'; intros x
    -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): `Finsupp.mulHom_ext'` needs to have increased priority
    apply MonoidHom.ext_mnat
    exact hX _

Extensionality of Ring Homomorphisms on Multivariate Polynomials via Constants and Variables

Informal description

Let $A$ be a semiring and let $f, g \colon R[X_i : i \in \sigma] \to A$ be two ring homomorphisms from the multivariate polynomial ring over $R$ to $A$. If $f$ and $g$ agree on all constant polynomials (i.e., $f(C(r)) = g(C(r))$ for all $r \in R$) and on all degree one monomials (i.e., $f(X_i) = g(X_i)$ for all $i \in \sigma$), then $f = g$.

MvPolynomial.ringHom_ext' theorem

 {A : Type*} [Semiring A] {f g : MvPolynomial σ R →+* A} (hC : f.comp C = g.comp C) (hX : ∀ i, f (X i) = g (X i)) :
  f = g

Full source

/-- See note [partially-applied ext lemmas]. -/
@[ext 1100]
theorem ringHom_ext' {A : Type*} [Semiring A] {f g : MvPolynomialMvPolynomial σ R →+* A}
    (hC : f.comp C = g.comp C) (hX : ∀ i, f (X i) = g (X i)) : f = g :=
  ringHom_ext (RingHom.ext_iff.1 hC) hX

Extensionality of Ring Homomorphisms on Multivariate Polynomials via Constant Composition and Variables

Informal description

Let $A$ be a semiring and let $f, g \colon R[X_i : i \in \sigma] \to A$ be two ring homomorphisms from the multivariate polynomial ring over $R$ to $A$. If the compositions of $f$ and $g$ with the constant embedding $C$ are equal (i.e., $f \circ C = g \circ C$) and $f$ and $g$ agree on all degree one monomials (i.e., $f(X_i) = g(X_i)$ for all $i \in \sigma$), then $f = g$.

MvPolynomial.hom_eq_hom theorem

 [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

Full source

theorem hom_eq_hom [Semiring S₂] (f g : MvPolynomialMvPolynomial σ R →+* S₂) (hC : f.comp C = g.comp C)
    (hX : ∀ n : σ, f (X n) = g (X n)) (p : MvPolynomial σ R) : f p = g p :=
  RingHom.congr_fun (ringHom_ext' hC hX) p

Equality of Ring Homomorphisms on Multivariate Polynomials via Constant Composition and Variables

Informal description

Let $S_2$ be a semiring and let $f, g \colon R[X_i : i \in \sigma] \to S_2$ be two ring homomorphisms from the multivariate polynomial ring over $R$ to $S_2$. If the compositions of $f$ and $g$ with the constant embedding $C$ are equal (i.e., $f \circ C = g \circ C$) and $f$ and $g$ agree on all degree one monomials (i.e., $f(X_n) = g(X_n)$ for all $n \in \sigma$), then $f(p) = g(p)$ for any polynomial $p \in R[X_i : i \in \sigma]$.

MvPolynomial.is_id theorem

 (f : MvPolynomial σ R →+* MvPolynomial σ R) (hC : f.comp C = C) (hX : ∀ n : σ, f (X n) = X n) (p : MvPolynomial σ R) :
  f p = p

Full source

theorem is_id (f : MvPolynomialMvPolynomial σ R →+* MvPolynomial σ R) (hC : f.comp C = C)
    (hX : ∀ n : σ, f (X n) = X n) (p : MvPolynomial σ R) : f p = p :=
  hom_eq_hom f (RingHom.id _) hC hX p

Identity Characterization for Ring Endomorphisms of Multivariate Polynomial Rings

Informal description

Let $R$ be a commutative semiring and $\sigma$ an arbitrary type. For any ring homomorphism $f \colon R[X_i : i \in \sigma] \to R[X_i : i \in \sigma]$ such that: 1. The composition $f \circ C$ equals the constant embedding $C$, and 2. $f(X_n) = X_n$ for all $n \in \sigma$, then $f$ is the identity map, i.e., $f(p) = p$ for all $p \in R[X_i : i \in \sigma]$.

MvPolynomial.algHom_ext' theorem

 {A B : Type*} [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

Full source

@[ext 1100]
theorem algHom_ext' {A B : Type*} [CommSemiring A] [CommSemiring B] [Algebra R A] [Algebra R B]
    {f g : MvPolynomialMvPolynomial σ 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 :=
  AlgHom.coe_ringHom_injective (MvPolynomial.ringHom_ext' (congr_arg AlgHom.toRingHom h₁) h₂)

Extensionality of $R$-algebra homomorphisms on multivariate polynomials via composition and generators

Informal description

Let $A$ and $B$ be commutative semirings with $R$-algebra structures, and let $f, g \colon A[X_i : i \in \sigma] \to B$ be two $R$-algebra homomorphisms. If the compositions of $f$ and $g$ with the canonical $R$-algebra homomorphism $A \to A[X_i : i \in \sigma]$ are equal (i.e., $f \circ \iota = g \circ \iota$ where $\iota$ is the canonical map) and $f(X_i) = g(X_i)$ for all $i \in \sigma$, then $f = g$.

MvPolynomial.algHom_ext theorem

 {A : Type*} [Semiring A] [Algebra R A] {f g : MvPolynomial σ R →ₐ[R] A} (hf : ∀ i : σ, f (X i) = g (X i)) : f = g

Full source

@[ext 1200]
theorem algHom_ext {A : Type*} [Semiring A] [Algebra R A] {f g : MvPolynomialMvPolynomial σ R →ₐ[R] A}
    (hf : ∀ i : σ, f (X i) = g (X i)) : f = g :=
  AddMonoidAlgebra.algHom_ext' (mulHom_ext' fun X : σ => MonoidHom.ext_mnat (hf X))

Extensionality of $R$-algebra homomorphisms on multivariate polynomials via generators

Informal description

Let $A$ be a semiring with an $R$-algebra structure, and let $f, g \colon R[X_i : i \in \sigma] \to A$ be two $R$-algebra homomorphisms. If $f(X_i) = g(X_i)$ for all $i \in \sigma$, then $f = g$.

MvPolynomial.algHom_C theorem

{A : Type*} [Semiring A] [Algebra R A] (f : MvPolynomial σ R →ₐ[R] A) (r : R) : f (C r) = algebraMap R A r

Full source

@[simp]
theorem algHom_C {A : Type*} [Semiring A] [Algebra R A] (f : MvPolynomialMvPolynomial σ R →ₐ[R] A) (r : R) :
    f (C r) = algebraMap R A r :=
  f.commutes r

Algebra Homomorphism Preserves Constant Polynomials

Informal description

For any commutative semiring $R$, any type $\sigma$, any semiring $A$ with an $R$-algebra structure, and any $R$-algebra homomorphism $f \colon R[X_i : i \in \sigma] \to A$, the homomorphism $f$ maps the constant polynomial $C(r)$ (for $r \in R$) to the image of $r$ under the canonical algebra map $R \to A$. That is, $f(C(r)) = \text{algebraMap}_R^A(r)$.

MvPolynomial.adjoin_range_X theorem

: Algebra.adjoin R (range (X : σ → MvPolynomial σ R)) = ⊤

Full source

@[simp]
theorem adjoin_range_X : Algebra.adjoin R (range (X : σ → MvPolynomial σ R)) = ⊤ := by
  set S := Algebra.adjoin R (range (X : σ → MvPolynomial σ R))
  refine top_unique fun p hp => ?_; clear hp
  induction p using MvPolynomial.induction_on with
  | C => exact S.algebraMap_mem _
  | add p q hp hq => exact S.add_mem hp hq
  | mul_X p i hp => exact S.mul_mem hp (Algebra.subset_adjoin <| mem_range_self _)

Degree one monomials generate the multivariate polynomial ring

Informal description

The $R$-subalgebra generated by the set $\{X_i \mid i \in \sigma\}$ of degree one monomials in the multivariate polynomial ring $R[X_i : i \in \sigma]$ is equal to the entire ring.

MvPolynomial.linearMap_ext theorem

 {M : Type*} [AddCommMonoid M] [Module R M] {f g : MvPolynomial σ R →ₗ[R] M}
  (h : ∀ s, f ∘ₗ monomial s = g ∘ₗ monomial s) : f = g

Full source

@[ext]
theorem linearMap_ext {M : Type*} [AddCommMonoid M] [Module R M] {f g : MvPolynomialMvPolynomial σ R →ₗ[R] M}
    (h : ∀ s, f ∘ₗ monomial s = g ∘ₗ monomial s) : f = g :=
  Finsupp.lhom_ext' h

Extensionality of Linear Maps on Multivariate Polynomials via Monomials

Informal description

Let $R$ be a commutative semiring, $\sigma$ a type, and $M$ an $R$-module. For any two $R$-linear maps $f, g \colon R[X_i : i \in \sigma] \to M$, if for every monomial $X^s$ (where $s \colon \sigma \to \mathbb{N}$ is finitely supported) the compositions $f \circ \text{monomial}(s)$ and $g \circ \text{monomial}(s)$ are equal as linear maps from $R$ to $M$, then $f = g$.

MvPolynomial.support definition

(p : MvPolynomial σ R) : Finset (σ →₀ ℕ)

Full source

/-- The finite set of all `m : σ →₀ ℕ` such that `X^m` has a non-zero coefficient. -/
def support (p : MvPolynomial σ R) : Finset (σ →₀ ℕ) :=
  Finsupp.support p

Support of a multivariate polynomial

Informal description

For a multivariate polynomial $p \in R[X_i : i \in \sigma]$, the function returns the finite set of monomials (represented as functions $\sigma \to \mathbb{N}$ with finite support) that have non-zero coefficients in $p$.

MvPolynomial.finsupp_support_eq_support theorem

(p : MvPolynomial σ R) : Finsupp.support p = p.support

Full source

theorem finsupp_support_eq_support (p : MvPolynomial σ R) : Finsupp.support p = p.support :=
  rfl

Equality of Supports for Multivariate Polynomials

Informal description

For any multivariate polynomial $p \in R[X_i : i \in \sigma]$, the support of $p$ as a finitely supported function (i.e., the set of monomials with non-zero coefficients) is equal to the support of $p$ as a multivariate polynomial.

MvPolynomial.support_monomial theorem

[h : Decidable (a = 0)] : (monomial s a).support = if a = 0 then ∅ else { s }

Full source

theorem support_monomial [h : Decidable (a = 0)] :
    (monomial s a).support = if a = 0 then ∅ else {s} := by
  rw [← Subsingleton.elim (Classical.decEq R a 0) h]
  rfl

Support of Monomial in Multivariate Polynomial Ring: $\operatorname{supp}(aX^s) = \text{if } a=0 \text{ then } \emptyset \text{ else } \{s\}$

Informal description

Let $R$ be a commutative semiring and $\sigma$ an arbitrary type. For any monomial $aX^s$ in the multivariate polynomial ring $R[X_i : i \in \sigma]$, where $a \in R$ is a coefficient and $s : \sigma \to \mathbb{N}$ is a finitely supported function representing exponents, the support of the monomial is empty if $a = 0$, and is the singleton set $\{s\}$ otherwise. In other words: \[ \operatorname{supp}(aX^s) = \begin{cases} \emptyset & \text{if } a = 0 \\ \{s\} & \text{if } a \neq 0 \end{cases} \]

MvPolynomial.support_monomial_subset theorem

: (monomial s a).support ⊆ { s }

Full source

theorem support_monomial_subset : (monomial s a).support ⊆ {s} :=
  support_single_subset

Support of Monomial is Subset of Singleton

Informal description

For any monomial $a X^s$ in the multivariate polynomial ring $R[X_i : i \in \sigma]$, the support of the monomial (i.e., the set of exponent vectors with non-zero coefficients) is a subset of the singleton set $\{s\}$.

MvPolynomial.support_add theorem

[DecidableEq σ] : (p + q).support ⊆ p.support ∪ q.support

Full source

theorem support_add [DecidableEq σ] : (p + q).support ⊆ p.support ∪ q.support :=
  Finsupp.support_add

Support of Sum of Multivariate Polynomials is Contained in Union of Supports

Informal description

For any multivariate polynomials $p$ and $q$ in $R[X_i : i \in \sigma]$ where $\sigma$ has decidable equality, the support of their sum $p + q$ is contained in the union of their supports, i.e., $\operatorname{supp}(p + q) \subseteq \operatorname{supp}(p) \cup \operatorname{supp}(q)$.

MvPolynomial.support_X theorem

[Nontrivial R] : (X n : MvPolynomial σ R).support = {Finsupp.single n 1}

Full source

theorem support_X [Nontrivial R] : (X n : MvPolynomial σ R).support = {Finsupp.single n 1} := by
  classical rw [X, support_monomial, if_neg]; exact one_ne_zero

Support of Degree One Monomial: $\operatorname{supp}(X_n) = \{\delta_n\}$

Informal description

Let $R$ be a nontrivial commutative semiring and $\sigma$ an arbitrary type. For any variable $n \in \sigma$, the support of the degree one monomial $X_n$ in the multivariate polynomial ring $R[X_i : i \in \sigma]$ is the singleton set containing the finitely supported function that maps $n$ to 1 and all other variables to 0. In other words: \[ \operatorname{supp}(X_n) = \{\delta_n\} \] where $\delta_n$ denotes the function $\sigma \to \mathbb{N}$ defined by $\delta_n(n) = 1$ and $\delta_n(m) = 0$ for all $m \neq n$.

MvPolynomial.support_X_pow theorem

[Nontrivial R] (s : σ) (n : ℕ) : (X s ^ n : MvPolynomial σ R).support = {Finsupp.single s n}

Full source

theorem support_X_pow [Nontrivial R] (s : σ) (n : ℕ) :
    (X s ^ n : MvPolynomial σ R).support = {Finsupp.single s n} := by
  classical
    rw [X_pow_eq_monomial, support_monomial, if_neg (one_ne_zero' R)]

Support of Power of Variable Monomial: $\operatorname{supp}(X_s^n) = \{\delta_{s,n}\}$

Informal description

Let $R$ be a nontrivial commutative semiring and $\sigma$ an arbitrary type. For any variable $s \in \sigma$ and natural number $n \in \mathbb{N}$, the support of the monomial $X_s^n$ in the multivariate polynomial ring $R[X_i : i \in \sigma]$ is the singleton set containing the finitely supported function that maps $s$ to $n$ and all other variables to $0$. In symbols: \[ \operatorname{supp}(X_s^n) = \{\delta_{s,n}\} \] where $\delta_{s,n} : \sigma \to \mathbb{N}$ is defined by $\delta_{s,n}(s) = n$ and $\delta_{s,n}(t) = 0$ for all $t \neq s$.

MvPolynomial.support_zero theorem

: (0 : MvPolynomial σ R).support = ∅

Full source

@[simp]
theorem support_zero : (0 : MvPolynomial σ R).support = ∅ :=
  rfl

Support of the Zero Polynomial is Empty

Informal description

The support of the zero polynomial in the multivariate polynomial ring $R[X_i : i \in \sigma]$ is the empty set, i.e., $\text{support}(0) = \emptyset$.

MvPolynomial.support_smul theorem

{S₁ : Type*} [SMulZeroClass S₁ R] {a : S₁} {f : MvPolynomial σ R} : (a • f).support ⊆ f.support

Full source

theorem support_smul {S₁ : Type*} [SMulZeroClass S₁ R] {a : S₁} {f : MvPolynomial σ R} :
    (a • f).support ⊆ f.support :=
  Finsupp.support_smul

Support of Scalar Multiple in Multivariate Polynomial Ring is Contained in Original Support

Informal description

Let $R$ be a commutative semiring, $\sigma$ a type, and $S₁$ a type with a scalar multiplication action on $R$ that preserves zero. For any scalar $a \in S₁$ and any multivariate polynomial $f \in R[X_i : i \in \sigma]$, the support of the scalar multiple $a \cdot f$ is contained in the support of $f$.

MvPolynomial.support_sum theorem

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

Full source

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

Support of Sum of Multivariate Polynomials is Contained in Union of Supports

Informal description

Let $\sigma$ be a type with decidable equality, $R$ a commutative semiring, and $\alpha$ an arbitrary type. For any finite set $s \subseteq \alpha$ and any function $f : \alpha \to R[X_i : i \in \sigma]$ (where $R[X_i : i \in \sigma]$ denotes the multivariate polynomial ring over $R$ with variables indexed by $\sigma$), the support of the sum $\sum_{x \in s} f(x)$ is contained in the finite union $\bigcup_{x \in s} \text{supp}(f(x))$ of the supports of the individual polynomials $f(x)$.

MvPolynomial.coeff definition

(m : σ →₀ ℕ) (p : MvPolynomial σ R) : R

Full source

/-- The coefficient of the monomial `m` in the multi-variable polynomial `p`. -/
def coeff (m : σ →₀ ℕ) (p : MvPolynomial σ R) : R :=
  @DFunLike.coe ((σ →₀ ℕ) →₀ R) _ _ _ p m

Coefficient of a monomial in a multivariate polynomial

Informal description

For a multivariate polynomial $ p $ with variables indexed by $ \sigma $ and coefficients in a commutative semiring $ R $, and a monomial $ m $ represented as a finitely supported function $ \sigma \to \mathbb{N} $, the function returns the coefficient of $ m $ in $ p $.

MvPolynomial.mem_support_iff theorem

{p : MvPolynomial σ R} {m : σ →₀ ℕ} : m ∈ p.support ↔ p.coeff m ≠ 0

Full source

@[simp]
theorem mem_support_iff {p : MvPolynomial σ R} {m : σ →₀ ℕ} : m ∈ p.supportm ∈ p.support ↔ p.coeff m ≠ 0 := by
  simp [support, coeff]

Support-Coefficient Criterion: $m \in \text{supp}(p) \leftrightarrow c_m \neq 0$

Informal description

For any multivariate polynomial $p \in R[X_i : i \in \sigma]$ and any monomial $m$ (represented as a finitely supported function $\sigma \to \mathbb{N}$), the monomial $m$ belongs to the support of $p$ if and only if the coefficient of $m$ in $p$ is nonzero.

MvPolynomial.not_mem_support_iff theorem

{p : MvPolynomial σ R} {m : σ →₀ ℕ} : m ∉ p.support ↔ p.coeff m = 0

Full source

theorem not_mem_support_iff {p : MvPolynomial σ R} {m : σ →₀ ℕ} : m ∉ p.supportm ∉ p.support ↔ p.coeff m = 0 :=
  by simp

Support-Coefficient Criterion: $m \notin \text{supp}(p) \leftrightarrow c_m = 0$

Informal description

For any multivariate polynomial $p \in R[X_i : i \in \sigma]$ and any monomial $m$ (represented as a finitely supported function $\sigma \to \mathbb{N}$), the monomial $m$ is not in the support of $p$ if and only if the coefficient of $m$ in $p$ is zero.

MvPolynomial.sum_def theorem

 {A} [AddCommMonoid A] {p : MvPolynomial σ R} {b : (σ →₀ ℕ) → R → A} : p.sum b = ∑ m ∈ p.support, b m (p.coeff m)

Full source

theorem sum_def {A} [AddCommMonoid A] {p : MvPolynomial σ R} {b : (σ →₀ ℕ) → R → A} :
    p.sum b = ∑ m ∈ p.support, b m (p.coeff m) := by simp [support, Finsupp.sum, coeff]

Definition of Sum for Multivariate Polynomials via Support and Coefficients

Informal description

Let $R$ be a commutative semiring, $\sigma$ an arbitrary type, and $A$ an additive commutative monoid. For any multivariate polynomial $p \in R[X_i : i \in \sigma]$ and any function $b : (\sigma \to \mathbb{N}) \to R \to A$, the sum of $p$ with respect to $b$ equals the finite sum over all monomials $m$ in the support of $p$ of $b(m, c_m)$, where $c_m$ is the coefficient of $m$ in $p$. In symbols: \[ \sum p = \sum_{m \in \text{supp}(p)} b(m, c_m) \]

MvPolynomial.support_mul theorem

[DecidableEq σ] (p q : MvPolynomial σ R) : (p * q).support ⊆ p.support + q.support

Full source

theorem support_mul [DecidableEq σ] (p q : MvPolynomial σ R) :
    (p * q).support ⊆ p.support + q.support :=
  AddMonoidAlgebra.support_mul p q

Support of Product of Multivariate Polynomials is Contained in Minkowski Sum of Supports

Informal description

Let $\sigma$ be a type with decidable equality and $R$ be a commutative semiring. For any two multivariate polynomials $p, q \in R[X_i : i \in \sigma]$, the support of their product $p \cdot q$ is contained in the Minkowski sum of their supports, i.e., \[ \text{supp}(p \cdot q) \subseteq \text{supp}(p) + \text{supp}(q), \] where $\text{supp}(p) + \text{supp}(q) = \{m + n \mid m \in \text{supp}(p), n \in \text{supp}(q)\}$.

MvPolynomial.ext theorem

(p q : MvPolynomial σ R) : (∀ m, coeff m p = coeff m q) → p = q

Full source

@[ext]
theorem ext (p q : MvPolynomial σ R) : (∀ m, coeff m p = coeff m q) → p = q :=
  Finsupp.ext

Extensionality of Multivariate Polynomials via Coefficients

Informal description

For any two multivariate polynomials $p$ and $q$ in $R[X_i : i \in \sigma]$, if the coefficients of $p$ and $q$ are equal for every monomial $m$, then $p = q$.

MvPolynomial.coeff_add theorem

(m : σ →₀ ℕ) (p q : MvPolynomial σ R) : coeff m (p + q) = coeff m p + coeff m q

Full source

@[simp]
theorem coeff_add (m : σ →₀ ℕ) (p q : MvPolynomial σ R) : coeff m (p + q) = coeff m p + coeff m q :=
  add_apply p q m

Additivity of Coefficients in Multivariate Polynomial Addition

Informal description

For any monomial $m$ (represented as a finitely supported function $\sigma \to \mathbb{N}$) and any two multivariate polynomials $p, q$ in $R[X_i : i \in \sigma]$, the coefficient of $m$ in the sum $p + q$ is equal to the sum of the coefficients of $m$ in $p$ and $q$, i.e., \[ \text{coeff}_m(p + q) = \text{coeff}_m(p) + \text{coeff}_m(q). \]

MvPolynomial.coeff_smul theorem

 {S₁ : Type*} [SMulZeroClass S₁ R] (m : σ →₀ ℕ) (C : S₁) (p : MvPolynomial σ R) : coeff m (C • p) = C • coeff m p

Full source

@[simp]
theorem coeff_smul {S₁ : Type*} [SMulZeroClass S₁ R] (m : σ →₀ ℕ) (C : S₁) (p : MvPolynomial σ R) :
    coeff m (C • p) = C • coeff m p :=
  smul_apply C p m

Scalar Multiplication Commutes with Coefficients in Multivariate Polynomials

Informal description

Let $R$ be a commutative semiring, $\sigma$ an arbitrary type, and $S₁$ a type with a scalar multiplication action on $R$ that preserves zero. For any monomial $m \colon \sigma \to \mathbb{N}$, scalar $C \in S₁$, and multivariate polynomial $p \in R[X_i : i \in \sigma]$, the coefficient of $m$ in the scalar multiple $C \cdot p$ is equal to the scalar multiple of the coefficient of $m$ in $p$, i.e., \[ \text{coeff}_m(C \cdot p) = C \cdot \text{coeff}_m(p). \]

MvPolynomial.coeff_zero theorem

(m : σ →₀ ℕ) : coeff m (0 : MvPolynomial σ R) = 0

Full source

@[simp]
theorem coeff_zero (m : σ →₀ ℕ) : coeff m (0 : MvPolynomial σ R) = 0 :=
  rfl

Coefficient of Monomial in Zero Polynomial is Zero

Informal description

For any monomial $m$ represented as a finitely supported function $\sigma \to \mathbb{N}$, the coefficient of $m$ in the zero polynomial is $0$.

MvPolynomial.coeff_zero_X theorem

(i : σ) : coeff 0 (X i : MvPolynomial σ R) = 0

Full source

@[simp]
theorem coeff_zero_X (i : σ) : coeff 0 (X i : MvPolynomial σ R) = 0 :=
  single_eq_of_ne fun h => by cases Finsupp.single_eq_zero.1 h

Zero Coefficient Property of Linear Monomial $X_i$

Informal description

For any variable index $i$ in $\sigma$, the coefficient of the zero monomial (i.e., the constant term) in the degree one monomial $X_i$ is zero.

MvPolynomial.coeffAddMonoidHom definition

(m : σ →₀ ℕ) : MvPolynomial σ R →+ R

Full source

/-- `MvPolynomial.coeff m` but promoted to an `AddMonoidHom`. -/
@[simps]
def coeffAddMonoidHom (m : σ →₀ ℕ) : MvPolynomialMvPolynomial σ R →+ R where
  toFun := coeff m
  map_zero' := coeff_zero m
  map_add' := coeff_add m

Coefficient extraction as an additive monoid homomorphism

Informal description

For a fixed monomial $ m $ represented as a finitely supported function $ \sigma \to \mathbb{N} $, the function that maps a multivariate polynomial $ p $ in $ R[X_i : i \in \sigma] $ to its coefficient of $ m $ in $ p $ is an additive monoid homomorphism from the additive monoid of multivariate polynomials to the additive monoid of coefficients $ R $. More precisely, this means: 1. The zero polynomial is mapped to $ 0 \in R $. 2. For any two polynomials $ p $ and $ q $, the coefficient of $ m $ in $ p + q $ is the sum of the coefficients of $ m $ in $ p $ and $ q $.

MvPolynomial.lcoeff definition

(m : σ →₀ ℕ) : MvPolynomial σ R →ₗ[R] R

Full source

/-- `MvPolynomial.coeff m` but promoted to a `LinearMap`. -/
@[simps]
def lcoeff (m : σ →₀ ℕ) : MvPolynomialMvPolynomial σ R →ₗ[R] R where
  toFun := coeff m
  map_add' := coeff_add m
  map_smul' := coeff_smul m

Linear coefficient map for multivariate polynomials

Informal description

For a given monomial $m$ (represented as a finitely supported function $\sigma \to \mathbb{N}$), the function $\text{lcoeff}_m$ maps a multivariate polynomial $p \in R[X_i : i \in \sigma]$ to its coefficient of $m$ in $p$, viewed as a linear map over $R$. This linear map satisfies: 1. Additivity: $\text{lcoeff}_m(p + q) = \text{lcoeff}_m(p) + \text{lcoeff}_m(q)$ for any polynomials $p, q$ 2. Linearity: $\text{lcoeff}_m(a \cdot p) = a \cdot \text{lcoeff}_m(p)$ for any scalar $a \in R$ and polynomial $p$

MvPolynomial.coeff_sum theorem

 {X : Type*} (s : Finset X) (f : X → MvPolynomial σ R) (m : σ →₀ ℕ) : coeff m (∑ x ∈ s, f x) = ∑ x ∈ s, coeff m (f x)

Full source

theorem coeff_sum {X : Type*} (s : Finset X) (f : X → MvPolynomial σ R) (m : σ →₀ ℕ) :
    coeff m (∑ x ∈ s, f x) = ∑ x ∈ s, coeff m (f x) :=
  map_sum (@coeffAddMonoidHom R σ _ _) _ s

Linearity of Coefficient Extraction with Respect to Finite Sums in Multivariate Polynomials

Informal description

For any finite set $X$, any function $f \colon X \to R[X_i : i \in \sigma]$ mapping elements of $X$ to multivariate polynomials, and any monomial $m$ represented as a finitely supported function $\sigma \to \mathbb{N}$, the coefficient of $m$ in the sum of polynomials $\sum_{x \in s} f(x)$ is equal to the sum of the coefficients of $m$ in each polynomial $f(x)$ for $x \in s$. In other words, the coefficient extraction function $\text{coeff}_m$ commutes with finite sums: \[ \text{coeff}_m\left(\sum_{x \in s} f(x)\right) = \sum_{x \in s} \text{coeff}_m(f(x)). \]

MvPolynomial.monic_monomial_eq theorem

(m) : monomial m (1 : R) = (m.prod fun n e => X n ^ e : MvPolynomial σ R)

Full source

theorem monic_monomial_eq (m) :
    monomial m (1 : R) = (m.prod fun n e => X n ^ e : MvPolynomial σ R) := by simp [monomial_eq]

Monomial Identity: $1 \cdot X^m = \prod_n X_n^{m(n)}$

Informal description

For any commutative semiring $R$ and any type $\sigma$, given a monomial $m : \sigma \to \mathbb{N}$ (represented as a finitely supported function), the monomial with coefficient $1 \in R$ and exponents $m$ is equal to the product of the variables $X_n$ raised to their respective exponents $m(n)$. In symbols: $$ \text{monomial } m \, 1 = \prod_{n \in \sigma} X_n^{m(n)} $$ where the product is taken over the support of $m$.

MvPolynomial.coeff_monomial theorem

[DecidableEq σ] (m n) (a) : coeff m (monomial n a : MvPolynomial σ R) = if n = m then a else 0

Full source

@[simp]
theorem coeff_monomial [DecidableEq σ] (m n) (a) :
    coeff m (monomial n a : MvPolynomial σ R) = if n = m then a else 0 :=
  Finsupp.single_apply

Coefficient of a Monomial in a Multivariate Polynomial

Informal description

Let $\sigma$ be a type with decidable equality, $R$ a commutative semiring, and $m, n : \sigma \to \mathbb{N}$ finitely supported functions. For any coefficient $a \in R$, the coefficient of the monomial $m$ in the polynomial $\text{monomial } n \, a$ is given by: $$ \text{coeff } m \, (\text{monomial } n \, a) = \begin{cases} a & \text{if } n = m, \\ 0 & \text{otherwise.} \end{cases} $$

MvPolynomial.coeff_C theorem

[DecidableEq σ] (m) (a) : coeff m (C a : MvPolynomial σ R) = if 0 = m then a else 0

Full source

@[simp]
theorem coeff_C [DecidableEq σ] (m) (a) :
    coeff m (C a : MvPolynomial σ R) = if 0 = m then a else 0 :=
  Finsupp.single_apply

Coefficient of Constant Polynomial in Multivariate Polynomial Ring

Informal description

Let $\sigma$ be a type with decidable equality and $R$ a commutative semiring. For any monomial $m : \sigma \to \mathbb{N}$ and any coefficient $a \in R$, the coefficient of $m$ in the constant polynomial $C(a)$ is given by: $$ \text{coeff}_m(C(a)) = \begin{cases} a & \text{if } m = 0, \\ 0 & \text{otherwise.} \end{cases} $$

MvPolynomial.coeff_one theorem

[DecidableEq σ] (m) : coeff m (1 : MvPolynomial σ R) = if 0 = m then 1 else 0

Full source

theorem coeff_one [DecidableEq σ] (m) : coeff m (1 : MvPolynomial σ R) = if 0 = m then 1 else 0 :=
  coeff_C m 1

Coefficient of the Constant One Polynomial in Multivariate Polynomial Ring

Informal description

For any monomial $m : \sigma \to \mathbb{N}$ in a multivariate polynomial ring over a commutative semiring $R$ with decidable equality on $\sigma$, the coefficient of $m$ in the constant polynomial $1$ is given by: $$ \text{coeff}_m(1) = \begin{cases} 1 & \text{if } m = 0, \\ 0 & \text{otherwise.} \end{cases} $$

MvPolynomial.coeff_zero_C theorem

(a) : coeff 0 (C a : MvPolynomial σ R) = a

Full source

@[simp]
theorem coeff_zero_C (a) : coeff 0 (C a : MvPolynomial σ R) = a :=
  single_eq_same

Coefficient of Constant Polynomial at Zero Monomial

Informal description

For any coefficient $a$ in a commutative semiring $R$, the coefficient of the zero monomial in the constant polynomial $C(a)$ is equal to $a$, i.e., $\text{coeff}_0(C(a)) = a$.

MvPolynomial.coeff_zero_one theorem

: coeff 0 (1 : MvPolynomial σ R) = 1

Full source

@[simp]
theorem coeff_zero_one : coeff 0 (1 : MvPolynomial σ R) = 1 :=
  coeff_zero_C 1

Coefficient of One at Zero Monomial in Multivariate Polynomials

Informal description

For any commutative semiring $R$ and any type $\sigma$, the coefficient of the zero monomial in the constant polynomial $1$ is equal to $1$, i.e., $\text{coeff}_0(1) = 1$.

MvPolynomial.coeff_X_pow theorem

 [DecidableEq σ] (i : σ) (m) (k : ℕ) : coeff m (X i ^ k : MvPolynomial σ R) = if Finsupp.single i k = m then 1 else 0

Full source

theorem coeff_X_pow [DecidableEq σ] (i : σ) (m) (k : ℕ) :
    coeff m (X i ^ k : MvPolynomial σ R) = if Finsupp.single i k = m then 1 else 0 := by
  have := coeff_monomial m (Finsupp.single i k) (1 : R)
  rwa [@monomial_eq _ _ (1 : R) (Finsupp.single i k) _, C_1, one_mul, Finsupp.prod_single_index]
    at this
  exact pow_zero _

Coefficient of $X_i^k$ in Multivariate Polynomials: $\text{coeff}_m(X_i^k) = \delta_{m, \text{single } i \, k}$

Informal description

Let $\sigma$ be a type with decidable equality and $R$ be a commutative semiring. For any variable $i \in \sigma$, any monomial $m : \sigma \to \mathbb{N}$, and any natural number $k$, the coefficient of $m$ in the polynomial $(X_i)^k$ is given by: \[ \text{coeff}_m(X_i^k) = \begin{cases} 1 & \text{if } m = \text{single } i \, k, \\ 0 & \text{otherwise.} \end{cases} \] where $\text{single } i \, k$ denotes the monomial where the variable $i$ has exponent $k$ and all other variables have exponent $0$.

MvPolynomial.coeff_X' theorem

[DecidableEq σ] (i : σ) (m) : coeff m (X i : MvPolynomial σ R) = if Finsupp.single i 1 = m then 1 else 0

Full source

theorem coeff_X' [DecidableEq σ] (i : σ) (m) :
    coeff m (X i : MvPolynomial σ R) = if Finsupp.single i 1 = m then 1 else 0 := by
  rw [← coeff_X_pow, pow_one]

Coefficient of $X_i$ in Multivariate Polynomials: $\text{coeff}_m(X_i) = \delta_{m, \text{single } i \, 1}$

Informal description

Let $\sigma$ be a type with decidable equality and $R$ be a commutative semiring. For any variable $i \in \sigma$ and any monomial $m : \sigma \to \mathbb{N}$, the coefficient of $m$ in the polynomial $X_i$ is given by: \[ \text{coeff}_m(X_i) = \begin{cases} 1 & \text{if } m = \text{single } i \, 1, \\ 0 & \text{otherwise.} \end{cases} \] where $\text{single } i \, 1$ denotes the monomial where the variable $i$ has exponent $1$ and all other variables have exponent $0$.

MvPolynomial.coeff_X theorem

(i : σ) : coeff (Finsupp.single i 1) (X i : MvPolynomial σ R) = 1

Full source

@[simp]
theorem coeff_X (i : σ) : coeff (Finsupp.single i 1) (X i : MvPolynomial σ R) = 1 := by
  classical rw [coeff_X', if_pos rfl]

Coefficient of $X_i$ in its own monomial is 1

Informal description

For any variable $i$ in the type $\sigma$, the coefficient of the monomial $\text{single } i \, 1$ (where only the variable $i$ has exponent 1 and all others have exponent 0) in the polynomial $X_i$ is equal to 1.

MvPolynomial.coeff_C_mul theorem

(m) (a : R) (p : MvPolynomial σ R) : coeff m (C a * p) = a * coeff m p

Full source

@[simp]
theorem coeff_C_mul (m) (a : R) (p : MvPolynomial σ R) : coeff m (C a * p) = a * coeff m p := by
  classical
  rw [mul_def, sum_C]
  · simp +contextual [sum_def, coeff_sum]
  simp

Coefficient of Scalar Multiplication in Multivariate Polynomials: $\text{coeff}_m(a \cdot p) = a \cdot \text{coeff}_m(p)$

Informal description

For any monomial $m$ represented as a finitely supported function $\sigma \to \mathbb{N}$, any coefficient $a \in R$, and any multivariate polynomial $p \in R[X_i : i \in \sigma]$, the coefficient of $m$ in the product of the constant polynomial $a$ with $p$ is equal to $a$ multiplied by the coefficient of $m$ in $p$. In symbols: \[ \text{coeff}_m(a \cdot p) = a \cdot \text{coeff}_m(p) \]

MvPolynomial.coeff_mul theorem

 [DecidableEq σ] (p q : MvPolynomial σ R) (n : σ →₀ ℕ) :
  coeff n (p * q) = ∑ x ∈ Finset.antidiagonal n, coeff x.1 p * coeff x.2 q

Full source

theorem coeff_mul [DecidableEq σ] (p q : MvPolynomial σ R) (n : σ →₀ ℕ) :
    coeff n (p * q) = ∑ x ∈ Finset.antidiagonal n, coeff x.1 p * coeff x.2 q :=
  AddMonoidAlgebra.mul_apply_antidiagonal p q _ _ Finset.mem_antidiagonal

Coefficient Formula for Multiplication of Multivariate Polynomials

Informal description

Let $R$ be a commutative semiring and $\sigma$ an arbitrary type. For any two multivariate polynomials $p, q \in R[X_i : i \in \sigma]$ and any monomial $n \colon \sigma \to \mathbb{N}$ (with finite support), the coefficient of $n$ in the product $p \cdot q$ is given by: \[ \text{coeff}_n(p \cdot q) = \sum_{(a,b) \in \text{antidiagonal}(n)} \text{coeff}_a(p) \cdot \text{coeff}_b(q) \] where $\text{antidiagonal}(n)$ denotes all pairs of monomials $(a,b)$ such that $a + b = n$.

MvPolynomial.coeff_mul_monomial theorem

(m) (s : σ →₀ ℕ) (r : R) (p : MvPolynomial σ R) : coeff (m + s) (p * monomial s r) = coeff m p * r

Full source

@[simp]
theorem coeff_mul_monomial (m) (s : σ →₀ ℕ) (r : R) (p : MvPolynomial σ R) :
    coeff (m + s) (p * monomial s r) = coeff m p * r :=
  AddMonoidAlgebra.mul_single_apply_aux p _ _ _ _ fun _a _ => add_left_inj _

Coefficient Formula for Multiplication by a Monomial in Multivariate Polynomials

Informal description

Let $R$ be a commutative semiring and $\sigma$ an arbitrary type. For any multivariate polynomial $p \in R[X_i : i \in \sigma]$, monomial $s \colon \sigma \to \mathbb{N}$ (with finite support), coefficient $r \in R$, and monomial $m \colon \sigma \to \mathbb{N}$, the coefficient of the monomial $m + s$ in the product $p \cdot (r X^s)$ equals the product of the coefficient of $m$ in $p$ and $r$, i.e., \[ \text{coeff}_{m + s}(p \cdot (r X^s)) = (\text{coeff}_m p) \cdot r. \]

MvPolynomial.coeff_monomial_mul theorem

(m) (s : σ →₀ ℕ) (r : R) (p : MvPolynomial σ R) : coeff (s + m) (monomial s r * p) = r * coeff m p

Full source

@[simp]
theorem coeff_monomial_mul (m) (s : σ →₀ ℕ) (r : R) (p : MvPolynomial σ R) :
    coeff (s + m) (monomial s r * p) = r * coeff m p :=
  AddMonoidAlgebra.single_mul_apply_aux p _ _ _ _ fun _a _ => add_right_inj _

Coefficient of Monomial Multiplication in Multivariate Polynomials

Informal description

For any monomial exponent $m$, any finitely supported function $s \colon \sigma \to \mathbb{N}$ representing exponents, any coefficient $r \in R$, and any multivariate polynomial $p \in R[X_i : i \in \sigma]$, the coefficient of the monomial $s + m$ in the product of the monomial $r X^s$ and $p$ is equal to $r$ multiplied by the coefficient of $m$ in $p$. In symbols: \[ \text{coeff}_{s + m}(r X^s \cdot p) = r \cdot \text{coeff}_m(p). \]

MvPolynomial.coeff_mul_X theorem

(m) (s : σ) (p : MvPolynomial σ R) : coeff (m + Finsupp.single s 1) (p * X s) = coeff m p

Full source

@[simp]
theorem coeff_mul_X (m) (s : σ) (p : MvPolynomial σ R) :
    coeff (m + Finsupp.single s 1) (p * X s) = coeff m p :=
  (coeff_mul_monomial _ _ _ _).trans (mul_one _)

Coefficient Preservation in Multiplication by Variable $X_s$ in Multivariate Polynomials

Informal description

For any multivariate polynomial $p$ with variables indexed by $\sigma$ and coefficients in a commutative semiring $R$, any monomial exponent $m \colon \sigma \to \mathbb{N}$, and any variable index $s \in \sigma$, the coefficient of the monomial $m + \delta_s$ in the product $p \cdot X_s$ equals the coefficient of $m$ in $p$, where $\delta_s$ is the monomial with exponent 1 at $s$ and 0 elsewhere. In symbols: \[ \text{coeff}_{m + \delta_s}(p \cdot X_s) = \text{coeff}_m(p). \]

MvPolynomial.coeff_X_mul theorem

(m) (s : σ) (p : MvPolynomial σ R) : coeff (Finsupp.single s 1 + m) (X s * p) = coeff m p

Full source

@[simp]
theorem coeff_X_mul (m) (s : σ) (p : MvPolynomial σ R) :
    coeff (Finsupp.single s 1 + m) (X s * p) = coeff m p :=
  (coeff_monomial_mul _ _ _ _).trans (one_mul _)

Coefficient of $X_s \cdot p$ at $X_s \cdot X^m$ equals coefficient of $p$ at $X^m$

Informal description

For any monomial exponent $m \colon \sigma \to \mathbb{N}$, any variable index $s \in \sigma$, and any multivariate polynomial $p \in R[X_i : i \in \sigma]$, the coefficient of the monomial $X_s \cdot X^m$ (represented as $\text{single}\,s\,1 + m$) in the product $X_s \cdot p$ is equal to the coefficient of $m$ in $p$. In symbols: \[ \text{coeff}_{\text{single}\,s\,1 + m}(X_s \cdot p) = \text{coeff}_m(p). \]

MvPolynomial.coeff_single_X_pow theorem

 [DecidableEq σ] (s s' : σ) (n n' : ℕ) :
  (X (R := R) s ^ n).coeff (Finsupp.single s' n') = if s = s' ∧ n = n' ∨ n = 0 ∧ n' = 0 then 1 else 0

Full source

lemma coeff_single_X_pow [DecidableEq σ] (s s' : σ) (n n' : ℕ) :
    (X (R := R) s ^ n).coeff (Finsupp.single s' n')
    = if s = s' ∧ n = n' ∨ n = 0 ∧ n' = 0 then 1 else 0 := by
  simp only [coeff_X_pow, single_eq_single_iff]

Coefficient of Monomial in Power of Variable: $\text{coeff}_{X_{s'}^{n'}}(X_s^n) = \delta_{s,s'}\delta_{n,n'} + \delta_{n,0}\delta_{n',0}$

Informal description

Let $\sigma$ be a type with decidable equality and $R$ be a commutative semiring. For any variables $s, s' \in \sigma$ and natural numbers $n, n'$, the coefficient of the monomial $X_{s'}^{n'}$ in the polynomial $(X_s)^n$ is given by: \[ \text{coeff}_{X_{s'}^{n'}}(X_s^n) = \begin{cases} 1 & \text{if } (s = s' \text{ and } n = n') \text{ or } (n = 0 \text{ and } n' = 0), \\ 0 & \text{otherwise.} \end{cases} \]

MvPolynomial.coeff_single_X theorem

[DecidableEq σ] (s s' : σ) (n : ℕ) : (X s).coeff (R := R) (Finsupp.single s' n) = if n = 1 ∧ s = s' then 1 else 0

Full source

@[simp]
lemma coeff_single_X [DecidableEq σ] (s s' : σ) (n : ℕ) :
    (X s).coeff (R := R) (Finsupp.single s' n) = if n = 1 ∧ s = s' then 1 else 0 := by
  simpa [eq_comm, and_comm] using coeff_single_X_pow s s' 1 n

Coefficient of Monomial in Variable Polynomial: $\text{coeff}_{X_{s'}^n}(X_s) = \delta_{n,1}\delta_{s,s'}$

Informal description

Let $\sigma$ be a type with decidable equality and $R$ be a commutative semiring. For any variables $s, s' \in \sigma$ and natural number $n$, the coefficient of the monomial $X_{s'}^n$ in the polynomial $X_s$ is given by: \[ \text{coeff}_{X_{s'}^n}(X_s) = \begin{cases} 1 & \text{if } n = 1 \text{ and } s = s', \\ 0 & \text{otherwise.} \end{cases} \]

MvPolynomial.support_mul_X theorem

(s : σ) (p : MvPolynomial σ R) : (p * X s).support = p.support.map (addRightEmbedding (Finsupp.single s 1))

Full source

@[simp]
theorem support_mul_X (s : σ) (p : MvPolynomial σ R) :
    (p * X s).support = p.support.map (addRightEmbedding (Finsupp.single s 1)) :=
  AddMonoidAlgebra.support_mul_single p _ (by simp) _

Support of Product with Variable Monomial in Multivariate Polynomials

Informal description

For any variable $s$ in $\sigma$ and any multivariate polynomial $p$ in $R[X_i : i \in \sigma]$, the support of the product $p \cdot X_s$ is equal to the image of the support of $p$ under the function that adds the monomial $X_s$ (represented as $\text{single } s \text{ } 1$) to each monomial in the support of $p$.

MvPolynomial.support_X_mul theorem

(s : σ) (p : MvPolynomial σ R) : (X s * p).support = p.support.map (addLeftEmbedding (Finsupp.single s 1))

Full source

@[simp]
theorem support_X_mul (s : σ) (p : MvPolynomial σ R) :
    (X s * p).support = p.support.map (addLeftEmbedding (Finsupp.single s 1)) :=
  AddMonoidAlgebra.support_single_mul p _ (by simp) _

Support of $X_s \cdot p$ under Left Multiplication by a Variable

Informal description

For any variable $s$ in $\sigma$ and any multivariate polynomial $p$ in $R[X_i : i \in \sigma]$, the support of the product $X_s \cdot p$ is equal to the image of the support of $p$ under the embedding that adds the monomial $X_s$ (represented as $\text{single } s \text{ } 1$) to each monomial in the support of $p$.

MvPolynomial.support_smul_eq theorem

 {S₁ : Type*} [Semiring S₁] [Module S₁ R] [NoZeroSMulDivisors S₁ R] {a : S₁} (h : a ≠ 0) (p : MvPolynomial σ R) :
  (a • p).support = p.support

Full source

@[simp]
theorem support_smul_eq {S₁ : Type*} [Semiring S₁] [Module S₁ R] [NoZeroSMulDivisors S₁ R] {a : S₁}
    (h : a ≠ 0) (p : MvPolynomial σ R) : (a • p).support = p.support :=
  Finsupp.support_smul_eq h

Support Preservation under Scalar Multiplication in Multivariate Polynomials

Informal description

Let $S₁$ be a semiring and $R$ be a commutative semiring with a module structure over $S₁$, such that $S₁$ has no zero divisors acting on $R$. For any nonzero element $a \in S₁$ and any multivariate polynomial $p \in R[X_i : i \in \sigma]$, the support of the scalar multiple $a \cdot p$ is equal to the support of $p$.

MvPolynomial.support_sdiff_support_subset_support_add theorem

[DecidableEq σ] (p q : MvPolynomial σ R) : p.support \ q.support ⊆ (p + q).support

Full source

theorem support_sdiff_support_subset_support_add [DecidableEq σ] (p q : MvPolynomial σ R) :
    p.support \ q.supportp.support \ q.support ⊆ (p + q).support := by
  intro m hm
  simp only [Classical.not_not, mem_support_iff, Finset.mem_sdiff, Ne] at hm
  simp [hm.2, hm.1]

Support Difference in Sum of Multivariate Polynomials

Informal description

For any multivariate polynomials $p$ and $q$ with variables indexed by a type $\sigma$ and coefficients in a commutative semiring $R$, the set difference of the supports of $p$ and $q$ is contained in the support of their sum $p + q$. In other words, for any monomial $m$ that appears in $p$ but not in $q$, $m$ must appear in $p + q$.

MvPolynomial.support_symmDiff_support_subset_support_add theorem

[DecidableEq σ] (p q : MvPolynomial σ R) : p.support ∆ q.support ⊆ (p + q).support

Full source

theorem support_symmDiff_support_subset_support_add [DecidableEq σ] (p q : MvPolynomial σ R) :
    p.support ∆ q.supportp.support ∆ q.support ⊆ (p + q).support := by
  rw [symmDiff_def, Finset.sup_eq_union]
  apply Finset.union_subset
  · exact support_sdiff_support_subset_support_add p q
  · rw [add_comm]
    exact support_sdiff_support_subset_support_add q p

Symmetric Difference of Supports in Sum of Multivariate Polynomials

Informal description

For any two multivariate polynomials $p$ and $q$ with variables indexed by a type $\sigma$ and coefficients in a commutative semiring $R$, the symmetric difference of their supports is contained in the support of their sum. In other words, if a monomial appears in exactly one of $p$ or $q$, then it must appear in $p + q$.

MvPolynomial.coeff_mul_monomial' theorem

 (m) (s : σ →₀ ℕ) (r : R) (p : MvPolynomial σ R) : coeff m (p * monomial s r) = if s ≤ m then coeff (m - s) p * r else 0

Full source

theorem coeff_mul_monomial' (m) (s : σ →₀ ℕ) (r : R) (p : MvPolynomial σ R) :
    coeff m (p * monomial s r) = if s ≤ m then coeff (m - s) p * r else 0 := by
  classical
  split_ifs with h
  · conv_rhs => rw [← coeff_mul_monomial _ s]
    congr with t
    rw [tsub_add_cancel_of_le h]
  · contrapose! h
    rw [← mem_support_iff] at h
    obtain ⟨j, -, rfl⟩ : ∃ j ∈ support p, j + s = m := by
      simpa [Finset.mem_add]
        using Finset.add_subset_add_left support_monomial_subset <| support_mul _ _ h
    exact le_add_left le_rfl

Coefficient Formula for Multiplication by a Monomial in Multivariate Polynomials (Case Analysis Version)

Informal description

Let $R$ be a commutative semiring and $\sigma$ an arbitrary type. For any multivariate polynomial $p \in R[X_i : i \in \sigma]$, monomial $s \colon \sigma \to \mathbb{N}$ (with finite support), coefficient $r \in R$, and monomial $m \colon \sigma \to \mathbb{N}$, the coefficient of $m$ in the product $p \cdot (r X^s)$ is given by: \[ \text{coeff}_m(p \cdot (r X^s)) = \begin{cases} \text{coeff}_{m-s}(p) \cdot r & \text{if } s \leq m \\ 0 & \text{otherwise} \end{cases} \]

MvPolynomial.coeff_monomial_mul' theorem

 (m) (s : σ →₀ ℕ) (r : R) (p : MvPolynomial σ R) : coeff m (monomial s r * p) = if s ≤ m then r * coeff (m - s) p else 0

Full source

theorem coeff_monomial_mul' (m) (s : σ →₀ ℕ) (r : R) (p : MvPolynomial σ R) :
    coeff m (monomial s r * p) = if s ≤ m then r * coeff (m - s) p else 0 := by
  -- note that if we allow `R` to be non-commutative we will have to duplicate the proof above.
  rw [mul_comm, mul_comm r]
  exact coeff_mul_monomial' _ _ _ _

Coefficient Formula for Left Multiplication by a Monomial in Multivariate Polynomials

Informal description

Let $R$ be a commutative semiring and $\sigma$ an arbitrary type. For any multivariate polynomial $p \in R[X_i : i \in \sigma]$, monomial $s \colon \sigma \to \mathbb{N}$ (with finite support), coefficient $r \in R$, and monomial $m \colon \sigma \to \mathbb{N}$, the coefficient of $m$ in the product $(r X^s) \cdot p$ is given by: \[ \text{coeff}_m((r X^s) \cdot p) = \begin{cases} r \cdot \text{coeff}_{m-s}(p) & \text{if } s \leq m \\ 0 & \text{otherwise} \end{cases} \]

MvPolynomial.coeff_mul_X' theorem

 [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

Full source

theorem coeff_mul_X' [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 := by
  refine (coeff_mul_monomial' _ _ _ _).trans ?_
  simp_rw [Finsupp.single_le_iff, Finsupp.mem_support_iff, Nat.succ_le_iff, pos_iff_ne_zero,
    mul_one]

Coefficient Formula for Right Multiplication by $X_s$ in Multivariate Polynomials

Informal description

Let $R$ be a commutative semiring and $\sigma$ an arbitrary type. For any multivariate polynomial $p \in R[X_i : i \in \sigma]$, variable $s \in \sigma$, and monomial $m \colon \sigma \to \mathbb{N}$ (with finite support), the coefficient of $m$ in the product $p \cdot X_s$ is given by: \[ \text{coeff}_m(p \cdot X_s) = \begin{cases} \text{coeff}_{m - e_s}(p) & \text{if } s \in \text{supp}(m) \\ 0 & \text{otherwise} \end{cases} \] where $e_s \colon \sigma \to \mathbb{N}$ is the indicator function at $s$ (i.e., $e_s(s) = 1$ and $e_s(t) = 0$ for $t \neq s$), and $\text{supp}(m)$ denotes the support of $m$.

MvPolynomial.coeff_X_mul' theorem

 [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

Full source

theorem coeff_X_mul' [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 := by
  refine (coeff_monomial_mul' _ _ _ _).trans ?_
  simp_rw [Finsupp.single_le_iff, Finsupp.mem_support_iff, Nat.succ_le_iff, pos_iff_ne_zero,
    one_mul]

Coefficient Formula for Left Multiplication by $X_s$ in Multivariate Polynomials

Informal description

Let $R$ be a commutative semiring and $\sigma$ an arbitrary type. For any multivariate polynomial $p \in R[X_i : i \in \sigma]$, variable $s \in \sigma$, and monomial $m \colon \sigma \to \mathbb{N}$ (with finite support), the coefficient of $m$ in the product $X_s \cdot p$ is given by: \[ \text{coeff}_m(X_s \cdot p) = \begin{cases} \text{coeff}_{m - e_s}(p) & \text{if } s \in \text{supp}(m) \\ 0 & \text{otherwise} \end{cases} \] where $e_s \colon \sigma \to \mathbb{N}$ is the indicator function at $s$ (i.e., $e_s(s) = 1$ and $e_s(t) = 0$ for $t \neq s$), and $\text{supp}(m)$ denotes the support of $m$.

MvPolynomial.ne_zero_iff theorem

{p : MvPolynomial σ R} : p ≠ 0 ↔ ∃ d, coeff d p ≠ 0

Full source

theorem ne_zero_iff {p : MvPolynomial σ R} : p ≠ 0p ≠ 0 ↔ ∃ d, coeff d p ≠ 0 := by
  rw [Ne, eq_zero_iff]
  push_neg
  rfl

Nonzero Multivariate Polynomial Characterization: $p \neq 0 \leftrightarrow \exists d, \text{coeff } d p \neq 0$

Informal description

A multivariate polynomial $p$ with variables indexed by $\sigma$ and coefficients in a commutative semiring $R$ is nonzero if and only if there exists a monomial $d$ (represented as a finitely supported function $\sigma \to \mathbb{N}$) such that the coefficient of $d$ in $p$ is nonzero.

MvPolynomial.X_ne_zero theorem

[Nontrivial R] (s : σ) : X (R := R) s ≠ 0

Full source

@[simp]
theorem X_ne_zero [Nontrivial R] (s : σ) :
    XX (R := R) s ≠ 0 := by
  rw [ne_zero_iff]
  use Finsupp.single s 1
  simp only [coeff_X, ne_eq, one_ne_zero, not_false_eq_true]

Nonzero Property of Degree One Monomial $X_s$ in Multivariate Polynomial Ring

Informal description

For any nontrivial commutative semiring $R$ and any variable index $s \in \sigma$, the degree one monomial $X_s$ in the multivariate polynomial ring $R[X_i : i \in \sigma]$ is nonzero.

MvPolynomial.support_eq_empty theorem

{p : MvPolynomial σ R} : p.support = ∅ ↔ p = 0

Full source

@[simp]
theorem support_eq_empty {p : MvPolynomial σ R} : p.support = ∅ ↔ p = 0 :=
  Finsupp.support_eq_empty

Empty Support Characterization for Multivariate Polynomials

Informal description

For any multivariate polynomial $p$ with variables indexed by $\sigma$ and coefficients in a commutative semiring $R$, the support of $p$ (the set of monomials with non-zero coefficients) is empty if and only if $p$ is the zero polynomial.

MvPolynomial.support_nonempty theorem

{p : MvPolynomial σ R} : p.support.Nonempty ↔ p ≠ 0

Full source

@[simp]
lemma support_nonempty {p : MvPolynomial σ R} : p.support.Nonempty ↔ p ≠ 0 := by
  rw [Finset.nonempty_iff_ne_empty, ne_eq, support_eq_empty]

Nonempty Support Characterization for Multivariate Polynomials: $\operatorname{supp}(p) \neq \emptyset \iff p \neq 0$

Informal description

For any multivariate polynomial $p$ with variables indexed by $\sigma$ and coefficients in a commutative semiring $R$, the support of $p$ (the set of monomials with non-zero coefficients) is nonempty if and only if $p$ is not the zero polynomial.

MvPolynomial.exists_coeff_ne_zero theorem

{p : MvPolynomial σ R} (h : p ≠ 0) : ∃ d, coeff d p ≠ 0

Full source

theorem exists_coeff_ne_zero {p : MvPolynomial σ R} (h : p ≠ 0) : ∃ d, coeff d p ≠ 0 :=
  ne_zero_iff.mp h

Existence of Nonzero Coefficient in Nonzero Multivariate Polynomial

Informal description

For any nonzero multivariate polynomial $p$ with variables indexed by $\sigma$ and coefficients in a commutative semiring $R$, there exists a monomial $d$ (represented as a finitely supported function $\sigma \to \mathbb{N}$) such that the coefficient of $d$ in $p$ is nonzero.

MvPolynomial.C_dvd_iff_dvd_coeff theorem

(r : R) (φ : MvPolynomial σ R) : C r ∣ φ ↔ ∀ i, r ∣ φ.coeff i

Full source

theorem C_dvd_iff_dvd_coeff (r : R) (φ : MvPolynomial σ R) : CC r ∣ φC r ∣ φ ↔ ∀ i, r ∣ φ.coeff i := by
  constructor
  · rintro ⟨φ, rfl⟩ c
    rw [coeff_C_mul]
    apply dvd_mul_right
  · intro h
    choose C hc using h
    classical
      let c' : (σ →₀ ℕ) → R := fun i => if i ∈ φ.support then C i else 0
      let ψ : MvPolynomial σ R := ∑ i ∈ φ.support, monomial i (c' i)
      use ψ
      apply MvPolynomial.ext
      intro i
      simp only [ψ, c', coeff_C_mul, coeff_sum, coeff_monomial, Finset.sum_ite_eq']
      split_ifs with hi
      · rw [hc]
      · rw [not_mem_support_iff] at hi
        rwa [mul_zero]

Divisibility Criterion for Constant Polynomials in Multivariate Polynomial Ring: $r \mid \varphi \leftrightarrow \forall m, r \mid c_m(\varphi)$

Informal description

For any element $r$ in a commutative semiring $R$ and any multivariate polynomial $\varphi \in R[X_i : i \in \sigma]$, the constant polynomial $r$ divides $\varphi$ if and only if $r$ divides every coefficient of $\varphi$. In symbols: \[ r \mid \varphi \leftrightarrow \forall m, r \mid \text{coeff}_m(\varphi) \]

MvPolynomial.isRegular_X theorem

: IsRegular (X n : MvPolynomial σ R)

Full source

@[simp] lemma isRegular_X : IsRegular (X n : MvPolynomial σ R) := by
  suffices IsLeftRegular (X n : MvPolynomial σ R) from
    ⟨this, this.right_of_commute <| Commute.all _⟩
  intro P Q (hPQ : (X n) * P = (X n) * Q)
  ext i
  rw [← coeff_X_mul i n P, hPQ, coeff_X_mul i n Q]

Regularity of the Monomial $X_n$ in Multivariate Polynomial Ring

Informal description

The degree one monomial $X_n$ in the multivariate polynomial ring $R[X_i : i \in \sigma]$ is a regular element, meaning that for any polynomials $p, q \in R[X_i : i \in \sigma]$, if $X_n \cdot p = X_n \cdot q$, then $p = q$.

MvPolynomial.isRegular_X_pow theorem

(k : ℕ) : IsRegular (X n ^ k : MvPolynomial σ R)

Full source

@[simp] lemma isRegular_X_pow (k : ℕ) : IsRegular (X n ^ k : MvPolynomial σ R) := isRegular_X.pow k

Regularity of Powers of Monomial $X_n$ in Multivariate Polynomial Ring

Informal description

For any natural number $k$, the monomial $X_n^k$ in the multivariate polynomial ring $R[X_i : i \in \sigma]$ is a regular element. That is, for any polynomials $p, q \in R[X_i : i \in \sigma]$, if $X_n^k \cdot p = X_n^k \cdot q$, then $p = q$.

MvPolynomial.isRegular_prod_X theorem

(s : Finset σ) : IsRegular (∏ n ∈ s, X n : MvPolynomial σ R)

Full source

@[simp] lemma isRegular_prod_X (s : Finset σ) :
    IsRegular (∏ n ∈ s, X n : MvPolynomial σ R) :=
  IsRegular.prod fun _ _ ↦ isRegular_X

Regularity of Product of Variables in Multivariate Polynomial Ring

Informal description

For any finite subset $s$ of the variable index set $\sigma$, the product of monomials $\prod_{n \in s} X_n$ in the multivariate polynomial ring $R[X_i : i \in \sigma]$ is a regular element. That is, for any polynomials $p, q \in R[X_i : i \in \sigma]$, if $(\prod_{n \in s} X_n) \cdot p = (\prod_{n \in s} X_n) \cdot q$, then $p = q$.

MvPolynomial.coeffs definition

(p : MvPolynomial σ R) : Finset R

Full source

/-- The finset of nonzero coefficients of a multivariate polynomial. -/
def coeffs (p : MvPolynomial σ R) : Finset R :=
  letI := Classical.decEq R
  Finset.image p.coeff p.support

Nonzero coefficients of a multivariate polynomial

Informal description

For a multivariate polynomial $ p $ with variables indexed by $ \sigma $ and coefficients in a commutative semiring $ R $, the function returns the finite set of all nonzero coefficients appearing in $ p $. This is obtained by taking the image of the support of $ p $ (the set of monomials with nonzero coefficients) under the coefficient function.

MvPolynomial.coeffs_zero theorem

: coeffs (0 : MvPolynomial σ R) = ∅

Full source

@[simp]
lemma coeffs_zero : coeffs (0 : MvPolynomial σ R) = ∅ :=
  rfl

Zero Polynomial Has No Nonzero Coefficients

Informal description

The set of nonzero coefficients of the zero polynomial in the multivariate polynomial ring $R[X_i : i \in \sigma]$ is empty, i.e., $\text{coeffs}(0) = \emptyset$.

MvPolynomial.coeffs_one theorem

: coeffs (1 : MvPolynomial σ R) ⊆ { 1 }

Full source

lemma coeffs_one : coeffscoeffs (1 : MvPolynomial σ R) ⊆ {1} := by
  classical
    rw [coeffs, Finset.image_subset_iff]
    simp_all [coeff_one]

Nonzero Coefficients of the Constant One Polynomial: $\text{coeffs}(1) \subseteq \{1\}$

Informal description

For the constant polynomial $1$ in the multivariate polynomial ring $R[X_i : i \in \sigma]$, the set of its nonzero coefficients is a subset of the singleton set $\{1\}$.

MvPolynomial.coeffs_eq_empty_of_subsingleton theorem

[Subsingleton R] (p : MvPolynomial σ R) : p.coeffs = ∅

Full source

@[nontriviality]
lemma coeffs_eq_empty_of_subsingleton [Subsingleton R] (p : MvPolynomial σ R) : p.coeffs = ∅ := by
  simpa [coeffs] using Subsingleton.eq_zero p

Empty Coefficient Set for Multivariate Polynomials over Subsingleton Rings

Informal description

For any multivariate polynomial $p$ over a commutative semiring $R$ that is a subsingleton (i.e., $R$ has at most one element), the set of nonzero coefficients of $p$ is empty.

MvPolynomial.coeffs_one_of_nontrivial theorem

[Nontrivial R] : coeffs (1 : MvPolynomial σ R) = { 1 }

Full source

@[simp]
lemma coeffs_one_of_nontrivial [Nontrivial R] : coeffs (1 : MvPolynomial σ R) = {1} := by
  apply Finset.Subset.antisymm coeffs_one
  simp only [coeffs, Finset.singleton_subset_iff, Finset.mem_image]
  exact ⟨0, by simp⟩

Nonzero coefficients of constant one polynomial: $\text{coeffs}(1) = \{1\}$ for nontrivial $R$

Informal description

For a nontrivial commutative semiring $R$ and any type $\sigma$, the set of nonzero coefficients of the constant polynomial $1$ in the multivariate polynomial ring $R[X_i : i \in \sigma]$ is exactly the singleton set $\{1\}$.

MvPolynomial.mem_coeffs_iff theorem

{p : MvPolynomial σ R} {c : R} : c ∈ p.coeffs ↔ ∃ n ∈ p.support, c = p.coeff n

Full source

lemma mem_coeffs_iff {p : MvPolynomial σ R} {c : R} :
    c ∈ p.coeffsc ∈ p.coeffs ↔ ∃ n ∈ p.support, c = p.coeff n := by
  simp [coeffs, eq_comm, (Finset.mem_image)]

Characterization of Coefficient Membership in Multivariate Polynomials

Informal description

For a multivariate polynomial $p \in R[X_i : i \in \sigma]$ and a coefficient $c \in R$, the coefficient $c$ appears in the set of nonzero coefficients of $p$ if and only if there exists a monomial $n$ in the support of $p$ such that the coefficient of $n$ in $p$ equals $c$.

MvPolynomial.coeff_mem_coeffs theorem

{p : MvPolynomial σ R} (m : σ →₀ ℕ) (h : p.coeff m ≠ 0) : p.coeff m ∈ p.coeffs

Full source

lemma coeff_mem_coeffs {p : MvPolynomial σ R} (m : σ →₀ ℕ)
    (h : p.coeff m ≠ 0) : p.coeff m ∈ p.coeffs :=
  letI := Classical.decEq R
  Finset.mem_image_of_mem p.coeff (mem_support_iff.mpr h)

Nonzero Coefficients Belong to Coefficient Set

Informal description

For any multivariate polynomial $p \in R[X_i : i \in \sigma]$ and any monomial $m$ (represented as a finitely supported function $\sigma \to \mathbb{N}$), if the coefficient of $m$ in $p$ is nonzero, then this coefficient belongs to the finite set of all nonzero coefficients of $p$.

MvPolynomial.zero_not_mem_coeffs theorem

(p : MvPolynomial σ R) : 0 ∉ p.coeffs

Full source

lemma zero_not_mem_coeffs (p : MvPolynomial σ R) : 0 ∉ p.coeffs := by
  intro hz
  obtain ⟨n, hnsupp, hn⟩ := mem_coeffs_iff.mp hz
  exact (mem_support_iff.mp hnsupp) hn.symm

Nonzero Coefficients Exclude Zero in Multivariate Polynomials

Informal description

For any multivariate polynomial $p \in R[X_i : i \in \sigma]$, the zero coefficient does not appear in the set of nonzero coefficients of $p$.

MvPolynomial.constantCoeff definition

: MvPolynomial σ R →+* R

Full source

/-- `constantCoeff p` returns the constant term of the polynomial `p`, defined as `coeff 0 p`.
This is a ring homomorphism.
-/
def constantCoeff : MvPolynomialMvPolynomial σ R →+* R where
  toFun := coeff 0
  map_one' := by simp [AddMonoidAlgebra.one_def]
  map_mul' := by classical simp [coeff_mul, Finsupp.support_single_ne_zero]
  map_zero' := coeff_zero _
  map_add' := coeff_add _

Constant term of a multivariate polynomial

Informal description

The function `constantCoeff` maps a multivariate polynomial $ p \in R[X_i : i \in \sigma] $ to its constant term, which is the coefficient of the monomial $ 0 $ (the monomial where all variables have exponent zero). This function is a ring homomorphism from the ring of multivariate polynomials to the coefficient ring $ R $.

MvPolynomial.constantCoeff_eq theorem

: (constantCoeff : MvPolynomial σ R → R) = coeff 0

Full source

theorem constantCoeff_eq : (constantCoeff : MvPolynomial σ R → R) = coeff 0 :=
  rfl

Constant Coefficient as Zero-Monomial Coefficient in Multivariate Polynomials

Informal description

The constant coefficient function `constantCoeff` for multivariate polynomials in $R[X_i : i \in \sigma]$ is equal to the coefficient function `coeff` evaluated at the zero monomial (where all exponents are zero). In other words, for any polynomial $p \in R[X_i : i \in \sigma]$, the constant term of $p$ is given by the coefficient of the monomial $0$ in $p$.

MvPolynomial.constantCoeff_C theorem

(r : R) : constantCoeff (C r : MvPolynomial σ R) = r

Full source

@[simp]
theorem constantCoeff_C (r : R) : constantCoeff (C r : MvPolynomial σ R) = r := by
  classical simp [constantCoeff_eq]

Constant Term of Constant Polynomial in Multivariate Polynomial Ring

Informal description

For any coefficient $r$ in a commutative semiring $R$, the constant term of the constant polynomial $C(r)$ in the multivariate polynomial ring $R[X_i : i \in \sigma]$ is equal to $r$.

MvPolynomial.constantCoeff_X theorem

(i : σ) : constantCoeff (X i : MvPolynomial σ R) = 0

Full source

@[simp]
theorem constantCoeff_X (i : σ) : constantCoeff (X i : MvPolynomial σ R) = 0 := by
  simp [constantCoeff_eq]

Vanishing Constant Term Property of Linear Monomial $X_i$

Informal description

For any variable index $i$ in $\sigma$, the constant term (coefficient of the zero monomial) of the degree one monomial $X_i$ in the multivariate polynomial ring $R[X_j : j \in \sigma]$ is zero.

MvPolynomial.constantCoeff_smul theorem

{R : Type*} [SMulZeroClass R S₁] (a : R) (f : MvPolynomial σ S₁) : constantCoeff (a • f) = a • constantCoeff f

Full source

@[simp]
theorem constantCoeff_smul {R : Type*} [SMulZeroClass R S₁] (a : R) (f : MvPolynomial σ S₁) :
    constantCoeff (a • f) = a • constantCoeff f :=
  rfl

Scalar Multiplication Commutes with Constant Term Extraction in Multivariate Polynomials

Informal description

Let $R$ be a type with a scalar multiplication structure that preserves zero, and let $S₁$ be a commutative semiring. For any scalar $a \in R$ and any multivariate polynomial $f \in S₁[X_i : i \in \sigma]$, the constant term of the scalar multiple $a \cdot f$ is equal to the scalar multiple of the constant term of $f$, i.e., $\text{constantCoeff}(a \cdot f) = a \cdot \text{constantCoeff}(f)$.

MvPolynomial.constantCoeff_monomial theorem

[DecidableEq σ] (d : σ →₀ ℕ) (r : R) : constantCoeff (monomial d r) = if d = 0 then r else 0

Full source

theorem constantCoeff_monomial [DecidableEq σ] (d : σ →₀ ℕ) (r : R) :
    constantCoeff (monomial d r) = if d = 0 then r else 0 := by
  rw [constantCoeff_eq, coeff_monomial]

Constant Term of a Monomial in Multivariate Polynomials

Informal description

Let $\sigma$ be a type with decidable equality and $R$ a commutative semiring. For any finitely supported function $d : \sigma \to \mathbb{N}$ (representing exponents of variables) and any coefficient $r \in R$, the constant term of the monomial $r X^d$ is $r$ if $d$ is the zero function (i.e., all exponents are zero), and $0$ otherwise. In other words: $$ \text{constantCoeff}(r X^d) = \begin{cases} r & \text{if } d = 0, \\ 0 & \text{otherwise.} \end{cases} $$

MvPolynomial.constantCoeff_comp_C theorem

: constantCoeff.comp (C : R →+* MvPolynomial σ R) = RingHom.id R

Full source

@[simp]
theorem constantCoeff_comp_C : constantCoeff.comp (C : R →+* MvPolynomial σ R) = RingHom.id R := by
  ext x
  exact constantCoeff_C σ x

Identity Property of Constant Term and Constant Polynomial Embedding

Informal description

The composition of the constant term homomorphism with the constant polynomial embedding $C$ is equal to the identity ring homomorphism on $R$. In other words, for any coefficient $r \in R$, we have $\text{constantCoeff}(C(r)) = r$.

MvPolynomial.constantCoeff_comp_algebraMap theorem

: constantCoeff.comp (algebraMap R (MvPolynomial σ R)) = RingHom.id R

Full source

theorem constantCoeff_comp_algebraMap :
    constantCoeff.comp (algebraMap R (MvPolynomial σ R)) = RingHom.id R :=
  constantCoeff_comp_C _ _

Identity Property of Constant Term and Algebra Map in Multivariate Polynomial Ring

Informal description

The composition of the constant term homomorphism with the algebra map from $R$ to the multivariate polynomial ring $R[X_i : i \in \sigma]$ is equal to the identity ring homomorphism on $R$. In other words, for any element $r \in R$, we have $\text{constantCoeff}(\text{algebraMap}(r)) = r$.

MvPolynomial.support_sum_monomial_coeff theorem

(p : MvPolynomial σ R) : (∑ v ∈ p.support, monomial v (coeff v p)) = p

Full source

@[simp]
theorem support_sum_monomial_coeff (p : MvPolynomial σ R) :
    (∑ v ∈ p.support, monomial v (coeff v p)) = p :=
  Finsupp.sum_single p

Decomposition of Multivariate Polynomial into Monomials

Informal description

For any multivariate polynomial $p \in R[X_i : i \in \sigma]$, the sum of the monomials $X^v$ weighted by their respective coefficients $p_v$ over all monomials $v$ in the support of $p$ equals $p$ itself. In other words, $$ \sum_{v \in \text{supp}(p)} p_v X^v = p. $$

MvPolynomial.as_sum theorem

(p : MvPolynomial σ R) : p = ∑ v ∈ p.support, monomial v (coeff v p)

Full source

theorem as_sum (p : MvPolynomial σ R) : p = ∑ v ∈ p.support, monomial v (coeff v p) :=
  (support_sum_monomial_coeff p).symm

Decomposition of Multivariate Polynomial into Monomial Sum

Informal description

For any multivariate polynomial $p \in R[X_i : i \in \sigma]$, $p$ can be expressed as the sum of its monomials, where each monomial $X^v$ (with $v : \sigma \to \mathbb{N}$ a finitely supported function) is weighted by its corresponding coefficient $p_v$ in $p$, summed over all monomials $v$ in the support of $p$. That is, $$ p = \sum_{v \in \text{supp}(p)} p_v X^v. $$

MvPolynomial.coeffsIn definition

: Submodule R (MvPolynomial σ S)

Full source

/-- The `R`-submodule of multivariate polynomials whose coefficients lie in a `R`-submodule `M`. -/
@[simps]
def coeffsIn : Submodule R (MvPolynomial σ S) where
  carrier := {p | ∀ i, p.coeff i ∈ M}
  add_mem' := by simp+contextual [add_mem]
  zero_mem' := by simp
  smul_mem' := by simp+contextual [Submodule.smul_mem]

Submodule of multivariate polynomials with coefficients in a submodule

Informal description

The $R$-submodule of multivariate polynomials in $S[X_i : i \in \sigma]$ consisting of all polynomials whose coefficients lie in an $R$-submodule $M$ of $S$. Specifically, a polynomial $p$ is in this submodule if for every monomial $i$, the coefficient $p_i$ belongs to $M$.

MvPolynomial.mem_coeffsIn theorem

: p ∈ coeffsIn σ M ↔ ∀ i, p.coeff i ∈ M

Full source

lemma mem_coeffsIn : p ∈ coeffsIn σ Mp ∈ coeffsIn σ M ↔ ∀ i, p.coeff i ∈ M := .rfl

Membership Criterion for Polynomials in Coefficient Submodule

Informal description

A multivariate polynomial $p$ with variables indexed by $\sigma$ and coefficients in a commutative semiring $S$ belongs to the submodule $\text{coeffsIn}_{\sigma} M$ if and only if for every monomial $i$, the coefficient $p_i$ of $p$ at $i$ is an element of the submodule $M$ of $S$.

MvPolynomial.monomial_mem_coeffsIn theorem

: monomial i x ∈ coeffsIn σ M ↔ x ∈ M

Full source

@[simp]
lemma monomial_mem_coeffsIn : monomialmonomial i x ∈ coeffsIn σ Mmonomial i x ∈ coeffsIn σ M ↔ x ∈ M := by
  classical
  simp only [mem_coeffsIn, coeff_monomial]
  exact ⟨fun h ↦ by simpa using h i, fun hs j ↦ by split <;> simp [hs]⟩

Monomial Membership in Coefficient Submodule Criterion

Informal description

For a multivariate polynomial ring $R[X_i : i \in \sigma]$ and a submodule $M$ of $R$, the monomial $x X^i$ belongs to the submodule of polynomials with coefficients in $M$ if and only if the coefficient $x$ is in $M$. In other words: $$ x X^i \in \text{coeffsIn}_{\sigma} M \leftrightarrow x \in M. $$

MvPolynomial.C_mem_coeffsIn theorem

: C x ∈ coeffsIn σ M ↔ x ∈ M

Full source

@[simp]
lemma C_mem_coeffsIn : CC x ∈ coeffsIn σ MC x ∈ coeffsIn σ M ↔ x ∈ M := by simpa using monomial_mem_coeffsIn (i := 0)

Membership Criterion for Constant Polynomials in Coefficient Submodule

Informal description

For a commutative semiring $R$, a type $\sigma$, and an $R$-submodule $M$ of $S$, the constant polynomial $C(x) \in R[X_i : i \in \sigma]$ belongs to the submodule of polynomials with coefficients in $M$ if and only if $x \in M$. In other words: $$ C(x) \in \text{coeffsIn}_{\sigma} M \leftrightarrow x \in M. $$

MvPolynomial.one_coeffsIn theorem

: 1 ∈ coeffsIn σ M ↔ 1 ∈ M

Full source

@[simp]
lemma one_coeffsIn : 1 ∈ coeffsIn σ M1 ∈ coeffsIn σ M ↔ 1 ∈ M := by simpa using C_mem_coeffsIn (x := (1 : S))

Membership of One in Coefficient Submodule Criterion

Informal description

The constant polynomial $1$ belongs to the submodule of multivariate polynomials with coefficients in $M$ if and only if the constant $1$ belongs to $M$. In other words: $$ 1 \in \text{coeffsIn}_{\sigma} M \leftrightarrow 1 \in M. $$

MvPolynomial.mul_monomial_mem_coeffsIn theorem

: p * monomial i 1 ∈ coeffsIn σ M ↔ p ∈ coeffsIn σ M

Full source

@[simp]
lemma mul_monomial_mem_coeffsIn : p * monomial i 1 ∈ coeffsIn σ Mp * monomial i 1 ∈ coeffsIn σ M ↔ p ∈ coeffsIn σ M := by
  classical
  simp only [mem_coeffsIn, coeff_mul_monomial', Finsupp.mem_support_iff]
  constructor
  · rintro hp j
    simpa using hp (j + i)
  · rintro hp i
    split <;> simp [hp]

Membership condition for right multiplication by a monomial in coefficient submodule

Informal description

Let $R$ be a commutative semiring, $\sigma$ a type, and $M$ an $R$-submodule of $S$. For any multivariate polynomial $p \in R[X_i : i \in \sigma]$ and any monomial $\text{monomial}\ i\ 1$ (where $i : \sigma \to \mathbb{N}$ is a finitely supported function), the product $p \cdot \text{monomial}\ i\ 1$ belongs to the submodule $\text{coeffsIn}\ \sigma\ M$ if and only if $p$ belongs to $\text{coeffsIn}\ \sigma\ M$. In other words: \[ p \cdot (1 \cdot X^i) \in \text{coeffsIn}_{\sigma} M \leftrightarrow p \in \text{coeffsIn}_{\sigma} M. \]

MvPolynomial.monomial_mul_mem_coeffsIn theorem

: monomial i 1 * p ∈ coeffsIn σ M ↔ p ∈ coeffsIn σ M

Full source

@[simp]
lemma monomial_mul_mem_coeffsIn : monomialmonomial i 1 * p ∈ coeffsIn σ Mmonomial i 1 * p ∈ coeffsIn σ M ↔ p ∈ coeffsIn σ M := by
  simp [mul_comm]

Membership condition for monomial multiplication in coefficient submodule

Informal description

Let $R$ be a commutative semiring, $\sigma$ a type, and $M$ an $R$-submodule of $S$. For any monomial $\text{monomial}\ i\ 1$ (where $i : \sigma \to₀ ℕ$) and any multivariate polynomial $p \in R[X_i : i \in \sigma]$, the product $\text{monomial}\ i\ 1 \cdot p$ belongs to the submodule $\text{coeffsIn}\ \sigma\ M$ if and only if $p$ belongs to $\text{coeffsIn}\ \sigma\ M$.

MvPolynomial.mul_X_mem_coeffsIn theorem

: p * X s ∈ coeffsIn σ M ↔ p ∈ coeffsIn σ M

Full source

@[simp]
lemma mul_X_mem_coeffsIn : p * X s ∈ coeffsIn σ Mp * X s ∈ coeffsIn σ M ↔ p ∈ coeffsIn σ M := by
  simpa [-mul_monomial_mem_coeffsIn] using mul_monomial_mem_coeffsIn (i := .single s 1)

Membership condition for right multiplication by $X_s$ in coefficient submodule

Informal description

For a multivariate polynomial $p$ in the ring $R[X_i : i \in \sigma]$ and a variable $X_s$ (where $s \in \sigma$), the product $p \cdot X_s$ belongs to the submodule $\text{coeffsIn}_{\sigma} M$ if and only if $p$ belongs to $\text{coeffsIn}_{\sigma} M$. Here, $\text{coeffsIn}_{\sigma} M$ denotes the submodule of polynomials whose coefficients all lie in the submodule $M$ of $R$.

MvPolynomial.X_mul_mem_coeffsIn theorem

: X s * p ∈ coeffsIn σ M ↔ p ∈ coeffsIn σ M

Full source

@[simp]
lemma X_mul_mem_coeffsIn : XX s * p ∈ coeffsIn σ MX s * p ∈ coeffsIn σ M ↔ p ∈ coeffsIn σ M := by simp [mul_comm]

Membership condition for left multiplication by $X_s$ in coefficient submodule

Informal description

For any multivariate polynomial $p$ in the ring $R[X_i : i \in \sigma]$ and any variable $X_s$ (where $s \in \sigma$), the product $X_s \cdot p$ belongs to the submodule $\text{coeffsIn}\ \sigma\ M$ if and only if $p$ belongs to $\text{coeffsIn}\ \sigma\ M$. Here, $\text{coeffsIn}\ \sigma\ M$ is the submodule of polynomials whose coefficients all lie in the submodule $M$ of $R$.

MvPolynomial.coeffsIn_eq_span_monomial theorem

: coeffsIn σ M = .span R ({monomial i m | (m ∈ M) (i : σ →₀ ℕ)})

Full source

lemma coeffsIn_eq_span_monomial : coeffsIn σ M = .span R {monomial i m | (m ∈ M) (i : σ →₀ ℕ)} := by
  classical
  refine le_antisymm ?_ <| Submodule.span_le.2 ?_
  · rintro p hp
    rw [p.as_sum]
    exact sum_mem fun i hi ↦ Submodule.subset_span ⟨_, hp i, _, rfl⟩
  · rintro _ ⟨m, hm, s, n, rfl⟩ i
    simp [coeff_X_pow]
    split <;> simp [hm]

Coefficient Submodule as Span of Monomials

Informal description

The submodule $\text{coeffsIn}\ \sigma\ M$ of multivariate polynomials in $R[X_i : i \in \sigma]$ with coefficients in a submodule $M$ of $R$ is equal to the $R$-linear span of the set of monomials $\{a X^i \mid a \in M, i \in \sigma \to \mathbb{N}\}$.

MvPolynomial.coeffsIn_le theorem

{N : Submodule R (MvPolynomial σ S)} : coeffsIn σ M ≤ N ↔ ∀ m ∈ M, ∀ i, monomial i m ∈ N

Full source

lemma coeffsIn_le {N : Submodule R (MvPolynomial σ S)} :
    coeffsIncoeffsIn σ M ≤ N ↔ ∀ m ∈ M, ∀ i, monomial i m ∈ N := by
  simp [coeffsIn_eq_span_monomial, Submodule.span_le, Set.subset_def,
    forall_swap (α := MvPolynomial σ S)]

Characterization of Submodule Containment via Monomial Membership

Informal description

For any submodule $N$ of the multivariate polynomial ring $S[X_i : i \in \sigma]$ over $R$, the submodule $\text{coeffsIn}\ \sigma\ M$ is contained in $N$ if and only if for every element $m \in M$ and every monomial index $i$, the monomial $m X^i$ belongs to $N$.

MvPolynomial.coeffsIn_mul theorem

(M N : Submodule R S) : coeffsIn σ (M * N) = coeffsIn σ M * coeffsIn σ N

Full source

lemma coeffsIn_mul (M N : Submodule R S) : coeffsIn σ (M * N) = coeffsIn σ M * coeffsIn σ N := by
  classical
  refine le_antisymm (coeffsIn_le.2 ?_) ?_
  · intros r hr s
    induction hr using Submodule.mul_induction_on' with
    | mem_mul_mem m hm n hn =>
      rw [← add_zero s, ← monomial_mul]
      apply Submodule.mul_mem_mul <;> simpa
    | add x _ y _ hx hy =>
      simpa [map_add] using add_mem hx hy
  · rw [Submodule.mul_le]
    intros x hx y hy k
    rw [MvPolynomial.coeff_mul]
    exact sum_mem fun c hc ↦ Submodule.mul_mem_mul (hx _) (hy _)

Product of Coefficient Submodules Equals Coefficient Submodule of Product

Informal description

For any submodules $M$ and $N$ of a commutative semiring $S$ over a ring $R$, the submodule of multivariate polynomials with coefficients in the product submodule $M \cdot N$ is equal to the product of the submodules of polynomials with coefficients in $M$ and $N$ respectively. That is, \[ \text{coeffsIn}\ \sigma\ (M \cdot N) = \text{coeffsIn}\ \sigma\ M \cdot \text{coeffsIn}\ \sigma\ N. \]

MvPolynomial.coeffsIn_pow theorem

: ∀ {n}, n ≠ 0 → ∀ M : Submodule R S, coeffsIn σ (M ^ n) = coeffsIn σ M ^ n

Full source

lemma coeffsIn_pow : ∀ {n}, n ≠ 0 → ∀ M : Submodule R S, coeffsIn σ (M ^ n) = coeffsIn σ M ^ n
  | 1, _, M => by simp
  | n + 2, _, M => by rw [pow_succ, coeffsIn_mul, coeffsIn_pow, ← pow_succ]; exact n.succ_ne_zero

Power of Coefficient Submodule Equals Coefficient Submodule of Power

Informal description

For any nonzero natural number $n$ and any submodule $M$ of a commutative semiring $S$ over a ring $R$, the submodule of multivariate polynomials with coefficients in the $n$-th power of $M$ is equal to the $n$-th power of the submodule of polynomials with coefficients in $M$. That is, \[ \text{coeffsIn}\ \sigma\ (M^n) = (\text{coeffsIn}\ \sigma\ M)^n. \]

MvPolynomial.le_coeffsIn_pow theorem

: ∀ {n}, coeffsIn σ M ^ n ≤ coeffsIn σ (M ^ n)

Full source

lemma le_coeffsIn_pow : ∀ {n}, coeffsIn σ M ^ n ≤ coeffsIn σ (M ^ n)
  | 0 => by simpa using ⟨1, map_one _⟩
  | n + 1 => (coeffsIn_pow n.succ_ne_zero _).ge

Inclusion of Power of Coefficient Submodule in Coefficient Submodule of Power

Informal description

For any natural number $n$ and any submodule $M$ of a commutative semiring $S$ over a ring $R$, the $n$-th power of the submodule of multivariate polynomials with coefficients in $M$ is contained in the submodule of polynomials with coefficients in the $n$-th power of $M$. That is, \[ (\text{coeffsIn}\ \sigma\ M)^n \leq \text{coeffsIn}\ \sigma\ (M^n). \]

Mathlib.Algebra.MvPolynomial.Basic

Important definitions

Notation

Definitions

Implementation notes

Tags