Mathlib.Algebra.Polynomial.Basic

Polynomial structure

(R : Type*) [Semiring R]

Full source

/-- `Polynomial R` is the type of univariate polynomials over `R`,
denoted as `R[X]` within the `Polynomial` namespace.

Polynomials should be seen as (semi-)rings with the additional constructor `X`.
The embedding from `R` is called `C`. -/
structure Polynomial (R : Type*) [Semiring R] where ofFinsupp ::
  toFinsupp : AddMonoidAlgebra R ℕ

Univariate Polynomials over a Semiring

Informal description

The structure `Polynomial R` represents the type of univariate polynomials over a semiring `R`, denoted as `R[X]`. It includes constructors for constant polynomials (`C`) and the polynomial variable (`X`), and provides operations and properties consistent with polynomial arithmetic.

Polynomial.term_[X] definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc] scoped[Polynomial] notation:9000 R "[X]" => Polynomial R

Polynomial ring notation `R[X]`

Informal description

The notation `R[X]` represents the type of univariate polynomials over the semiring `R`.

Polynomial.forall_iff_forall_finsupp theorem

(P : R[X] → Prop) : (∀ p, P p) ↔ ∀ q : R[ℕ], P ⟨q⟩

Full source

theorem forall_iff_forall_finsupp (P : R[X] → Prop) :
    (∀ p, P p) ↔ ∀ q : R[ℕ], P ⟨q⟩ :=
  ⟨fun h q => h ⟨q⟩, fun h ⟨p⟩ => h p⟩

Universal Quantification Equivalence between Polynomials and Additive Monoid Algebra Elements

Informal description

For any predicate $P$ on univariate polynomials over a semiring $R$, the statement that $P$ holds for all polynomials $p \in R[X]$ is equivalent to the statement that $P$ holds for all elements $q$ of the additive monoid algebra $R[\mathbb{N}]$ when viewed as polynomials via the canonical embedding $\langle q \rangle$.

Polynomial.exists_iff_exists_finsupp theorem

(P : R[X] → Prop) :
    (∃ p, P p) ↔ ∃ q : R[ℕ], P ⟨q⟩

Full source

theorem exists_iff_exists_finsupp (P : R[X] → Prop) :
    (∃ p, P p) ↔ ∃ q : R[ℕ], P ⟨q⟩ :=
  ⟨fun ⟨⟨p⟩, hp⟩ => ⟨p, hp⟩, fun ⟨q, hq⟩ => ⟨⟨q⟩, hq⟩⟩

Existence Correspondence Between Polynomials and Additive Monoid Algebra Elements

Informal description

For any predicate $P$ on univariate polynomials over a semiring $R$, there exists a polynomial $p$ satisfying $P(p)$ if and only if there exists an element $q$ of the additive monoid algebra $R[\mathbb{N}]$ such that $P(\langle q \rangle)$ holds.

Polynomial.eta theorem

(f : R[X]) : Polynomial.ofFinsupp f.toFinsupp = f

Full source

@[simp]
theorem eta (f : R[X]) : Polynomial.ofFinsupp f.toFinsupp = f := by cases f; rfl

Polynomial Representation Invariance under Conversion

Informal description

For any univariate polynomial $f$ over a semiring $R$, the polynomial obtained by converting $f$ to its underlying additive monoid algebra representation and back is equal to $f$ itself, i.e., $\text{ofFinsupp}(f.\text{toFinsupp}) = f$.

Polynomial.zero instance

: Zero R[X]

Full source

instance zero : Zero R[X] :=
  ⟨⟨0⟩⟩

Zero Element in Polynomial Ring

Informal description

The polynomial ring $R[X]$ over a semiring $R$ has a zero element, given by the constant polynomial $0$.

Polynomial.one instance

: One R[X]

Full source

instance one : One R[X] :=
  ⟨⟨1⟩⟩

Multiplicative Identity in Polynomial Ring

Informal description

The polynomial ring $R[X]$ over a semiring $R$ has a multiplicative identity element, given by the constant polynomial $1$.

Polynomial.add' instance

: Add R[X]

Full source

instance add' : Add R[X] :=
  ⟨add⟩

Addition Operation on Polynomials

Informal description

The type of univariate polynomials $R[X]$ over a semiring $R$ is equipped with a canonical addition operation.

Polynomial.neg' instance

{R : Type u} [Ring R] : Neg R[X]

Full source

instance neg' {R : Type u} [Ring R] : Neg R[X] :=
  ⟨neg⟩

Negation Operation on Polynomial Ring

Informal description

For any ring $R$, the polynomial ring $R[X]$ is equipped with a negation operation, making it an additive group.

Polynomial.sub instance

{R : Type u} [Ring R] : Sub R[X]

Full source

instance sub {R : Type u} [Ring R] : Sub R[X] :=
  ⟨fun a b => a + -b⟩

Subtraction Operation on Polynomial Ring

Informal description

For any ring $R$, the polynomial ring $R[X]$ is equipped with a canonical subtraction operation.

Polynomial.mul' instance

: Mul R[X]

Full source

instance mul' : Mul R[X] :=
  ⟨mul⟩

Multiplication Operation on Polynomial Ring

Informal description

The ring of univariate polynomials $R[X]$ over a semiring $R$ is equipped with a multiplication operation.

Polynomial.add_eq_add theorem

: add p q = p + q

Full source

@[simp] theorem add_eq_add : add p q = p + q := rfl

Equivalence of Polynomial Addition Operations

Informal description

For any two polynomials $p$ and $q$ in $R[X]$, the addition operation defined via `add` is equal to the standard polynomial addition operation $p + q$.

Polynomial.mul_eq_mul theorem

: mul p q = p * q

Full source

@[simp] theorem mul_eq_mul : mul p q = p * q := rfl

Equivalence of Polynomial Multiplication Operations

Informal description

For any two polynomials $p$ and $q$ in $R[X]$, the multiplication operation defined via `mul` is equal to the standard polynomial multiplication operation $p * q$.

Polynomial.instNSMul instance

: SMul ℕ R[X]

Full source

instance instNSMul : SMul ℕ R[X] where
  smul r p := ⟨r • p.toFinsupp⟩

Natural Number Scalar Multiplication on Polynomials

Informal description

The type of univariate polynomials $R[X]$ over a semiring $R$ has a natural scalar multiplication operation by natural numbers, defined by repeated addition.

Polynomial.smulZeroClass instance

{S : Type*} [SMulZeroClass S R] : SMulZeroClass S R[X]

Full source

instance smulZeroClass {S : Type*} [SMulZeroClass S R] : SMulZeroClass S R[X] where
  smul r p := ⟨r • p.toFinsupp⟩
  smul_zero a := congr_arg ofFinsupp (smul_zero a)

Scalar Multiplication Preserving Zero in Polynomial Ring

Informal description

For any type $S$ with a scalar multiplication action on a semiring $R$ that preserves zero (i.e., $s \cdot 0 = 0$ for all $s \in S$), the polynomial ring $R[X]$ inherits a scalar multiplication action from $S$ that also preserves zero. This action is defined by extending the scalar multiplication coefficient-wise: $(s \cdot p)(X) = \sum_{n} (s \cdot a_n) X^n$ for any polynomial $p(X) = \sum_{n} a_n X^n \in R[X]$.

Polynomial.instNoZeroSMulDivisors instance

{S : Type*} [Zero S] [SMulZeroClass S R] [NoZeroSMulDivisors S R] : NoZeroSMulDivisors S R[X]

Full source

instance {S : Type*} [Zero S] [SMulZeroClass S R] [NoZeroSMulDivisors S R] :
    NoZeroSMulDivisors S R[X] where
  eq_zero_or_eq_zero_of_smul_eq_zero eq :=
    (eq_zero_or_eq_zero_of_smul_eq_zero <| congr_arg toFinsupp eq).imp id (congr_arg ofFinsupp)

No Zero Divisors in Scalar Multiplication of Polynomial Ring

Informal description

For any type $S$ with a zero element and a scalar multiplication action on a semiring $R$ that preserves zero, if $S$ and $R$ have no zero divisors with respect to scalar multiplication (i.e., $s \cdot r = 0$ implies $s = 0$ or $r = 0$ for all $s \in S$ and $r \in R$), then the polynomial ring $R[X]$ also has no zero divisors with respect to the coefficient-wise scalar multiplication from $S$.

Polynomial.pow instance

: Pow R[X] ℕ

Full source

instance (priority := 1) pow : Pow R[X] ℕ where pow p n := npowRec n p

Power Operation on Polynomial Ring

Informal description

The ring of univariate polynomials $R[X]$ over a semiring $R$ is equipped with a power operation, where for any polynomial $p \in R[X]$ and natural number $n \in \mathbb{N}$, the power $p^n$ is defined as the product of $p$ multiplied by itself $n$ times.

Polynomial.ofFinsupp_zero theorem

: (⟨0⟩ : R[X]) = 0

Full source

@[simp]
theorem ofFinsupp_zero : (⟨0⟩ : R[X]) = 0 :=
  rfl

Zero Polynomial Construction from Monoid Algebra: $\langle 0 \rangle = 0$

Informal description

The polynomial constructed from the zero element of the additive monoid algebra is equal to the zero polynomial in $R[X]$, i.e., $\langle 0 \rangle = 0$.

Polynomial.ofFinsupp_one theorem

: (⟨1⟩ : R[X]) = 1

Full source

@[simp]
theorem ofFinsupp_one : (⟨1⟩ : R[X]) = 1 :=
  rfl

Lifting of Multiplicative Identity to Polynomial Ring: $\langle 1 \rangle = 1$

Informal description

The polynomial obtained by lifting the multiplicative identity $1$ from the additive monoid algebra to the polynomial ring $R[X]$ is equal to the constant polynomial $1$.

Polynomial.ofFinsupp_add theorem

{a b} : (⟨a + b⟩ : R[X]) = ⟨a⟩ + ⟨b⟩

Full source

@[simp]
theorem ofFinsupp_add {a b} : (⟨a + b⟩ : R[X]) = ⟨a⟩ + ⟨b⟩ :=
  show _ = add _ _ by rw [add_def]

Addition Commutes with Polynomial Construction from Monoid Algebra

Informal description

For any elements $a$ and $b$ in the additive monoid algebra over a semiring $R$, the polynomial constructed from the sum $a + b$ is equal to the sum of the polynomials constructed from $a$ and $b$ separately. In other words, the construction of polynomials from monoid algebra elements preserves addition: $$\langle a + b \rangle = \langle a \rangle + \langle b \rangle$$

Polynomial.ofFinsupp_neg theorem

{R : Type u} [Ring R] {a} : (⟨-a⟩ : R[X]) = -⟨a⟩

Full source

@[simp]
theorem ofFinsupp_neg {R : Type u} [Ring R] {a} : (⟨-a⟩ : R[X]) = -⟨a⟩ :=
  show _ = neg _ by rw [neg_def]

Negation Commutes with Polynomial Construction from Monoid Algebra

Informal description

For any ring $R$ and any element $a$ in the additive monoid algebra over $R$, the polynomial constructed from the negation of $a$ is equal to the negation of the polynomial constructed from $a$. In other words, the construction of polynomials from monoid algebra elements commutes with negation: $$\langle -a \rangle = -\langle a \rangle$$

Polynomial.ofFinsupp_sub theorem

{R : Type u} [Ring R] {a b} : (⟨a - b⟩ : R[X]) = ⟨a⟩ - ⟨b⟩

Full source

@[simp]
theorem ofFinsupp_sub {R : Type u} [Ring R] {a b} : (⟨a - b⟩ : R[X]) = ⟨a⟩ - ⟨b⟩ := by
  rw [sub_eq_add_neg, ofFinsupp_add, ofFinsupp_neg]
  rfl

Subtraction Commutes with Polynomial Construction from Monoid Algebra

Informal description

For any ring $R$ and any elements $a, b$ in the additive monoid algebra over $R$, the polynomial constructed from the difference $a - b$ is equal to the difference of the polynomials constructed from $a$ and $b$ separately. That is, $$\langle a - b \rangle = \langle a \rangle - \langle b \rangle$$ where $\langle \cdot \rangle$ denotes the polynomial construction from the monoid algebra and $-$ denotes polynomial subtraction.

Polynomial.ofFinsupp_mul theorem

(a b) : (⟨a * b⟩ : R[X]) = ⟨a⟩ * ⟨b⟩

Full source

@[simp]
theorem ofFinsupp_mul (a b) : (⟨a * b⟩ : R[X]) = ⟨a⟩ * ⟨b⟩ :=
  show _ = mul _ _ by rw [mul_def]

Polynomial Construction Preserves Multiplication

Informal description

For any elements $a$ and $b$ in the additive monoid algebra over a semiring $R$, the polynomial constructed from the product $a * b$ is equal to the product of the polynomials constructed from $a$ and $b$ individually. That is, $$\langle a * b \rangle = \langle a \rangle \cdot \langle b \rangle$$ where $\langle \cdot \rangle$ denotes the polynomial construction from the monoid algebra and $\cdot$ denotes polynomial multiplication.

Polynomial.ofFinsupp_nsmul theorem

(a : ℕ) (b) : (⟨a • b⟩ : R[X]) = (a • ⟨b⟩ : R[X])

Full source

@[simp]
theorem ofFinsupp_nsmul (a : ℕ) (b) :
    (⟨a • b⟩ : R[X]) = (a • ⟨b⟩ : R[X]) :=
  rfl

Polynomial Construction Preserves Natural Number Scalar Multiplication

Informal description

For any natural number $a$ and any element $b$ in the additive monoid algebra over a semiring $R$, the polynomial constructed from the scalar multiple $a \cdot b$ is equal to the scalar multiple $a$ applied to the polynomial constructed from $b$. That is, $$\langle a \cdot b \rangle = a \cdot \langle b \rangle$$ where $\langle \cdot \rangle$ denotes the polynomial construction from the monoid algebra and $\cdot$ denotes scalar multiplication.

Polynomial.ofFinsupp_smul theorem

{S : Type*} [SMulZeroClass S R] (a : S) (b) : (⟨a • b⟩ : R[X]) = (a • ⟨b⟩ : R[X])

Full source

@[simp]
theorem ofFinsupp_smul {S : Type*} [SMulZeroClass S R] (a : S) (b) :
    (⟨a • b⟩ : R[X]) = (a • ⟨b⟩ : R[X]) :=
  rfl

Polynomial Construction Preserves Scalar Multiplication

Informal description

Let $R$ be a semiring and $S$ be a type equipped with a scalar multiplication action on $R$ that preserves zero. For any scalar $a \in S$ and any element $b$ in the additive monoid algebra over $R$, the polynomial constructed from the scalar multiple $a \cdot b$ is equal to the scalar multiple $a$ applied to the polynomial constructed from $b$. That is, $$\langle a \cdot b \rangle = a \cdot \langle b \rangle$$ where $\langle \cdot \rangle$ denotes the polynomial construction from the monoid algebra and $\cdot$ denotes the scalar multiplication operation.

Polynomial.ofFinsupp_pow theorem

(a) (n : ℕ) : (⟨a ^ n⟩ : R[X]) = ⟨a⟩ ^ n

Full source

@[simp]
theorem ofFinsupp_pow (a) (n : ℕ) : (⟨a ^ n⟩ : R[X]) = ⟨a⟩ ^ n := by
  change _ = npowRec n _
  induction n with
  | zero        => simp [npowRec]
  | succ n n_ih => simp [npowRec, n_ih, pow_succ]

Power Preservation in Polynomial Construction: $\langle a^n \rangle = \langle a \rangle^n$

Informal description

For any element $a$ in the additive monoid algebra over a semiring $R$ and any natural number $n$, the polynomial constructed from the $n$-th power of $a$ is equal to the $n$-th power of the polynomial constructed from $a$. That is, $$\langle a^n \rangle = \langle a \rangle^n$$ where $\langle \cdot \rangle$ denotes the polynomial construction from the monoid algebra.

Polynomial.toFinsupp_zero theorem

: (0 : R[X]).toFinsupp = 0

Full source

@[simp]
theorem toFinsupp_zero : (0 : R[X]).toFinsupp = 0 :=
  rfl

Preservation of Zero in Polynomial to Additive Monoid Algebra Map

Informal description

The image of the zero polynomial $0 \in R[X]$ under the canonical map to the additive monoid algebra $R[\mathbb{N}]$ is equal to the zero element $0$ in $R[\mathbb{N}]$.

Polynomial.toFinsupp_one theorem

: (1 : R[X]).toFinsupp = 1

Full source

@[simp]
theorem toFinsupp_one : (1 : R[X]).toFinsupp = 1 :=
  rfl

Preservation of Multiplicative Identity in Polynomial to Additive Monoid Algebra Map

Informal description

The image of the multiplicative identity polynomial $1 \in R[X]$ under the canonical map to the additive monoid algebra $R[\mathbb{N}]$ is equal to the multiplicative identity element $1$ in $R[\mathbb{N}]$.

Polynomial.toFinsupp_add theorem

(a b : R[X]) : (a + b).toFinsupp = a.toFinsupp + b.toFinsupp

Full source

@[simp]
theorem toFinsupp_add (a b : R[X]) : (a + b).toFinsupp = a.toFinsupp + b.toFinsupp := by
  cases a
  cases b
  rw [← ofFinsupp_add]

Additivity of Polynomial to Monoid Algebra Map

Informal description

For any two polynomials $a, b \in R[X]$ over a semiring $R$, the image of their sum under the canonical map to the additive monoid algebra $R[\mathbb{N}]$ is equal to the sum of their individual images. That is, $$(a + b).\text{toFinsupp} = a.\text{toFinsupp} + b.\text{toFinsupp}.$$

Polynomial.toFinsupp_neg theorem

{R : Type u} [Ring R] (a : R[X]) : (-a).toFinsupp = -a.toFinsupp

Full source

@[simp]
theorem toFinsupp_neg {R : Type u} [Ring R] (a : R[X]) : (-a).toFinsupp = -a.toFinsupp := by
  cases a
  rw [← ofFinsupp_neg]

Negation Commutes with Polynomial to Monoid Algebra Map

Informal description

For any ring $R$ and any polynomial $a \in R[X]$, the image of the negation $-a$ under the canonical map to the additive monoid algebra $R[\mathbb{N}]$ is equal to the negation of the image of $a$ under the same map. In other words, the map commutes with negation: $$(-a).\text{toFinsupp} = -a.\text{toFinsupp}$$

Polynomial.toFinsupp_sub theorem

{R : Type u} [Ring R] (a b : R[X]) : (a - b).toFinsupp = a.toFinsupp - b.toFinsupp

Full source

@[simp]
theorem toFinsupp_sub {R : Type u} [Ring R] (a b : R[X]) :
    (a - b).toFinsupp = a.toFinsupp - b.toFinsupp := by
  rw [sub_eq_add_neg, ← toFinsupp_neg, ← toFinsupp_add]
  rfl

Subtraction Preserved by Polynomial to Monoid Algebra Map

Informal description

For any ring $R$ and any polynomials $a, b \in R[X]$, the image of the difference $a - b$ under the canonical map to the additive monoid algebra $R[\mathbb{N}]$ equals the difference of their individual images. That is, $$(a - b).\text{toFinsupp} = a.\text{toFinsupp} - b.\text{toFinsupp}.$$

Polynomial.toFinsupp_mul theorem

(a b : R[X]) : (a * b).toFinsupp = a.toFinsupp * b.toFinsupp

Full source

@[simp]
theorem toFinsupp_mul (a b : R[X]) : (a * b).toFinsupp = a.toFinsupp * b.toFinsupp := by
  cases a
  cases b
  rw [← ofFinsupp_mul]

Polynomial Multiplication Preserved by Monoid Algebra Map

Informal description

For any two polynomials $a, b \in R[X]$ over a semiring $R$, the image of their product under the canonical map to the additive monoid algebra $R[\mathbb{N}]$ equals the product of their individual images. That is, $$(a \cdot b).\text{toFinsupp} = a.\text{toFinsupp} \cdot b.\text{toFinsupp}.$$

Polynomial.toFinsupp_nsmul theorem

(a : ℕ) (b : R[X]) : (a • b).toFinsupp = a • b.toFinsupp

Full source

@[simp]
theorem toFinsupp_nsmul (a : ℕ) (b : R[X]) :
    (a • b).toFinsupp = a • b.toFinsupp :=
  rfl

Natural Number Scalar Multiplication Preserved by Monoid Algebra Map

Informal description

For any natural number $a$ and any polynomial $b \in R[X]$ over a semiring $R$, the image of the scalar multiple $a \cdot b$ under the canonical map to the additive monoid algebra $R[\mathbb{N}]$ equals the scalar multiple of the image of $b$. That is, $$(a \cdot b).\text{toFinsupp} = a \cdot b.\text{toFinsupp}.$$

Polynomial.toFinsupp_smul theorem

{S : Type*} [SMulZeroClass S R] (a : S) (b : R[X]) : (a • b).toFinsupp = a • b.toFinsupp

Full source

@[simp]
theorem toFinsupp_smul {S : Type*} [SMulZeroClass S R] (a : S) (b : R[X]) :
    (a • b).toFinsupp = a • b.toFinsupp :=
  rfl

Scalar Multiplication Commutes with Polynomial-to-Monoid-Algebra Map

Informal description

For any scalar $a$ in a type $S$ with a scalar multiplication action on a semiring $R$ that preserves zero, and for any polynomial $b \in R[X]$, the image of the scalar multiple $a \cdot b$ under the canonical map to the additive monoid algebra $R[\mathbb{N}]$ equals the scalar multiple of the image of $b$. That is, $$(a \cdot b).\text{toFinsupp} = a \cdot b.\text{toFinsupp}.$$

Polynomial.toFinsupp_pow theorem

(a : R[X]) (n : ℕ) : (a ^ n).toFinsupp = a.toFinsupp ^ n

Full source

@[simp]
theorem toFinsupp_pow (a : R[X]) (n : ℕ) : (a ^ n).toFinsupp = a.toFinsupp ^ n := by
  cases a
  rw [← ofFinsupp_pow]

Power Preservation under Polynomial-to-Monoid-Algebra Map: $(a^n).\text{toFinsupp} = (a.\text{toFinsupp})^n$

Informal description

For any polynomial $a \in R[X]$ over a semiring $R$ and any natural number $n \in \mathbb{N}$, the image of $a^n$ under the canonical map to the additive monoid algebra $R[\mathbb{N}]$ equals the $n$-th power of the image of $a$. That is, $$(a^n).\text{toFinsupp} = (a.\text{toFinsupp})^n.$$

IsSMulRegular.polynomial theorem

{S : Type*} [SMulZeroClass S R] {a : S} (ha : IsSMulRegular R a) : IsSMulRegular R[X] a

Full source

theorem _root_.IsSMulRegular.polynomial {S : Type*} [SMulZeroClass S R] {a : S}
    (ha : IsSMulRegular R a) : IsSMulRegular R[X] a
  | ⟨_x⟩, ⟨_y⟩, h => congr_arg _ <| ha.finsupp (Polynomial.ofFinsupp.inj h)

Regularity of scalar multiplication in polynomial rings: $R$-regular implies $R[X]$-regular

Informal description

Let $R$ be a semiring and $S$ be a type with a scalar multiplication action on $R$ that preserves zero. If an element $a \in S$ is $R$-regular (i.e., the map $x \mapsto a \cdot x$ is injective on $R$), then $a$ is also $R[X]$-regular (i.e., the map $p \mapsto a \cdot p$ is injective on the polynomial ring $R[X]$).

Polynomial.toFinsupp_injective theorem

: Function.Injective (toFinsupp : R[X] → AddMonoidAlgebra _ _)

Full source

theorem toFinsupp_injective : Function.Injective (toFinsupp : R[X] → AddMonoidAlgebra _ _) :=
  fun ⟨_x⟩ ⟨_y⟩ => congr_arg _

Injectivity of the Polynomial-to-AddMonoidAlgebra Map

Informal description

The function `toFinsupp`, which maps a polynomial `p ∈ R[X]` to its representation as an element of the additive monoid algebra `R[ℕ]`, is injective. That is, for any two polynomials `p, q ∈ R[X]`, if `toFinsupp p = toFinsupp q`, then `p = q`.

Polynomial.toFinsupp_inj theorem

{a b : R[X]} : a.toFinsupp = b.toFinsupp ↔ a = b

Full source

@[simp]
theorem toFinsupp_inj {a b : R[X]} : a.toFinsupp = b.toFinsupp ↔ a = b :=
  toFinsupp_injective.eq_iff

Equivalence of Polynomial Equality and Additive Monoid Algebra Representation Equality

Informal description

For any two polynomials $a, b \in R[X]$, the equality of their representations in the additive monoid algebra $R[\mathbb{N}]$ is equivalent to the equality of the polynomials themselves. That is, $a.\text{toFinsupp} = b.\text{toFinsupp}$ if and only if $a = b$.

Polynomial.toFinsupp_eq_zero theorem

{a : R[X]} : a.toFinsupp = 0 ↔ a = 0

Full source

@[simp]
theorem toFinsupp_eq_zero {a : R[X]} : a.toFinsupp = 0 ↔ a = 0 := by
  rw [← toFinsupp_zero, toFinsupp_inj]

Zero Polynomial Characterization via Additive Monoid Algebra Representation

Informal description

For any polynomial $a \in R[X]$, the representation of $a$ in the additive monoid algebra $R[\mathbb{N}]$ is equal to the zero element if and only if $a$ is the zero polynomial.

Polynomial.toFinsupp_eq_one theorem

{a : R[X]} : a.toFinsupp = 1 ↔ a = 1

Full source

@[simp]
theorem toFinsupp_eq_one {a : R[X]} : a.toFinsupp = 1 ↔ a = 1 := by
  rw [← toFinsupp_one, toFinsupp_inj]

Equivalence of Polynomial Identity and Additive Monoid Algebra Identity Representation

Informal description

For any polynomial $a \in R[X]$, the equality $a.\text{toFinsupp} = 1$ holds in the additive monoid algebra $R[\mathbb{N}]$ if and only if $a$ is the multiplicative identity polynomial $1$ in $R[X]$.

Polynomial.ofFinsupp_inj theorem

{a b} : (⟨a⟩ : R[X]) = ⟨b⟩ ↔ a = b

Full source

/-- A more convenient spelling of `Polynomial.ofFinsupp.injEq` in terms of `Iff`. -/
theorem ofFinsupp_inj {a b} : (⟨a⟩ : R[X]) = ⟨b⟩ ↔ a = b :=
  iff_of_eq (ofFinsupp.injEq _ _)

Injectivity of Polynomial Construction from Additive Monoid Algebra

Informal description

For any two elements $a$ and $b$ in the additive monoid algebra $R[\mathbb{N}]$, the polynomial $\langle a \rangle$ is equal to $\langle b \rangle$ in $R[X]$ if and only if $a = b$ in $R[\mathbb{N}]$.

Polynomial.ofFinsupp_eq_zero theorem

{a} : (⟨a⟩ : R[X]) = 0 ↔ a = 0

Full source

@[simp]
theorem ofFinsupp_eq_zero {a} : (⟨a⟩ : R[X]) = 0 ↔ a = 0 := by
  rw [← ofFinsupp_zero, ofFinsupp_inj]

Zero Polynomial Equivalence: $\langle a \rangle = 0 \leftrightarrow a = 0$

Informal description

For any element $a$ in the additive monoid algebra $R[\mathbb{N}]$, the polynomial $\langle a \rangle$ in $R[X]$ is equal to the zero polynomial if and only if $a$ is the zero element in $R[\mathbb{N}]$.

Polynomial.ofFinsupp_eq_one theorem

{a} : (⟨a⟩ : R[X]) = 1 ↔ a = 1

Full source

@[simp]
theorem ofFinsupp_eq_one {a} : (⟨a⟩ : R[X]) = 1 ↔ a = 1 := by rw [← ofFinsupp_one, ofFinsupp_inj]

Equivalence of Polynomial and Additive Monoid Algebra Identities: $\langle a \rangle = 1 \leftrightarrow a = 1$

Informal description

For any element $a$ in the additive monoid algebra $R[\mathbb{N}]$, the polynomial $\langle a \rangle$ in $R[X]$ is equal to the constant polynomial $1$ if and only if $a$ is equal to the multiplicative identity $1$ in $R[\mathbb{N}]$.

Polynomial.inhabited instance

: Inhabited R[X]

Full source

instance inhabited : Inhabited R[X] :=
  ⟨0⟩

Inhabitedness of Polynomial Rings

Informal description

The polynomial ring $R[X]$ over a semiring $R$ is inhabited, meaning it contains at least one element.

Polynomial.instNatCast instance

: NatCast R[X]

Full source

instance instNatCast : NatCast R[X] where natCast n := ofFinsupp n

Natural Number Cast in Polynomial Semiring

Informal description

The polynomial ring $R[X]$ over a semiring $R$ has a canonical structure of a semiring with a natural number casting operation, where for any natural number $n$, the cast $\uparrow n$ is the constant polynomial $n \cdot 1_R$.

Polynomial.ofFinsupp_natCast theorem

(n : ℕ) : (⟨n⟩ : R[X]) = n

Full source

@[simp]
theorem ofFinsupp_natCast (n : ℕ) : (⟨n⟩ : R[X]) = n := rfl

Natural number casting via `ofFinsupp` yields constant polynomial

Informal description

For any natural number $n$, the polynomial obtained by casting $n$ through the `ofFinsupp` constructor is equal to the constant polynomial $n$ in the polynomial ring $R[X]$.

Polynomial.toFinsupp_natCast theorem

(n : ℕ) : (n : R[X]).toFinsupp = n

Full source

@[simp]
theorem toFinsupp_natCast (n : ℕ) : (n : R[X]).toFinsupp = n := rfl

Natural Number Coercion in Polynomial Ring Preserves Value

Informal description

For any natural number $n$, the canonical map from the polynomial ring $R[X]$ to the additive monoid algebra $R[\mathbb{N}]$ sends the constant polynomial $n$ to the natural number $n$ in $R[\mathbb{N}]$. In other words, the coercion of $n$ as a polynomial is equal to $n$ in the additive monoid algebra.

Polynomial.ofFinsupp_ofNat theorem

(n : ℕ) [n.AtLeastTwo] : (⟨ofNat(n)⟩ : R[X]) = ofNat(n)

Full source

@[simp]
theorem ofFinsupp_ofNat (n : ℕ) [n.AtLeastTwo] : (⟨ofNat(n)⟩ : R[X]) = ofNat(n) := rfl

Preservation of Numerals $\geq 2$ under Polynomial Construction from Additive Monoid Algebra

Informal description

For any natural number $n \geq 2$, the polynomial constructed from the additive monoid algebra element corresponding to the numeral $n$ is equal to the constant polynomial $n$ in $R[X]$. In other words, the embedding $\langle \cdot \rangle : R[\mathbb{N}] \to R[X]$ preserves numerals $\geq 2$.

Polynomial.toFinsupp_ofNat theorem

(n : ℕ) [n.AtLeastTwo] : (ofNat(n) : R[X]).toFinsupp = ofNat(n)

Full source

@[simp]
theorem toFinsupp_ofNat (n : ℕ) [n.AtLeastTwo] : (ofNat(n) : R[X]).toFinsupp = ofNat(n) := rfl

Conversion of Constant Polynomial $n \geq 2$ to Additive Monoid Algebra Preserves Value

Informal description

For any natural number $n \geq 2$, the conversion of the polynomial $n$ (interpreted as a constant polynomial in $R[X]$) to its underlying additive monoid algebra representation equals the natural number $n$ interpreted in the additive monoid algebra.

Polynomial.semiring instance

: Semiring R[X]

Full source

instance semiring : Semiring R[X] :=
  fast_instance% Function.Injective.semiring toFinsupp toFinsupp_injective toFinsupp_zero
    toFinsupp_one toFinsupp_add toFinsupp_mul (fun _ _ => toFinsupp_nsmul _ _) toFinsupp_pow
    fun _ => rfl

Semiring Structure on Polynomial Ring $R[X]$

Informal description

The ring of univariate polynomials $R[X]$ over a semiring $R$ forms a semiring, where addition and multiplication are defined in the usual way for polynomials.

Polynomial.distribSMul instance

{S} [DistribSMul S R] : DistribSMul S R[X]

Full source

instance distribSMul {S} [DistribSMul S R] : DistribSMul S R[X] :=
  fast_instance% Function.Injective.distribSMul ⟨⟨toFinsupp, toFinsupp_zero⟩, toFinsupp_add⟩
    toFinsupp_injective toFinsupp_smul

Distributive Scalar Multiplication on Polynomial Rings

Informal description

For any type $S$ with a distributive scalar multiplication action on a semiring $R$, the polynomial ring $R[X]$ inherits a distributive scalar multiplication action from $S$. This action is defined coefficient-wise: $(s \cdot p)(X) = \sum_{n} (s \cdot a_n) X^n$ for any polynomial $p(X) = \sum_{n} a_n X^n \in R[X]$, and satisfies $s \cdot (p + q) = s \cdot p + s \cdot q$ for all $s \in S$ and $p, q \in R[X]$.

Polynomial.distribMulAction instance

{S} [Monoid S] [DistribMulAction S R] : DistribMulAction S R[X]

Full source

instance distribMulAction {S} [Monoid S] [DistribMulAction S R] : DistribMulAction S R[X] :=
  fast_instance% Function.Injective.distribMulAction
    ⟨⟨toFinsupp, toFinsupp_zero (R := R)⟩, toFinsupp_add⟩ toFinsupp_injective toFinsupp_smul

Distributive Multiplicative Action on Polynomial Rings

Informal description

For any monoid $S$ acting distributively on a semiring $R$, the polynomial ring $R[X]$ inherits a distributive multiplicative action from $S$. This action is defined coefficient-wise: for any polynomial $p(X) = \sum_n a_n X^n \in R[X]$ and $s \in S$, we have $(s \cdot p)(X) = \sum_n (s \cdot a_n) X^n$.

Polynomial.faithfulSMul instance

{S} [SMulZeroClass S R] [FaithfulSMul S R] : FaithfulSMul S R[X]

Full source

instance faithfulSMul {S} [SMulZeroClass S R] [FaithfulSMul S R] : FaithfulSMul S R[X] where
  eq_of_smul_eq_smul {_s₁ _s₂} h :=
    eq_of_smul_eq_smul fun a : ℕℕ →₀ R => congr_arg toFinsupp (h ⟨a⟩)

Faithfulness of Scalar Multiplication in Polynomial Rings

Informal description

For any type $S$ with a scalar multiplication action on a semiring $R$ that preserves zero, if the scalar multiplication action of $S$ on $R$ is faithful (i.e., distinct elements of $S$ act differently on some element of $R$), then the induced scalar multiplication action of $S$ on the polynomial ring $R[X]$ is also faithful. This action is defined coefficient-wise: $(s \cdot p)(X) = \sum_{n} (s \cdot a_n) X^n$ for any polynomial $p(X) = \sum_{n} a_n X^n \in R[X]$.

Polynomial.module instance

{S} [Semiring S] [Module S R] : Module S R[X]

Full source

instance module {S} [Semiring S] [Module S R] : Module S R[X] :=
  fast_instance% Function.Injective.module _ ⟨⟨toFinsupp, toFinsupp_zero⟩, toFinsupp_add⟩
    toFinsupp_injective toFinsupp_smul

Module Structure on Polynomial Rings via Coefficient-wise Scalar Multiplication

Informal description

For any semiring $S$ and module $M$ over $S$ where $M$ is a semiring $R$, the polynomial ring $R[X]$ inherits a module structure over $S$. This module structure is defined coefficient-wise: for any polynomial $p(X) = \sum_n a_n X^n \in R[X]$ and scalar $s \in S$, the scalar multiplication is given by $(s \cdot p)(X) = \sum_n (s \cdot a_n) X^n$.

Polynomial.smulCommClass instance

{S₁ S₂} [SMulZeroClass S₁ R] [SMulZeroClass S₂ R] [SMulCommClass S₁ S₂ R] : SMulCommClass S₁ S₂ R[X]

Full source

instance smulCommClass {S₁ S₂} [SMulZeroClass S₁ R] [SMulZeroClass S₂ R] [SMulCommClass S₁ S₂ R] :
  SMulCommClass S₁ S₂ R[X] :=
  ⟨by
    rintro m n ⟨f⟩
    simp_rw [← ofFinsupp_smul, smul_comm m n f]⟩

Commutativity of Scalar Multiplication in Polynomial Rings

Informal description

For any semiring $R$ and types $S₁$, $S₂$ with scalar multiplication actions on $R$ that preserve zero, if the actions of $S₁$ and $S₂$ on $R$ commute, then the coefficient-wise scalar multiplication actions of $S₁$ and $S₂$ on the polynomial ring $R[X]$ also commute. That is, for any $s₁ \in S₁$, $s₂ \in S₂$, and $p \in R[X]$, we have $s₁ \cdot (s₂ \cdot p) = s₂ \cdot (s₁ \cdot p)$.

Polynomial.isScalarTower instance

 {S₁ S₂} [SMul S₁ S₂] [SMulZeroClass S₁ R] [SMulZeroClass S₂ R] [IsScalarTower S₁ S₂ R] : IsScalarTower S₁ S₂ R[X]

Full source

instance isScalarTower {S₁ S₂} [SMul S₁ S₂] [SMulZeroClass S₁ R] [SMulZeroClass S₂ R]
  [IsScalarTower S₁ S₂ R] : IsScalarTower S₁ S₂ R[X] :=
  ⟨by
    rintro _ _ ⟨⟩
    simp_rw [← ofFinsupp_smul, smul_assoc]⟩

Scalar Tower Property for Polynomial Rings

Informal description

For any semiring $R$ and types $S_1$, $S_2$ with scalar multiplication actions on $R$ that preserve zero, if $S_1$ and $S_2$ form a scalar tower over $R$ (i.e., $(s_1 \cdot s_2) \cdot r = s_1 \cdot (s_2 \cdot r)$ for all $s_1 \in S_1$, $s_2 \in S_2$, $r \in R$), then the polynomial ring $R[X]$ also forms a scalar tower with respect to the coefficient-wise scalar multiplication.

Polynomial.isScalarTower_right instance

{α K : Type*} [Semiring K] [DistribSMul α K] [IsScalarTower α K K] : IsScalarTower α K[X] K[X]

Full source

instance isScalarTower_right {α K : Type*} [Semiring K] [DistribSMul α K] [IsScalarTower α K K] :
    IsScalarTower α K[X] K[X] :=
  ⟨by
    rintro _ ⟨⟩ ⟨⟩
    simp_rw [smul_eq_mul, ← ofFinsupp_smul, ← ofFinsupp_mul, ← ofFinsupp_smul, smul_mul_assoc]⟩

Scalar Tower Property for Polynomial Rings with Distributive Scalar Multiplication

Informal description

For any semiring $K$ and type $\alpha$ with a distributive scalar multiplication action on $K$ that satisfies the scalar tower property (i.e., $(a \cdot b) \cdot c = a \cdot (b \cdot c)$ for all $a \in \alpha$, $b, c \in K$), the polynomial ring $K[X]$ also satisfies the scalar tower property with respect to the coefficient-wise scalar multiplication. That is, for any $a \in \alpha$ and polynomials $p, q \in K[X]$, we have $(a \cdot p) * q = a \cdot (p * q)$, where $*$ denotes polynomial multiplication.

Polynomial.isCentralScalar instance

{S} [SMulZeroClass S R] [SMulZeroClass Sᵐᵒᵖ R] [IsCentralScalar S R] : IsCentralScalar S R[X]

Full source

instance isCentralScalar {S} [SMulZeroClass S R] [SMulZeroClass Sᵐᵒᵖ R] [IsCentralScalar S R] :
  IsCentralScalar S R[X] :=
  ⟨by
    rintro _ ⟨⟩
    simp_rw [← ofFinsupp_smul, op_smul_eq_smul]⟩

Central Scalar Property for Polynomial Rings

Informal description

For any type $S$ with a scalar multiplication action on a semiring $R$ that preserves zero and satisfies the central scalar property (i.e., the left and right scalar multiplication actions of $S$ on $R$ coincide), the polynomial ring $R[X]$ inherits this central scalar property. That is, for any $s \in S$ and $p \in R[X]$, the left and right scalar multiplications $s \cdot p$ and $p \cdot s$ (via the multiplicative opposite $S^\text{op}$) are equal.

Polynomial.unique instance

[Subsingleton R] : Unique R[X]

Full source

instance unique [Subsingleton R] : Unique R[X] :=
  { Polynomial.inhabited with
    uniq := by
      rintro ⟨x⟩
      apply congr_arg ofFinsupp
      simp [eq_iff_true_of_subsingleton] }

Uniqueness of Polynomial Ring over Subsingleton Semiring

Informal description

When the semiring $R$ is a subsingleton (i.e., all elements of $R$ are equal), the polynomial ring $R[X]$ has exactly one element.

Polynomial.toFinsuppIso definition

: R[X] ≃+* R[ℕ]

Full source

/-- Ring isomorphism between `R[X]` and `R[ℕ]`. This is just an
implementation detail, but it can be useful to transfer results from `Finsupp` to polynomials. -/
@[simps apply symm_apply]
def toFinsuppIso : R[X]R[X] ≃+* R[ℕ] where
  toFun := toFinsupp
  invFun := ofFinsupp
  left_inv := fun ⟨_p⟩ => rfl
  right_inv _p := rfl
  map_mul' := toFinsupp_mul
  map_add' := toFinsupp_add

Polynomial ring isomorphism with additive monoid algebra

Informal description

The ring isomorphism between the polynomial ring $R[X]$ and the additive monoid algebra $R[\mathbb{N}]$, given by the canonical maps `toFinsupp` and `ofFinsupp`. Specifically: - The forward map sends a polynomial $p \in R[X]$ to its representation as a finitely supported function $\mathbb{N} \to R$ - The inverse map reconstructs a polynomial from such a representation - The isomorphism preserves both the additive and multiplicative structures This isomorphism is primarily an implementation detail for transferring results between polynomial and monoid algebra representations.

Polynomial.instDecidableEq instance

[DecidableEq R] : DecidableEq R[X]

Full source

instance [DecidableEq R] : DecidableEq R[X] :=
  @Equiv.decidableEq R[X] _ (toFinsuppIso R).toEquiv (Finsupp.instDecidableEq)

Decidable Equality for Polynomial Rings

Informal description

For any semiring $R$ with decidable equality, the polynomial ring $R[X]$ also has decidable equality.

Polynomial.toFinsuppIsoLinear definition

: R[X] ≃ₗ[R] R[ℕ]

Full source

/-- Linear isomorphism between `R[X]` and `R[ℕ]`. This is just an
implementation detail, but it can be useful to transfer results from `Finsupp` to polynomials. -/
@[simps!]
def toFinsuppIsoLinear : R[X]R[X] ≃ₗ[R] R[ℕ] where
  __ := toFinsuppIso R
  map_smul' _ _ := rfl

Linear isomorphism between polynomial ring and additive monoid algebra

Informal description

The linear isomorphism between the polynomial ring $R[X]$ and the additive monoid algebra $R[\mathbb{N}]$ over the semiring $R$, which preserves the $R$-module structure. Specifically: - The forward map sends a polynomial $p \in R[X]$ to its representation as a finitely supported function $\mathbb{N} \to R$ - The inverse map reconstructs a polynomial from such a representation - The isomorphism preserves both the additive structure and scalar multiplication by elements of $R$ This isomorphism is primarily an implementation detail for transferring results between polynomial and monoid algebra representations.

Polynomial.ofFinsupp_sum theorem

{ι : Type*} (s : Finset ι) (f : ι → R[ℕ]) : (⟨∑ i ∈ s, f i⟩ : R[X]) = ∑ i ∈ s, ⟨f i⟩

Full source

theorem ofFinsupp_sum {ι : Type*} (s : Finset ι) (f : ι → R[ℕ]) :
    (⟨∑ i ∈ s, f i⟩ : R[X]) = ∑ i ∈ s, ⟨f i⟩ :=
  map_sum (toFinsuppIso R).symm f s

Linearity of Polynomial Construction from Additive Monoid Algebra Sums

Informal description

For any finite set $s$ of indices of type $\iota$ and any family of elements $f : \iota \to R[\mathbb{N}]$ in the additive monoid algebra, the polynomial constructed from the sum $\sum_{i \in s} f(i)$ is equal to the sum of the polynomials constructed from each $f(i)$. That is, $$\left\langle \sum_{i \in s} f(i) \right\rangle = \sum_{i \in s} \langle f(i) \rangle$$ where $\langle \cdot \rangle$ denotes the conversion from $R[\mathbb{N}]$ to $R[X]$.

Polynomial.toFinsupp_sum theorem

{ι : Type*} (s : Finset ι) (f : ι → R[X]) : (∑ i ∈ s, f i : R[X]).toFinsupp = ∑ i ∈ s, (f i).toFinsupp

Full source

theorem toFinsupp_sum {ι : Type*} (s : Finset ι) (f : ι → R[X]) :
    (∑ i ∈ s, f i : R[X]).toFinsupp = ∑ i ∈ s, (f i).toFinsupp :=
  map_sum (toFinsuppIso R) f s

Sum Preservation under Polynomial-to-Monoid-Algebra Conversion

Informal description

For any finite set $s$ of indices and any family of polynomials $(f_i)_{i \in s}$ in $R[X]$, the conversion of the sum $\sum_{i \in s} f_i$ to the additive monoid algebra $R[\mathbb{N}]$ equals the sum of the conversions of each $f_i$ to $R[\mathbb{N}]$. In other words, the map `toFinsupp` from $R[X]$ to $R[\mathbb{N}]$ preserves finite sums.

Polynomial.support definition

: R[X] → Finset ℕ

Full source

/-- The set of all `n` such that `X^n` has a non-zero coefficient. -/
def support : R[X] → Finset ℕ
  | ⟨p⟩ => p.support

Support of a polynomial

Informal description

For a polynomial $ p \in R[X] $, the support of $ p $ is the finite set of all natural numbers $ n $ such that the coefficient of $ X^n $ in $ p $ is nonzero. In other words, it is the set of exponents $ n $ for which the monomial $ a_n X^n $ appears in $ p $ with $ a_n \neq 0 $.

Polynomial.support_ofFinsupp theorem

(p) : support (⟨p⟩ : R[X]) = p.support

Full source

@[simp]
theorem support_ofFinsupp (p) : support (⟨p⟩ : R[X]) = p.support := by rw [support]

Support Preservation in Polynomial Construction from Additive Monoid Algebra

Informal description

For any element $p$ of the additive monoid algebra $R[\mathbb{N}]$, the support of the polynomial $\langle p \rangle \in R[X]$ (constructed from $p$) is equal to the support of $p$ itself. In other words, the exponents with nonzero coefficients are preserved under the conversion from $R[\mathbb{N}]$ to $R[X]$.

Polynomial.support_toFinsupp theorem

(p : R[X]) : p.toFinsupp.support = p.support

Full source

theorem support_toFinsupp (p : R[X]) : p.toFinsupp.support = p.support := by rw [support]

Support Preservation in Polynomial-to-AddMonoidAlgebra Conversion

Informal description

For any polynomial $p \in R[X]$, the support of $p$ (viewed as an element of the additive monoid algebra $R[\mathbb{N}]$) is equal to the support of $p$ in the polynomial ring $R[X]$. That is, the set of exponents with nonzero coefficients remains unchanged when converting between these representations.

Polynomial.support_zero theorem

: (0 : R[X]).support = ∅

Full source

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

Support of Zero Polynomial is Empty

Informal description

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

Polynomial.support_eq_empty theorem

: p.support = ∅ ↔ p = 0

Full source

@[simp]
theorem support_eq_empty : p.support = ∅ ↔ p = 0 := by
  rcases p with ⟨⟩
  simp [support]

Support of Polynomial is Empty if and only if Zero Polynomial

Informal description

For a polynomial $p \in R[X]$, the support of $p$ is empty if and only if $p$ is the zero polynomial. That is, $p$ has no nonzero coefficients if and only if $p = 0$.

Polynomial.support_nonempty theorem

: p.support.Nonempty ↔ p ≠ 0

Full source

@[simp] lemma support_nonempty : p.support.Nonempty ↔ p ≠ 0 :=
  Finset.nonempty_iff_ne_empty.trans support_eq_empty.not

Nonempty Support Characterizes Nonzero Polynomials

Informal description

For a polynomial $p \in R[X]$, the support of $p$ is nonempty if and only if $p$ is not the zero polynomial. In other words, $p$ has at least one nonzero coefficient if and only if $p \neq 0$.

Polynomial.card_support_eq_zero theorem

: #p.support = 0 ↔ p = 0

Full source

theorem card_support_eq_zero : #p.support#p.support = 0 ↔ p = 0 := by simp

Zero Cardinality of Support Characterizes the Zero Polynomial

Informal description

For a polynomial $p \in R[X]$, the cardinality of its support (the set of exponents with nonzero coefficients) is zero if and only if $p$ is the zero polynomial. In other words, $\#\text{support}(p) = 0 \leftrightarrow p = 0$.

Polynomial.monomial definition

(n : ℕ) : R →ₗ[R] R[X]

Full source

/-- `monomial s a` is the monomial `a * X^s` -/
def monomial (n : ℕ) : R →ₗ[R] R[X] where
  toFun t := ⟨Finsupp.single n t⟩
  -- Porting note (https://github.com/leanprover-community/mathlib4/issues/10745): was `simp`.
  map_add' x y := by simp; rw [ofFinsupp_add]
  -- Porting note (https://github.com/leanprover-community/mathlib4/issues/10745): was `simp [← ofFinsupp_smul]`.
  map_smul' r x := by simp; rw [← ofFinsupp_smul, smul_single']

Monomial in polynomial ring

Informal description

The function `monomial n` maps a coefficient $a \in R$ to the monomial $a X^n$ in the polynomial ring $R[X]$, where $X$ is the polynomial variable. This function is an $R$-linear map from $R$ to $R[X]$.

Polynomial.toFinsupp_monomial theorem

(n : ℕ) (r : R) : (monomial n r).toFinsupp = Finsupp.single n r

Full source

@[simp]
theorem toFinsupp_monomial (n : ℕ) (r : R) : (monomial n r).toFinsupp = Finsupp.single n r := by
  simp [monomial]

Monomial-to-Finsupp Conversion: $rX^n \mapsto \text{single}(n, r)$

Informal description

For any natural number $n$ and coefficient $r$ in a semiring $R$, the conversion of the monomial $r X^n$ to its additive monoid algebra representation yields the finitely supported function that is $r$ at $n$ and zero elsewhere. In other words, the underlying representation of the monomial $\text{monomial}(n)(r)$ as a finitely supported function is $\text{single}(n, r)$.

Polynomial.ofFinsupp_single theorem

(n : ℕ) (r : R) : (⟨Finsupp.single n r⟩ : R[X]) = monomial n r

Full source

@[simp]
theorem ofFinsupp_single (n : ℕ) (r : R) : (⟨Finsupp.single n r⟩ : R[X]) = monomial n r := by
  simp [monomial]

Equivalence between single-term finitely supported function and monomial in $R[X]$

Informal description

For any natural number $n$ and coefficient $r$ in a semiring $R$, the polynomial constructed from the finitely supported function `Finsupp.single n r` is equal to the monomial $r X^n$ in the polynomial ring $R[X]$.

Polynomial.monomial_zero_right theorem

(n : ℕ) : monomial n (0 : R) = 0

Full source

@[simp]
theorem monomial_zero_right (n : ℕ) : monomial n (0 : R) = 0 :=
  (monomial n).map_zero

Monomial with Zero Coefficient is Zero Polynomial

Informal description

For any natural number $n$, the monomial $0 X^n$ in the polynomial ring $R[X]$ is equal to the zero polynomial.

Polynomial.monomial_zero_one theorem

: monomial 0 (1 : R) = 1

Full source

theorem monomial_zero_one : monomial 0 (1 : R) = 1 :=
  rfl

Monomial Identity: $1 \cdot X^0 = 1$

Informal description

The monomial with degree 0 and coefficient 1 in the polynomial ring $R[X]$ is equal to the multiplicative identity polynomial, i.e., $1 \cdot X^0 = 1$.

Polynomial.monomial_add theorem

(n : ℕ) (r s : R) : monomial n (r + s) = monomial n r + monomial n s

Full source

theorem monomial_add (n : ℕ) (r s : R) : monomial n (r + s) = monomial n r + monomial n s :=
  (monomial n).map_add _ _

Additivity of Monomial Construction: $(r + s)X^n = rX^n + sX^n$

Informal description

For any natural number $n$ and elements $r, s$ in a semiring $R$, the monomial $(r + s)X^n$ is equal to the sum of the monomials $rX^n$ and $sX^n$ in the polynomial ring $R[X]$. That is, $$(r + s)X^n = rX^n + sX^n.$$

Polynomial.monomial_mul_monomial theorem

(n m : ℕ) (r s : R) : monomial n r * monomial m s = monomial (n + m) (r * s)

Full source

theorem monomial_mul_monomial (n m : ℕ) (r s : R) :
    monomial n r * monomial m s = monomial (n + m) (r * s) :=
  toFinsupp_injective <| by
    simp only [toFinsupp_monomial, toFinsupp_mul, AddMonoidAlgebra.single_mul_single]

Monomial Multiplication Rule: $(rX^n)(sX^m) = (r s)X^{n+m}$

Informal description

For any natural numbers $n, m$ and elements $r, s$ in a semiring $R$, the product of the monomials $rX^n$ and $sX^m$ in the polynomial ring $R[X]$ is equal to the monomial $(r \cdot s)X^{n+m}$. In mathematical notation: $$(rX^n) \cdot (sX^m) = (r \cdot s)X^{n+m}.$$

Polynomial.monomial_pow theorem

(n : ℕ) (r : R) (k : ℕ) : monomial n r ^ k = monomial (n * k) (r ^ k)

Full source

@[simp]
theorem monomial_pow (n : ℕ) (r : R) (k : ℕ) : monomial n r ^ k = monomial (n * k) (r ^ k) := by
  induction k with
  | zero => simp [pow_zero, monomial_zero_one]
  | succ k ih => simp [pow_succ, ih, monomial_mul_monomial, mul_add, add_comm]

Power of Monomial Formula: $(rX^n)^k = r^kX^{n \cdot k}$

Informal description

For any natural number $n$, element $r$ in a semiring $R$, and natural number $k$, the $k$-th power of the monomial $rX^n$ in the polynomial ring $R[X]$ equals the monomial $r^kX^{n \cdot k}$. In mathematical notation: $$(rX^n)^k = r^kX^{n \cdot k}.$$

Polynomial.smul_monomial theorem

{S} [SMulZeroClass S R] (a : S) (n : ℕ) (b : R) : a • monomial n b = monomial n (a • b)

Full source

theorem smul_monomial {S} [SMulZeroClass S R] (a : S) (n : ℕ) (b : R) :
    a • monomial n b = monomial n (a • b) :=
  toFinsupp_injective <| AddMonoidAlgebra.smul_single _ _ _

Scalar multiplication distributes over monomials: $a \cdot (b X^n) = (a \cdot b) X^n$

Informal description

Let $R$ be a semiring and $S$ be a type with a scalar multiplication action on $R$ that preserves zero. For any scalar $a \in S$, natural number $n \in \mathbb{N}$, and coefficient $b \in R$, the scalar multiple $a \cdot (b X^n)$ is equal to $(a \cdot b) X^n$ in the polynomial ring $R[X]$. In mathematical notation: $$a \cdot (b X^n) = (a \cdot b) X^n.$$

Polynomial.monomial_injective theorem

(n : ℕ) : Function.Injective (monomial n : R → R[X])

Full source

theorem monomial_injective (n : ℕ) : Function.Injective (monomial n : R → R[X]) :=
  (toFinsuppIso R).symm.injective.comp (single_injective n)

Injectivity of the Monomial Map in Polynomial Rings

Informal description

For any natural number $n$, the function $\text{monomial}_n : R \to R[X]$, which maps a coefficient $a \in R$ to the monomial $a X^n$, is injective. That is, for any $a, b \in R$, if $\text{monomial}_n(a) = \text{monomial}_n(b)$, then $a = b$.

Polynomial.monomial_eq_zero_iff theorem

(t : R) (n : ℕ) : monomial n t = 0 ↔ t = 0

Full source

@[simp]
theorem monomial_eq_zero_iff (t : R) (n : ℕ) : monomialmonomial n t = 0 ↔ t = 0 :=
  LinearMap.map_eq_zero_iff _ (Polynomial.monomial_injective n)

Monomial is Zero if and only if Coefficient is Zero

Informal description

For any coefficient $t \in R$ and natural number $n \in \mathbb{N}$, the monomial $t X^n$ in the polynomial ring $R[X]$ is equal to the zero polynomial if and only if $t = 0$.

Polynomial.monomial_eq_monomial_iff theorem

{m n : ℕ} {a b : R} : monomial m a = monomial n b ↔ m = n ∧ a = b ∨ a = 0 ∧ b = 0

Full source

theorem monomial_eq_monomial_iff {m n : ℕ} {a b : R} :
    monomialmonomial m a = monomial n b ↔ m = n ∧ a = b ∨ a = 0 ∧ b = 0 := by
  rw [← toFinsupp_inj, toFinsupp_monomial, toFinsupp_monomial, Finsupp.single_eq_single_iff]

Monomial Equality Criterion: $aX^m = bX^n \iff (m=n \land a=b) \lor (a=0 \land b=0)$

Informal description

For any natural numbers $m, n$ and coefficients $a, b$ in a semiring $R$, the monomials $a X^m$ and $b X^n$ are equal if and only if either: 1. $m = n$ and $a = b$, or 2. $a = 0$ and $b = 0$.

Polynomial.support_add theorem

: (p + q).support ⊆ p.support ∪ q.support

Full source

theorem support_add : (p + q).support ⊆ p.support ∪ q.support := by
  simpa [support] using Finsupp.support_add

Support of Sum of Polynomials is Contained in Union of Supports

Informal description

For any two polynomials $p, q \in R[X]$ over a semiring $R$, the support of their sum $p + q$ is contained in the union of their individual supports, i.e., $$\operatorname{supp}(p + q) \subseteq \operatorname{supp}(p) \cup \operatorname{supp}(q).$$

Polynomial.C definition

: R →+* R[X]

Full source

/-- `C a` is the constant polynomial `a`.
`C` is provided as a ring homomorphism.
-/
def C : R →+* R[X] :=
  { monomial 0 with
    map_one' := by simp [monomial_zero_one]
    map_mul' := by simp [monomial_mul_monomial]
    map_zero' := by simp }

Constant polynomial ring homomorphism

Informal description

The function `C` maps an element $a \in R$ to the constant polynomial $a$ in the polynomial ring $R[X]$. This function is a ring homomorphism from $R$ to $R[X]$, meaning it preserves addition, multiplication, and multiplicative identity: - $C(a + b) = C(a) + C(b)$ - $C(a \cdot b) = C(a) \cdot C(b)$ - $C(1) = 1$

Polynomial.monomial_zero_left theorem

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

Full source

@[simp]
theorem monomial_zero_left (a : R) : monomial 0 a = C a :=
  rfl

Monomial at Degree Zero Equals Constant Polynomial

Informal description

For any coefficient $a$ in a semiring $R$, the monomial $a X^0$ is equal to the constant polynomial $C(a)$, i.e., $\text{monomial}(0, a) = C(a)$.

Polynomial.toFinsupp_C theorem

(a : R) : (C a).toFinsupp = single 0 a

Full source

@[simp]
theorem toFinsupp_C (a : R) : (C a).toFinsupp = single 0 a :=
  rfl

Constant Polynomial Representation in Additive Monoid Algebra: $(C(a)).\text{toFinsupp} = \text{single}(0, a)$

Informal description

For any element $a$ in a semiring $R$, the image of the constant polynomial $C(a)$ under the `toFinsupp` map is equal to the additive monoid algebra element `single 0 a`, which is zero everywhere except at degree $0$ where it takes the value $a$. In other words, the formal representation of $C(a)$ as a finitely supported function is $\text{single}(0, a)$.

Polynomial.C_0 theorem

: C (0 : R) = 0

Full source

theorem C_0 : C (0 : R) = 0 := by simp

Constant Polynomial at Zero: $C(0) = 0$

Informal description

The constant polynomial map $C$ evaluated at the zero element $0 \in R$ yields the zero polynomial in $R[X]$, i.e., $C(0) = 0$.

Polynomial.C_1 theorem

: C (1 : R) = 1

Full source

theorem C_1 : C (1 : R) = 1 :=
  rfl

Constant Polynomial Homomorphism Preserves One: $C(1) = 1$

Informal description

The constant polynomial homomorphism $C$ maps the multiplicative identity $1$ of the semiring $R$ to the multiplicative identity $1$ of the polynomial ring $R[X]$, i.e., $C(1) = 1$.

Polynomial.C_mul theorem

: C (a * b) = C a * C b

Full source

theorem C_mul : C (a * b) = C a * C b :=
  C.map_mul a b

Multiplicative Property of Constant Polynomial Homomorphism: $C(a \cdot b) = C(a) \cdot C(b)$

Informal description

For any elements $a, b$ in a semiring $R$, the constant polynomial homomorphism $C$ satisfies $C(a \cdot b) = C(a) \cdot C(b)$ in the polynomial ring $R[X]$.

Polynomial.C_add theorem

: C (a + b) = C a + C b

Full source

theorem C_add : C (a + b) = C a + C b :=
  C.map_add a b

Additivity of the Constant Polynomial Map: $C(a + b) = C(a) + C(b)$

Informal description

For any elements $a, b$ in a semiring $R$, the constant polynomial function $C$ satisfies $C(a + b) = C(a) + C(b)$.

Polynomial.smul_C theorem

{S} [SMulZeroClass S R] (s : S) (r : R) : s • C r = C (s • r)

Full source

@[simp]
theorem smul_C {S} [SMulZeroClass S R] (s : S) (r : R) : s • C r = C (s • r) :=
  smul_monomial _ _ r

Scalar Multiplication Commutes with Constant Polynomial Construction: $s \cdot C(r) = C(s \cdot r)$

Informal description

Let $R$ be a semiring and $S$ be a type with a scalar multiplication action on $R$ that preserves zero. For any scalar $s \in S$ and any element $r \in R$, the scalar multiple $s \cdot C(r)$ of the constant polynomial $C(r)$ is equal to the constant polynomial $C(s \cdot r)$. In mathematical notation: $$s \cdot C(r) = C(s \cdot r).$$

Polynomial.C_pow theorem

: C (a ^ n) = C a ^ n

Full source

theorem C_pow : C (a ^ n) = C a ^ n :=
  C.map_pow a n

Power of Constant Polynomial: $C(a^n) = C(a)^n$

Informal description

For any element $a$ in a semiring $R$ and any natural number $n$, the constant polynomial of $a^n$ is equal to the $n$-th power of the constant polynomial of $a$, i.e., $C(a^n) = (C(a))^n$ in the polynomial ring $R[X]$.

Polynomial.C_eq_natCast theorem

(n : ℕ) : C (n : R) = (n : R[X])

Full source

theorem C_eq_natCast (n : ℕ) : C (n : R) = (n : R[X]) :=
  map_natCast C n

Constant Polynomial Equals Natural Number Cast: $C(n) = n$ in $R[X]$

Informal description

For any natural number $n$ and semiring $R$, the constant polynomial $C(n)$ in $R[X]$ is equal to the canonical embedding of $n$ in $R[X]$, i.e., $C(n) = n$ where $n$ is interpreted as a constant polynomial.

Polynomial.C_mul_monomial theorem

: C a * monomial n b = monomial n (a * b)

Full source

@[simp]
theorem C_mul_monomial : C a * monomial n b = monomial n (a * b) := by
  simp only [← monomial_zero_left, monomial_mul_monomial, zero_add]

Multiplication of Constant Polynomial and Monomial: $C(a) \cdot (bX^n) = (a b)X^n$

Informal description

For any elements $a, b$ in a semiring $R$ and any natural number $n$, the product of the constant polynomial $C(a)$ and the monomial $bX^n$ in the polynomial ring $R[X]$ is equal to the monomial $(a \cdot b)X^n$. In mathematical notation: $$C(a) \cdot (bX^n) = (a \cdot b)X^n.$$

Polynomial.monomial_mul_C theorem

: monomial n a * C b = monomial n (a * b)

Full source

@[simp]
theorem monomial_mul_C : monomial n a * C b = monomial n (a * b) := by
  simp only [← monomial_zero_left, monomial_mul_monomial, add_zero]

Monomial multiplied by constant polynomial: $(aX^n) \cdot b = (a \cdot b)X^n$

Informal description

For any natural number $n$ and elements $a, b$ in a semiring $R$, the product of the monomial $aX^n$ and the constant polynomial $b$ in the polynomial ring $R[X]$ is equal to the monomial $(a \cdot b)X^n$. In mathematical notation: $$(aX^n) \cdot b = (a \cdot b)X^n.$$

Polynomial.X definition

: R[X]

Full source

/-- `X` is the polynomial variable (aka indeterminate). -/
def X : R[X] :=
  monomial 1 1

Polynomial variable $ X $

Informal description

The polynomial variable $ X $ in the polynomial ring $ R[X] $, which is defined as the monomial $ 1 \cdot X^1 $.

Polynomial.monomial_one_one_eq_X theorem

: monomial 1 (1 : R) = X

Full source

theorem monomial_one_one_eq_X : monomial 1 (1 : R) = X :=
  rfl

Monomial Identity: $1 \cdot X^1 = X$

Informal description

The monomial $1 \cdot X^1$ in the polynomial ring $R[X]$ is equal to the polynomial variable $X$.

Polynomial.monomial_one_right_eq_X_pow theorem

(n : ℕ) : monomial n (1 : R) = X ^ n

Full source

theorem monomial_one_right_eq_X_pow (n : ℕ) : monomial n (1 : R) = X ^ n := by
  induction n with
  | zero => simp [monomial_zero_one]
  | succ n ih => rw [pow_succ, ← ih, ← monomial_one_one_eq_X, monomial_mul_monomial, mul_one]

Monomial-Power Identity: $1 \cdot X^n = X^n$

Informal description

For any natural number $n$, the monomial $1 \cdot X^n$ in the polynomial ring $R[X]$ is equal to the $n$-th power of the polynomial variable $X$, i.e., $X^n$.

Polynomial.toFinsupp_X theorem

: X.toFinsupp = Finsupp.single 1 (1 : R)

Full source

@[simp]
theorem toFinsupp_X : X.toFinsupp = Finsupp.single 1 (1 : R) :=
  rfl

Underlying Representation of $X$ as a Single-Term Function

Informal description

The polynomial variable $X$ in the polynomial ring $R[X]$, when converted to its underlying additive monoid algebra representation, corresponds to the finitely supported function that takes the value $1$ at the index $1$ and is zero elsewhere. In other words, the underlying representation of $X$ is the single-term function $\text{single}(1, 1)$.

Polynomial.X_ne_C theorem

[Nontrivial R] (a : R) : X ≠ C a

Full source

theorem X_ne_C [Nontrivial R] (a : R) : XX ≠ C a := by
  intro he
  simpa using monomial_eq_monomial_iff.1 he

Non-Equality of Polynomial Variable and Constant Polynomial: $X \neq C(a)$

Informal description

For any nontrivial semiring $R$ and any element $a \in R$, the polynomial variable $X$ is not equal to the constant polynomial $C(a)$.

Polynomial.X_mul theorem

: X * p = p * X

Full source

/-- `X` commutes with everything, even when the coefficients are noncommutative. -/
theorem X_mul : X * p = p * X := by
  rcases p with ⟨⟩
  simp only [X, ← ofFinsupp_single, ← ofFinsupp_mul, LinearMap.coe_mk, ofFinsupp.injEq]
  ext
  simp [AddMonoidAlgebra.mul_apply, AddMonoidAlgebra.sum_single_index, add_comm]

Commutativity of $X$ with Polynomials: $X \cdot p = p \cdot X$

Informal description

For any polynomial $p$ in the polynomial ring $R[X]$, the product of the polynomial variable $X$ and $p$ is equal to the product of $p$ and $X$, i.e., $X \cdot p = p \cdot X$.

Polynomial.X_pow_mul theorem

{n : ℕ} : X ^ n * p = p * X ^ n

Full source

theorem X_pow_mul {n : ℕ} : X ^ n * p = p * X ^ n := by
  induction n with
  | zero => simp
  | succ n ih =>
    conv_lhs => rw [pow_succ]
    rw [mul_assoc, X_mul, ← mul_assoc, ih, mul_assoc, ← pow_succ]

Commutativity of $X^n$ with Polynomials: $X^n \cdot p = p \cdot X^n$

Informal description

For any natural number $n$ and any polynomial $p$ in the polynomial ring $R[X]$, the product of $X^n$ and $p$ is equal to the product of $p$ and $X^n$, i.e., $X^n \cdot p = p \cdot X^n$.

Polynomial.X_mul_C theorem

(r : R) : X * C r = C r * X

Full source

/-- Prefer putting constants to the left of `X`.

This lemma is the loop-avoiding `simp` version of `Polynomial.X_mul`. -/
@[simp]
theorem X_mul_C (r : R) : X * C r = C r * X :=
  X_mul

Commutativity of $X$ with Constant Polynomials: $X \cdot C(r) = C(r) \cdot X$

Informal description

For any element $r$ in the semiring $R$, the product of the polynomial variable $X$ and the constant polynomial $C(r)$ is equal to the product of $C(r)$ and $X$, i.e., $X \cdot C(r) = C(r) \cdot X$.

Polynomial.X_pow_mul_C theorem

(r : R) (n : ℕ) : X ^ n * C r = C r * X ^ n

Full source

/-- Prefer putting constants to the left of `X ^ n`.

This lemma is the loop-avoiding `simp` version of `X_pow_mul`. -/
@[simp]
theorem X_pow_mul_C (r : R) (n : ℕ) : X ^ n * C r = C r * X ^ n :=
  X_pow_mul

Commutativity of $X^n$ with Constant Polynomials: $X^n \cdot C(r) = C(r) \cdot X^n$

Informal description

For any element $r$ in a semiring $R$ and any natural number $n$, the product of the polynomial $X^n$ and the constant polynomial $C(r)$ is equal to the product of $C(r)$ and $X^n$, i.e., $X^n \cdot C(r) = C(r) \cdot X^n$.

Polynomial.X_pow_mul_assoc theorem

{n : ℕ} : p * X ^ n * q = p * q * X ^ n

Full source

theorem X_pow_mul_assoc {n : ℕ} : p * X ^ n * q = p * q * X ^ n := by
  rw [mul_assoc, X_pow_mul, ← mul_assoc]

Associativity of Polynomial Multiplication with $X^n$: $p \cdot X^n \cdot q = p \cdot q \cdot X^n$

Informal description

For any natural number $n$ and any polynomials $p, q$ in the polynomial ring $R[X]$, the product $p \cdot X^n \cdot q$ is equal to $p \cdot q \cdot X^n$.

Polynomial.X_pow_mul_assoc_C theorem

{n : ℕ} (r : R) : p * X ^ n * C r = p * C r * X ^ n

Full source

/-- Prefer putting constants to the left of `X ^ n`.

This lemma is the loop-avoiding `simp` version of `X_pow_mul_assoc`. -/
@[simp]
theorem X_pow_mul_assoc_C {n : ℕ} (r : R) : p * X ^ n * C r = p * C r * X ^ n :=
  X_pow_mul_assoc

Associativity of polynomial multiplication with $X^n$ and constant $C(r)$: $p \cdot X^n \cdot C(r) = p \cdot C(r) \cdot X^n$

Informal description

For any natural number $n$, any polynomial $p \in R[X]$, and any constant $r \in R$, the product $p \cdot X^n \cdot C(r)$ is equal to $p \cdot C(r) \cdot X^n$.

Polynomial.commute_X theorem

(p : R[X]) : Commute X p

Full source

theorem commute_X (p : R[X]) : Commute X p :=
  X_mul

Commutativity of $X$ with Polynomials: $X \cdot p = p \cdot X$

Informal description

For any polynomial $p$ in the polynomial ring $R[X]$, the polynomial variable $X$ commutes with $p$, i.e., $X \cdot p = p \cdot X$.

Polynomial.commute_X_pow theorem

(p : R[X]) (n : ℕ) : Commute (X ^ n) p

Full source

theorem commute_X_pow (p : R[X]) (n : ℕ) : Commute (X ^ n) p :=
  X_pow_mul

Commutativity of $X^n$ with Polynomials: $X^n \cdot p = p \cdot X^n$

Informal description

For any polynomial $p \in R[X]$ and any natural number $n$, the monomial $X^n$ commutes with $p$, i.e., $X^n \cdot p = p \cdot X^n$.

Polynomial.monomial_mul_X theorem

(n : ℕ) (r : R) : monomial n r * X = monomial (n + 1) r

Full source

@[simp]
theorem monomial_mul_X (n : ℕ) (r : R) : monomial n r * X = monomial (n + 1) r := by
  rw [X, monomial_mul_monomial, mul_one]

Monomial Multiplication by $X$: $(rX^n) \cdot X = rX^{n+1}$

Informal description

For any natural number $n$ and coefficient $r$ in a semiring $R$, the product of the monomial $rX^n$ and the polynomial variable $X$ in the polynomial ring $R[X]$ is equal to the monomial $rX^{n+1}$. In mathematical notation: $$(rX^n) \cdot X = rX^{n+1}.$$

Polynomial.monomial_mul_X_pow theorem

(n : ℕ) (r : R) (k : ℕ) : monomial n r * X ^ k = monomial (n + k) r

Full source

@[simp]
theorem monomial_mul_X_pow (n : ℕ) (r : R) (k : ℕ) :
    monomial n r * X ^ k = monomial (n + k) r := by
  induction k with
  | zero => simp
  | succ k ih => simp [ih, pow_succ, ← mul_assoc, add_assoc]

Monomial Multiplication by $X^k$: $(rX^n) \cdot X^k = rX^{n+k}$

Informal description

For any natural numbers $n, k$ and coefficient $r$ in a semiring $R$, the product of the monomial $rX^n$ and the $k$-th power of the polynomial variable $X$ in the polynomial ring $R[X]$ is equal to the monomial $rX^{n+k}$. In mathematical notation: $$(rX^n) \cdot X^k = rX^{n+k}.$$

Polynomial.X_mul_monomial theorem

(n : ℕ) (r : R) : X * monomial n r = monomial (n + 1) r

Full source

@[simp]
theorem X_mul_monomial (n : ℕ) (r : R) : X * monomial n r = monomial (n + 1) r := by
  rw [X_mul, monomial_mul_X]

Left Multiplication by $X$ on Monomials: $X \cdot (rX^n) = rX^{n+1}$

Informal description

For any natural number $n$ and coefficient $r$ in a semiring $R$, the product of the polynomial variable $X$ and the monomial $rX^n$ in the polynomial ring $R[X]$ is equal to the monomial $rX^{n+1}$. In mathematical notation: $$X \cdot (rX^n) = rX^{n+1}.$$

Polynomial.X_pow_mul_monomial theorem

(k n : ℕ) (r : R) : X ^ k * monomial n r = monomial (n + k) r

Full source

@[simp]
theorem X_pow_mul_monomial (k n : ℕ) (r : R) : X ^ k * monomial n r = monomial (n + k) r := by
  rw [X_pow_mul, monomial_mul_X_pow]

Multiplication of $X^k$ with Monomial: $X^k \cdot (rX^n) = rX^{n+k}$

Informal description

For any natural numbers $k, n$ and coefficient $r$ in a semiring $R$, the product of the $k$-th power of the polynomial variable $X$ and the monomial $rX^n$ in the polynomial ring $R[X]$ is equal to the monomial $rX^{n+k}$. In mathematical notation: $$X^k \cdot (rX^n) = rX^{n+k}.$$

Polynomial.coeff definition

: R[X] → ℕ → R

Full source

/-- `coeff p n` (often denoted `p.coeff n`) is the coefficient of `X^n` in `p`. -/
def coeff : R[X] → ℕ → R
  | ⟨p⟩ => p

Coefficient of a polynomial term

Informal description

The function `coeff p n` (often denoted `p.coeff n`) returns the coefficient of the term `X^n` in the polynomial `p`.

Polynomial.coeff_ofFinsupp theorem

(p) : coeff (⟨p⟩ : R[X]) = p

Full source

@[simp]
theorem coeff_ofFinsupp (p) : coeff (⟨p⟩ : R[X]) = p := by rw [coeff]

Coefficients of Polynomial from Additive Monoid Algebra Match Original Function

Informal description

For any finitely supported function $p \colon \mathbb{N} \to R$ (viewed as an element of the additive monoid algebra $R[\mathbb{N}]$), the coefficients of the polynomial $\langle p \rangle \in R[X]$ obtained by converting $p$ to a polynomial are equal to $p$ itself. In other words, the coefficient of $X^n$ in $\langle p \rangle$ is exactly $p(n)$ for each $n \in \mathbb{N}$.

Polynomial.coeff_injective theorem

: Injective (coeff : R[X] → ℕ → R)

Full source

theorem coeff_injective : Injective (coeff : R[X] → ℕ → R) := by
  rintro ⟨p⟩ ⟨q⟩
  simp only [coeff, DFunLike.coe_fn_eq, imp_self, ofFinsupp.injEq]

Injectivity of Polynomial Coefficient Function

Informal description

The coefficient function $\text{coeff} \colon R[X] \to \mathbb{N} \to R$, which maps a polynomial $p$ to its sequence of coefficients $(p_n)_{n \in \mathbb{N}}$, is injective. That is, if two polynomials $p, q \in R[X]$ satisfy $p_n = q_n$ for all $n \in \mathbb{N}$, then $p = q$.

Polynomial.coeff_inj theorem

: p.coeff = q.coeff ↔ p = q

Full source

@[simp]
theorem coeff_inj : p.coeff = q.coeff ↔ p = q :=
  coeff_injective.eq_iff

Polynomial Equality via Coefficient Equality

Informal description

For any two polynomials $p, q \in R[X]$, their coefficient sequences are equal if and only if the polynomials themselves are equal. That is, $p = q$ if and only if for all $n \in \mathbb{N}$, the coefficient of $X^n$ in $p$ equals the coefficient of $X^n$ in $q$.

Polynomial.toFinsupp_apply theorem

(f : R[X]) (i) : f.toFinsupp i = f.coeff i

Full source

theorem toFinsupp_apply (f : R[X]) (i) : f.toFinsupp i = f.coeff i := by cases f; rfl

Coefficient Correspondence Between Polynomial and Finsupp Representations

Informal description

For any polynomial $f \in R[X]$ and any natural number $i$, the coefficient of $X^i$ in the finitely supported function representation of $f$ is equal to the coefficient of $X^i$ in $f$, i.e., $f.\text{toFinsupp}(i) = f.\text{coeff}(i)$.

Polynomial.coeff_monomial theorem

: coeff (monomial n a) m = if n = m then a else 0

Full source

theorem coeff_monomial : coeff (monomial n a) m = if n = m then a else 0 := by
  simp [coeff, Finsupp.single_apply]

Coefficient Formula for Monomials: $\text{coeff}(aX^n, m) = a \delta_{n,m}$

Informal description

For any natural numbers $n, m$ and any coefficient $a$ in a semiring $R$, the coefficient of $X^m$ in the monomial $a X^n$ is equal to $a$ if $n = m$, and $0$ otherwise. In mathematical notation: $$\text{coeff}(a X^n, m) = \begin{cases} a & \text{if } n = m \\ 0 & \text{otherwise} \end{cases}$$

Polynomial.coeff_monomial_same theorem

(n : ℕ) (c : R) : (monomial n c).coeff n = c

Full source

@[simp]
theorem coeff_monomial_same (n : ℕ) (c : R) : (monomial n c).coeff n = c :=
  Finsupp.single_eq_same

Coefficient of Monomial at Its Own Degree

Informal description

For any natural number $n$ and any coefficient $c$ in a semiring $R$, the coefficient of $X^n$ in the monomial $c X^n$ is equal to $c$, i.e., $(c X^n).\text{coeff}(n) = c$.

Polynomial.coeff_monomial_of_ne theorem

{m n : ℕ} (c : R) (h : n ≠ m) : (monomial n c).coeff m = 0

Full source

theorem coeff_monomial_of_ne {m n : ℕ} (c : R) (h : n ≠ m) : (monomial n c).coeff m = 0 :=
  Finsupp.single_eq_of_ne h

Vanishing of Off-Diagonal Coefficients in Monomials

Informal description

For any natural numbers $m$ and $n$ with $n \neq m$, and any coefficient $c \in R$, the coefficient of $X^m$ in the monomial $c X^n$ is zero, i.e., $(c X^n).\text{coeff}(m) = 0$.

Polynomial.coeff_zero theorem

(n : ℕ) : coeff (0 : R[X]) n = 0

Full source

@[simp]
theorem coeff_zero (n : ℕ) : coeff (0 : R[X]) n = 0 :=
  rfl

Coefficients of the Zero Polynomial are Zero

Informal description

For any natural number $n$, the coefficient of $X^n$ in the zero polynomial $0 \in R[X]$ is $0$.

Polynomial.coeff_one theorem

{n : ℕ} : coeff (1 : R[X]) n = if n = 0 then 1 else 0

Full source

theorem coeff_one {n : ℕ} : coeff (1 : R[X]) n = if n = 0 then 1 else 0 := by
  simp_rw [eq_comm (a := n) (b := 0)]
  exact coeff_monomial

Coefficients of the Constant Polynomial 1: $\text{coeff}(1, n) = \delta_{n,0}$

Informal description

For any natural number $n$, the coefficient of $X^n$ in the constant polynomial $1 \in R[X]$ is $1$ if $n = 0$ and $0$ otherwise. In other words: $$\text{coeff}(1, n) = \begin{cases} 1 & \text{if } n = 0 \\ 0 & \text{otherwise} \end{cases}$$

Polynomial.coeff_one_zero theorem

: coeff (1 : R[X]) 0 = 1

Full source

@[simp]
theorem coeff_one_zero : coeff (1 : R[X]) 0 = 1 := by
  simp [coeff_one]

Constant Term of the Polynomial 1 is 1

Informal description

The coefficient of the constant term (degree 0) in the constant polynomial $1 \in R[X]$ is equal to $1$, i.e., $\text{coeff}(1, 0) = 1$.

Polynomial.coeff_X_one theorem

: coeff (X : R[X]) 1 = 1

Full source

@[simp]
theorem coeff_X_one : coeff (X : R[X]) 1 = 1 :=
  coeff_monomial

Coefficient of $X$ at degree 1 is 1

Informal description

The coefficient of the term $X^1$ in the polynomial $X$ is equal to $1$, i.e., $\text{coeff}(X, 1) = 1$.

Polynomial.coeff_X_zero theorem

: coeff (X : R[X]) 0 = 0

Full source

@[simp]
theorem coeff_X_zero : coeff (X : R[X]) 0 = 0 :=
  coeff_monomial

Vanishing Constant Term in $X$: $\text{coeff}(X, 0) = 0$

Informal description

The coefficient of the term $X^0$ (i.e., the constant term) in the polynomial $X$ is $0$.

Polynomial.coeff_monomial_succ theorem

: coeff (monomial (n + 1) a) 0 = 0

Full source

@[simp]
theorem coeff_monomial_succ : coeff (monomial (n + 1) a) 0 = 0 := by simp [coeff_monomial]

Vanishing Constant Term in Monomials of Degree $\geq 1$

Informal description

For any natural number $n$ and coefficient $a$ in a semiring $R$, the coefficient of $X^0$ in the monomial $a X^{n+1}$ is zero. In other words, $\text{coeff}(a X^{n+1}, 0) = 0$.

Polynomial.coeff_X theorem

: coeff (X : R[X]) n = if 1 = n then 1 else 0

Full source

theorem coeff_X : coeff (X : R[X]) n = if 1 = n then 1 else 0 :=
  coeff_monomial

Coefficient Formula for the Polynomial $X$: $\text{coeff}(X, n) = \delta_{1,n}$

Informal description

For any natural number $n$, the coefficient of $X^n$ in the polynomial $X$ is $1$ if $n = 1$ and $0$ otherwise. In mathematical notation: $$\text{coeff}(X, n) = \begin{cases} 1 & \text{if } n = 1 \\ 0 & \text{otherwise} \end{cases}$$

Polynomial.coeff_X_of_ne_one theorem

{n : ℕ} (hn : n ≠ 1) : coeff (X : R[X]) n = 0

Full source

theorem coeff_X_of_ne_one {n : ℕ} (hn : n ≠ 1) : coeff (X : R[X]) n = 0 := by
  rw [coeff_X, if_neg hn.symm]

Vanishing Coefficients of $X$ for $n \neq 1$

Informal description

For any natural number $n \neq 1$, the coefficient of $X^n$ in the polynomial $X$ is zero, i.e., $\text{coeff}(X, n) = 0$.

Polynomial.mem_support_iff theorem

: n ∈ p.support ↔ p.coeff n ≠ 0

Full source

@[simp]
theorem mem_support_iff : n ∈ p.supportn ∈ p.support ↔ p.coeff n ≠ 0 := by
  rcases p with ⟨⟩
  simp

Characterization of Support Elements in Polynomials: $n \in \text{support}(p) \leftrightarrow p_n \neq 0$

Informal description

For a polynomial $p \in R[X]$ and a natural number $n$, the exponent $n$ belongs to the support of $p$ if and only if the coefficient of $X^n$ in $p$ is nonzero. In other words, $n \in \text{support}(p) \leftrightarrow p_n \neq 0$.

Polynomial.not_mem_support_iff theorem

: n ∉ p.support ↔ p.coeff n = 0

Full source

theorem not_mem_support_iff : n ∉ p.supportn ∉ p.support ↔ p.coeff n = 0 := by simp

Characterization of Non-Support Elements in Polynomials: $n \notin \text{support}(p) \leftrightarrow p_n = 0$

Informal description

For a polynomial $p \in R[X]$ and a natural number $n$, the exponent $n$ is not in the support of $p$ if and only if the coefficient of $X^n$ in $p$ is zero. In other words, $n \notin \text{support}(p) \leftrightarrow p_n = 0$.

Polynomial.coeff_C theorem

: coeff (C a) n = ite (n = 0) a 0

Full source

theorem coeff_C : coeff (C a) n = ite (n = 0) a 0 := by
  convert coeff_monomial (a := a) (m := n) (n := 0) using 2
  simp [eq_comm]

Coefficient Formula for Constant Polynomials: $\text{coeff}(C(a), n) = a \delta_{n,0}$

Informal description

For any element $a$ in a semiring $R$ and any natural number $n$, the coefficient of $X^n$ in the constant polynomial $C(a)$ is equal to $a$ if $n = 0$, and $0$ otherwise. In mathematical notation: $$\text{coeff}(C(a), n) = \begin{cases} a & \text{if } n = 0 \\ 0 & \text{otherwise} \end{cases}$$

Polynomial.coeff_C_zero theorem

: coeff (C a) 0 = a

Full source

@[simp]
theorem coeff_C_zero : coeff (C a) 0 = a :=
  coeff_monomial

Coefficient of Constant Term in Constant Polynomial: $\text{coeff}(C(a), 0) = a$

Informal description

For any element $a$ in a semiring $R$, the coefficient of $X^0$ in the constant polynomial $C(a)$ is equal to $a$, i.e., $\text{coeff}(C(a), 0) = a$.

Polynomial.coeff_C_ne_zero theorem

(h : n ≠ 0) : (C a).coeff n = 0

Full source

theorem coeff_C_ne_zero (h : n ≠ 0) : (C a).coeff n = 0 := by rw [coeff_C, if_neg h]

Vanishing of Higher Coefficients in Constant Polynomials: $\text{coeff}(C(a), n) = 0$ for $n \neq 0$

Informal description

For any element $a$ in a semiring $R$ and any natural number $n \neq 0$, the coefficient of $X^n$ in the constant polynomial $C(a)$ is zero. In mathematical notation: $$\text{coeff}(C(a), n) = 0 \quad \text{for all } n \neq 0$$

Polynomial.coeff_C_succ theorem

{r : R} {n : ℕ} : coeff (C r) (n + 1) = 0

Full source

@[simp]
lemma coeff_C_succ {r : R} {n : ℕ} : coeff (C r) (n + 1) = 0 := by simp [coeff_C]

Vanishing of Higher Coefficients in Constant Polynomials: $\text{coeff}(C(r), n+1) = 0$

Informal description

For any element $r$ in a semiring $R$ and any natural number $n$, the coefficient of $X^{n+1}$ in the constant polynomial $C(r)$ is equal to $0$. In mathematical notation: $$\text{coeff}(C(r), n+1) = 0$$

Polynomial.coeff_natCast_ite theorem

: (Nat.cast m : R[X]).coeff n = ite (n = 0) m 0

Full source

@[simp]
theorem coeff_natCast_ite : (Nat.cast m : R[X]).coeff n = ite (n = 0) m 0 := by
  simp only [← C_eq_natCast, coeff_C, Nat.cast_ite, Nat.cast_zero]

Coefficient Formula for Constant Polynomials: $\text{coeff}(m, n) = m \delta_{n,0}$

Informal description

For any natural number $m$ and any index $n$, the coefficient of $X^n$ in the constant polynomial $m \in R[X]$ is equal to $m$ if $n = 0$, and $0$ otherwise. In mathematical notation: $$\text{coeff}(m, n) = \begin{cases} m & \text{if } n = 0 \\ 0 & \text{otherwise} \end{cases}$$

Polynomial.coeff_ofNat_zero theorem

(a : ℕ) [a.AtLeastTwo] : coeff (ofNat(a) : R[X]) 0 = ofNat(a)

Full source

@[simp]
theorem coeff_ofNat_zero (a : ℕ) [a.AtLeastTwo] :
    coeff (ofNat(a) : R[X]) 0 = ofNat(a) :=
  coeff_monomial

Coefficient of $X^0$ in Constant Polynomial $a$ is $a$ (for $a \geq 2$)

Informal description

For any natural number $a \geq 2$ interpreted as a constant polynomial in $R[X]$, the coefficient of $X^0$ is equal to $a$ itself. In mathematical notation: $$\text{coeff}(a, 0) = a$$ where $a$ is treated as the constant polynomial $a \cdot X^0$ in $R[X]$.

Polynomial.coeff_ofNat_succ theorem

(a n : ℕ) [h : a.AtLeastTwo] : coeff (ofNat(a) : R[X]) (n + 1) = 0

Full source

@[simp]
theorem coeff_ofNat_succ (a n : ℕ) [h : a.AtLeastTwo] :
    coeff (ofNat(a) : R[X]) (n + 1) = 0 := by
  rw [← Nat.cast_ofNat]
  simp [-Nat.cast_ofNat]

Vanishing of Higher Coefficients in Constant Polynomials: $\text{coeff}(a, n+1) = 0$ for $a \geq 2$

Informal description

For any natural numbers $a \geq 2$ and $n$, the coefficient of $X^{n+1}$ in the constant polynomial $a \in R[X]$ is zero. In mathematical notation: $$\text{coeff}(a, n+1) = 0$$ where $a$ is treated as the constant polynomial $a \cdot X^0$ in $R[X]$.

Polynomial.C_mul_X_pow_eq_monomial theorem

: ∀ {n : ℕ}, C a * X ^ n = monomial n a

Full source

theorem C_mul_X_pow_eq_monomial : ∀ {n : ℕ}, C a * X ^ n = monomial n a
  | 0 => mul_one _
  | n + 1 => by
    rw [pow_succ, ← mul_assoc, C_mul_X_pow_eq_monomial, X, monomial_mul_monomial, mul_one]

Monomial Representation: $a \cdot X^n = a X^n$

Informal description

For any natural number $n$ and element $a$ in a semiring $R$, the product of the constant polynomial $a$ and the $n$-th power of the polynomial variable $X$ in the polynomial ring $R[X]$ is equal to the monomial $a X^n$. In mathematical notation: $$a \cdot X^n = a X^n.$$

Polynomial.toFinsupp_C_mul_X_pow theorem

(a : R) (n : ℕ) : Polynomial.toFinsupp (C a * X ^ n) = Finsupp.single n a

Full source

@[simp high]
theorem toFinsupp_C_mul_X_pow (a : R) (n : ℕ) :
    Polynomial.toFinsupp (C a * X ^ n) = Finsupp.single n a := by
  rw [C_mul_X_pow_eq_monomial, toFinsupp_monomial]

Conversion of $a X^n$ to Finsupp Representation: $(a X^n).\text{toFinsupp} = \text{single}(n, a)$

Informal description

For any element $a$ in a semiring $R$ and any natural number $n$, the conversion of the polynomial $a \cdot X^n$ to its additive monoid algebra representation is the finitely supported function that takes the value $a$ at $n$ and zero elsewhere. In other words, the underlying representation of $a \cdot X^n$ is the single term $\text{single}(n, a)$. Mathematically, this can be written as: $$(a X^n).\text{toFinsupp} = \text{single}(n, a).$$

Polynomial.C_mul_X_eq_monomial theorem

: C a * X = monomial 1 a

Full source

theorem C_mul_X_eq_monomial : C a * X = monomial 1 a := by rw [← C_mul_X_pow_eq_monomial, pow_one]

Monomial Representation: $a \cdot X = a X^1$

Informal description

For any element $a$ in a semiring $R$, the product of the constant polynomial $a$ and the polynomial variable $X$ in the polynomial ring $R[X]$ is equal to the monomial $a X^1$. In mathematical notation: $$a \cdot X = a X^1.$$

Polynomial.toFinsupp_C_mul_X theorem

(a : R) : Polynomial.toFinsupp (C a * X) = Finsupp.single 1 a

Full source

@[simp high]
theorem toFinsupp_C_mul_X (a : R) : Polynomial.toFinsupp (C a * X) = Finsupp.single 1 a := by
  rw [C_mul_X_eq_monomial, toFinsupp_monomial]

Conversion of Linear Term $aX$ to Finsupp Representation: $(aX) \mapsto \text{single}(1, a)$

Informal description

For any element $a$ in a semiring $R$, the conversion of the polynomial $a \cdot X$ to its additive monoid algebra representation is the finitely supported function that takes the value $a$ at $1$ and zero elsewhere. In other words, the underlying representation of $a \cdot X$ is the single term $\text{single}(1, a)$. Mathematically, this can be written as: $$(a X).\text{toFinsupp} = \text{single}(1, a).$$

Polynomial.C_injective theorem

: Injective (C : R → R[X])

Full source

theorem C_injective : Injective (C : R → R[X]) :=
  monomial_injective 0

Injectivity of the Constant Polynomial Map

Informal description

The constant polynomial map $C : R \to R[X]$, which sends an element $a \in R$ to the constant polynomial $a$, is injective. That is, for any $a, b \in R$, if $C(a) = C(b)$, then $a = b$.

Polynomial.C_inj theorem

: C a = C b ↔ a = b

Full source

@[simp]
theorem C_inj : CC a = C b ↔ a = b :=
  C_injective.eq_iff

Injectivity of Constant Polynomial Construction: $C(a) = C(b) \leftrightarrow a = b$

Informal description

For any elements $a, b$ in a semiring $R$, the constant polynomials $C(a)$ and $C(b)$ in $R[X]$ are equal if and only if $a = b$.

Polynomial.C_eq_zero theorem

: C a = 0 ↔ a = 0

Full source

@[simp]
theorem C_eq_zero : CC a = 0 ↔ a = 0 :=
  C_injective.eq_iff' (map_zero C)

Zero Constant Polynomial Characterization: $C(a) = 0 \leftrightarrow a = 0$

Informal description

For any element $a$ in a semiring $R$, the constant polynomial $C(a)$ is equal to the zero polynomial if and only if $a$ is equal to zero in $R$, i.e., $C(a) = 0 \leftrightarrow a = 0$.

Polynomial.C_ne_zero theorem

: C a ≠ 0 ↔ a ≠ 0

Full source

theorem C_ne_zero : CC a ≠ 0C a ≠ 0 ↔ a ≠ 0 :=
  C_eq_zero.not

Nonzero Constant Polynomial Characterization: $C(a) \neq 0 \leftrightarrow a \neq 0$

Informal description

For any element $a$ in a semiring $R$, the constant polynomial $C(a)$ is nonzero if and only if $a$ is nonzero, i.e., $C(a) \neq 0 \leftrightarrow a \neq 0$.

Polynomial.subsingleton_iff_subsingleton theorem

: Subsingleton R[X] ↔ Subsingleton R

Full source

theorem subsingleton_iff_subsingleton : SubsingletonSubsingleton R[X] ↔ Subsingleton R :=
  ⟨@Injective.subsingleton _ _ _ C_injective, by
    intro
    infer_instance⟩

Subsingleton Property of Polynomial Ring $R[X]$ if and only if $R$ is Subsingleton

Informal description

The polynomial ring $R[X]$ is a subsingleton (i.e., has at most one element) if and only if the semiring $R$ is a subsingleton.

Polynomial.Nontrivial.of_polynomial_ne theorem

(h : p ≠ q) : Nontrivial R

Full source

theorem Nontrivial.of_polynomial_ne (h : p ≠ q) : Nontrivial R :=
  (subsingleton_or_nontrivial R).resolve_left fun _hI => h <| Subsingleton.elim _ _

Nontriviality of Semiring from Distinct Polynomials

Informal description

If two polynomials $p$ and $q$ in $R[X]$ are distinct, then the semiring $R$ is nontrivial (i.e., contains at least two distinct elements).

Polynomial.forall_eq_iff_forall_eq theorem

: (∀ f g : R[X], f = g) ↔ ∀ a b : R, a = b

Full source

theorem forall_eq_iff_forall_eq : (∀ f g : R[X], f = g) ↔ ∀ a b : R, a = b := by
  simpa only [← subsingleton_iff] using subsingleton_iff_subsingleton

Triviality of Polynomial Ring $R[X]$ if and only if $R$ is Trivial

Informal description

For any semiring $R$, all polynomials in $R[X]$ are equal if and only if all elements of $R$ are equal. In other words, the polynomial ring $R[X]$ is trivial (contains only one polynomial) precisely when the semiring $R$ is trivial (contains only one element).

Polynomial.ext_iff theorem

{p q : R[X]} : p = q ↔ ∀ n, coeff p n = coeff q n

Full source

theorem ext_iff {p q : R[X]} : p = q ↔ ∀ n, coeff p n = coeff q n := by
  rcases p with ⟨f : ℕℕ →₀ R⟩
  rcases q with ⟨g : ℕℕ →₀ R⟩
  simpa [coeff] using DFunLike.ext_iff (f := f) (g := g)

Polynomial Equality via Coefficient Equality

Informal description

Two polynomials $p$ and $q$ in $R[X]$ are equal if and only if their corresponding coefficients are equal for every natural number $n$, i.e., $p = q \leftrightarrow \forall n \in \mathbb{N}, \text{coeff}(p, n) = \text{coeff}(q, n)$.

Polynomial.ext theorem

{p q : R[X]} : (∀ n, coeff p n = coeff q n) → p = q

Full source

@[ext]
theorem ext {p q : R[X]} : (∀ n, coeff p n = coeff q n) → p = q :=
  ext_iff.2

Polynomial Equality via Coefficient Equality

Informal description

For any two polynomials $p, q \in R[X]$, if their corresponding coefficients are equal for every natural number $n$ (i.e., $\text{coeff}(p, n) = \text{coeff}(q, n)$ for all $n \in \mathbb{N}$), then $p = q$.

Polynomial.addSubmonoid_closure_setOf_eq_monomial theorem

: AddSubmonoid.closure {p : R[X] | ∃ n a, p = monomial n a} = ⊤

Full source

/-- Monomials generate the additive monoid of polynomials. -/
theorem addSubmonoid_closure_setOf_eq_monomial :
    AddSubmonoid.closure { p : R[X] | ∃ n a, p = monomial n a } = ⊤ := by
  apply top_unique
  rw [← AddSubmonoid.map_equiv_top (toFinsuppIso R).symm.toAddEquiv, ←
    Finsupp.add_closure_setOf_eq_single, AddMonoidHom.map_mclosure]
  refine AddSubmonoid.closure_mono (Set.image_subset_iff.2 ?_)
  rintro _ ⟨n, a, rfl⟩
  exact ⟨n, a, Polynomial.ofFinsupp_single _ _⟩

Monomials generate the additive structure of the polynomial ring $R[X]$

Informal description

The additive submonoid generated by the set of all monomials $\{aX^n \mid n \in \mathbb{N}, a \in R\}$ in the polynomial ring $R[X]$ is equal to the entire ring $R[X]$. In other words, every polynomial can be expressed as a finite sum of monomials.

Polynomial.addHom_ext theorem

{M : Type*} [AddZeroClass M] {f g : R[X] →+ M} (h : ∀ n a, f (monomial n a) = g (monomial n a)) : f = g

Full source

theorem addHom_ext {M : Type*} [AddZeroClass M] {f g : R[X]R[X] →+ M}
    (h : ∀ n a, f (monomial n a) = g (monomial n a)) : f = g :=
  AddMonoidHom.eq_of_eqOn_denseM addSubmonoid_closure_setOf_eq_monomial <| by
    rintro p ⟨n, a, rfl⟩
    exact h n a

Uniqueness of additive monoid homomorphisms on polynomials via monomial agreement

Informal description

Let $R$ be a semiring and $M$ be an additive monoid. For any two additive monoid homomorphisms $f, g \colon R[X] \to M$, if $f(aX^n) = g(aX^n)$ for all $n \in \mathbb{N}$ and $a \in R$, then $f = g$.

Polynomial.addHom_ext' theorem

 {M : Type*} [AddZeroClass M] {f g : R[X] →+ M}
  (h : ∀ n, f.comp (monomial n).toAddMonoidHom = g.comp (monomial n).toAddMonoidHom) : f = g

Full source

@[ext high]
theorem addHom_ext' {M : Type*} [AddZeroClass M] {f g : R[X]R[X] →+ M}
    (h : ∀ n, f.comp (monomial n).toAddMonoidHom = g.comp (monomial n).toAddMonoidHom) : f = g :=
  addHom_ext fun n => DFunLike.congr_fun (h n)

Uniqueness of additive monoid homomorphisms on polynomials via composition with monomial maps

Informal description

Let $R$ be a semiring and $M$ be an additive monoid. For any two additive monoid homomorphisms $f, g \colon R[X] \to M$, if for every natural number $n$ the compositions $f \circ \varphi_n$ and $g \circ \varphi_n$ are equal (where $\varphi_n$ is the additive monoid homomorphism sending $a \in R$ to the monomial $aX^n$), then $f = g$.

Polynomial.lhom_ext' theorem

 {M : Type*} [AddCommMonoid M] [Module R M] {f g : R[X] →ₗ[R] M} (h : ∀ n, f.comp (monomial n) = g.comp (monomial n)) :
  f = g

Full source

@[ext high]
theorem lhom_ext' {M : Type*} [AddCommMonoid M] [Module R M] {f g : R[X]R[X] →ₗ[R] M}
    (h : ∀ n, f.comp (monomial n) = g.comp (monomial n)) : f = g :=
  LinearMap.toAddMonoidHom_injective <| addHom_ext fun n => LinearMap.congr_fun (h n)

Uniqueness of Linear Maps on Polynomials via Monomial Agreement

Informal description

Let $R$ be a semiring and $M$ be an $R$-module. For any two $R$-linear maps $f, g \colon R[X] \to M$, if $f \circ \text{monomial}(n) = g \circ \text{monomial}(n)$ for all $n \in \mathbb{N}$, then $f = g$.

Polynomial.support_monomial theorem

(n) {a : R} (H : a ≠ 0) : (monomial n a).support = singleton n

Full source

theorem support_monomial (n) {a : R} (H : a ≠ 0) : (monomial n a).support = singleton n := by
  rw [← ofFinsupp_single, support]; exact Finsupp.support_single_ne_zero _ H

Support of Monomial $a X^n$ is $\{n\}$ for $a \neq 0$

Informal description

For any natural number $n$ and nonzero element $a$ in a semiring $R$, the support of the monomial $a X^n$ is the singleton set $\{n\}$.

Polynomial.support_monomial' theorem

(n) (a : R) : (monomial n a).support ⊆ singleton n

Full source

theorem support_monomial' (n) (a : R) : (monomial n a).support ⊆ singleton n := by
  rw [← ofFinsupp_single, support]
  exact Finsupp.support_single_subset

Support of Monomial is Subset of Singleton

Informal description

For any natural number $n$ and coefficient $a$ in a semiring $R$, the support of the monomial $a X^n$ is a subset of the singleton set $\{n\}$. In other words, the only possible nonzero coefficient in the monomial $a X^n$ is at the term $X^n$.

Polynomial.support_C theorem

{a : R} (h : a ≠ 0) : (C a).support = singleton 0

Full source

theorem support_C {a : R} (h : a ≠ 0) : (C a).support = singleton 0 :=
  support_monomial 0 h

Support of Constant Polynomial $C(a)$ is $\{0\}$ for $a \neq 0$

Informal description

For any nonzero element $a$ in a semiring $R$, the support of the constant polynomial $C(a)$ is the singleton set $\{0\}$.

Polynomial.support_C_subset theorem

(a : R) : (C a).support ⊆ singleton 0

Full source

theorem support_C_subset (a : R) : (C a).support ⊆ singleton 0 :=
  support_monomial' 0 a

Support of Constant Polynomial is Subset of $\{0\}$

Informal description

For any element $a$ in a semiring $R$, the support of the constant polynomial $C(a)$ is a subset of the singleton set $\{0\}$. In other words, the only possible nonzero coefficient in the constant polynomial $C(a)$ is the constant term (the coefficient of $X^0$).

Polynomial.support_C_mul_X theorem

{c : R} (h : c ≠ 0) : Polynomial.support (C c * X) = singleton 1

Full source

theorem support_C_mul_X {c : R} (h : c ≠ 0) : Polynomial.support (C c * X) = singleton 1 := by
  rw [C_mul_X_eq_monomial, support_monomial 1 h]

Support of Linear Term $cX$ is $\{1\}$ for $c \neq 0$

Informal description

For any nonzero element $c$ in a semiring $R$, the support of the polynomial $c X$ is the singleton set $\{1\}$.

Polynomial.support_C_mul_X' theorem

(c : R) : Polynomial.support (C c * X) ⊆ singleton 1

Full source

theorem support_C_mul_X' (c : R) : Polynomial.supportPolynomial.support (C c * X) ⊆ singleton 1 := by
  simpa only [C_mul_X_eq_monomial] using support_monomial' 1 c

Support of Linear Term $cX$ is Subset of $\{1\}$

Informal description

For any coefficient $c$ in a semiring $R$, the support of the polynomial $c X$ is contained in the singleton set $\{1\}$. In other words, the only possible nonzero coefficient in the polynomial $c X$ is at the term $X^1$.

Polynomial.support_C_mul_X_pow theorem

(n : ℕ) {c : R} (h : c ≠ 0) : Polynomial.support (C c * X ^ n) = singleton n

Full source

theorem support_C_mul_X_pow (n : ℕ) {c : R} (h : c ≠ 0) :
    Polynomial.support (C c * X ^ n) = singleton n := by
  rw [C_mul_X_pow_eq_monomial, support_monomial n h]

Support of $c X^n$ is $\{n\}$ for $c \neq 0$

Informal description

For any natural number $n$ and nonzero element $c$ in a semiring $R$, the support of the polynomial $c X^n$ is the singleton set $\{n\}$.

Polynomial.support_C_mul_X_pow' theorem

(n : ℕ) (c : R) : Polynomial.support (C c * X ^ n) ⊆ singleton n

Full source

theorem support_C_mul_X_pow' (n : ℕ) (c : R) : Polynomial.supportPolynomial.support (C c * X ^ n) ⊆ singleton n := by
  simpa only [C_mul_X_pow_eq_monomial] using support_monomial' n c

Support of $c X^n$ is contained in $\{n\}$

Informal description

For any natural number $n$ and coefficient $c$ in a semiring $R$, the support of the polynomial $c X^n$ is a subset of the singleton set $\{n\}$. In other words, the only possible nonzero coefficient in the polynomial $c X^n$ is at the term $X^n$.

Polynomial.support_binomial' theorem

(k m : ℕ) (x y : R) : Polynomial.support (C x * X ^ k + C y * X ^ m) ⊆ { k, m }

Full source

theorem support_binomial' (k m : ℕ) (x y : R) :
    Polynomial.supportPolynomial.support (C x * X ^ k + C y * X ^ m) ⊆ {k, m} :=
  support_add.trans
    (union_subset
      ((support_C_mul_X_pow' k x).trans (singleton_subset_iff.mpr (mem_insert_self k {m})))
      ((support_C_mul_X_pow' m y).trans
        (singleton_subset_iff.mpr (mem_insert_of_mem (mem_singleton_self m)))))

Support of Binomial Polynomial is Contained in $\{k, m\}$

Informal description

For any natural numbers $k, m$ and coefficients $x, y$ in a semiring $R$, the support of the binomial polynomial $x X^k + y X^m$ is a subset of the doubleton set $\{k, m\}$.

Polynomial.support_trinomial' theorem

(k m n : ℕ) (x y z : R) : Polynomial.support (C x * X ^ k + C y * X ^ m + C z * X ^ n) ⊆ { k, m, n }

Full source

theorem support_trinomial' (k m n : ℕ) (x y z : R) :
    Polynomial.supportPolynomial.support (C x * X ^ k + C y * X ^ m + C z * X ^ n) ⊆ {k, m, n} :=
  support_add.trans
    (union_subset
      (support_add.trans
        (union_subset
          ((support_C_mul_X_pow' k x).trans (singleton_subset_iff.mpr (mem_insert_self k {m, n})))
          ((support_C_mul_X_pow' m y).trans
            (singleton_subset_iff.mpr (mem_insert_of_mem (mem_insert_self m {n}))))))
      ((support_C_mul_X_pow' n z).trans
        (singleton_subset_iff.mpr (mem_insert_of_mem (mem_insert_of_mem (mem_singleton_self n))))))

Support of Trinomial $x X^k + y X^m + z X^n$ is Contained in $\{k, m, n\}$

Informal description

For any natural numbers $k, m, n$ and coefficients $x, y, z$ in a semiring $R$, the support of the trinomial polynomial $x X^k + y X^m + z X^n$ is contained in the finite set $\{k, m, n\}$.

Polynomial.X_pow_eq_monomial theorem

(n) : X ^ n = monomial n (1 : R)

Full source

theorem X_pow_eq_monomial (n) : X ^ n = monomial n (1 : R) := by
  induction n with
  | zero => rw [pow_zero, monomial_zero_one]
  | succ n hn => rw [pow_succ, hn, X, monomial_mul_monomial, one_mul]

Power of Polynomial Variable as Monomial: $X^n = \text{monomial}_n(1)$

Informal description

For any natural number $n$, the $n$-th power of the polynomial variable $X$ in the polynomial ring $R[X]$ is equal to the monomial with coefficient $1$ and degree $n$, i.e., $X^n = 1 \cdot X^n$.

Polynomial.toFinsupp_X_pow theorem

(n : ℕ) : (X ^ n).toFinsupp = Finsupp.single n (1 : R)

Full source

@[simp high]
theorem toFinsupp_X_pow (n : ℕ) : (X ^ n).toFinsupp = Finsupp.single n (1 : R) := by
  rw [X_pow_eq_monomial, toFinsupp_monomial]

Conversion of $X^n$ to Finsupp: $(X^n).\text{toFinsupp} = \text{single}(n, 1)$

Informal description

For any natural number $n$, the underlying additive monoid algebra representation of the polynomial $X^n$ in $R[X]$ is the finitely supported function that takes the value $1$ at $n$ and zero elsewhere. In other words, $(X^n).\text{toFinsupp} = \text{single}(n, 1)$.

Polynomial.smul_X_eq_monomial theorem

{n} : a • X ^ n = monomial n (a : R)

Full source

theorem smul_X_eq_monomial {n} : a • X ^ n = monomial n (a : R) := by
  rw [X_pow_eq_monomial, smul_monomial, smul_eq_mul, mul_one]

Scalar Multiplication of Polynomial Variable: $a \cdot X^n = a X^n$

Informal description

For any element $a$ in a semiring $R$ and any natural number $n$, the scalar multiple $a \cdot X^n$ in the polynomial ring $R[X]$ is equal to the monomial $a X^n$, where $X$ is the polynomial variable. In mathematical notation: $$a \cdot X^n = a X^n.$$

Polynomial.support_X_pow theorem

(H : ¬(1 : R) = 0) (n : ℕ) : (X ^ n : R[X]).support = singleton n

Full source

theorem support_X_pow (H : ¬(1 : R) = 0) (n : ℕ) : (X ^ n : R[X]).support = singleton n := by
  convert support_monomial n H
  exact X_pow_eq_monomial n

Support of $X^n$ is $\{n\}$ when $1 \neq 0$ in $R$

Informal description

For any natural number $n$, if the multiplicative identity $1$ in the semiring $R$ is not equal to the additive identity $0$, then the support of the polynomial $X^n$ in $R[X]$ is the singleton set $\{n\}$.

Polynomial.support_X_empty theorem

(H : (1 : R) = 0) : (X : R[X]).support = ∅

Full source

theorem support_X_empty (H : (1 : R) = 0) : (X : R[X]).support = ∅ := by
  rw [X, H, monomial_zero_right, support_zero]

Support of $X$ is Empty When $1 = 0$ in $R$

Informal description

If the multiplicative identity $1$ in the semiring $R$ is equal to the additive identity $0$, then the support of the polynomial variable $X$ in $R[X]$ is the empty set, i.e., $\text{support}(X) = \emptyset$.

Polynomial.support_X theorem

(H : ¬(1 : R) = 0) : (X : R[X]).support = singleton 1

Full source

theorem support_X (H : ¬(1 : R) = 0) : (X : R[X]).support = singleton 1 := by
  rw [← pow_one X, support_X_pow H 1]

Support of $X$ is $\{1\}$ when $1 \neq 0$ in $R$

Informal description

For a semiring $R$ where the multiplicative identity $1$ is not equal to the additive identity $0$, the support of the polynomial variable $X$ in $R[X]$ is the singleton set $\{1\}$.

Polynomial.monomial_left_inj theorem

{a : R} (ha : a ≠ 0) {i j : ℕ} : monomial i a = monomial j a ↔ i = j

Full source

theorem monomial_left_inj {a : R} (ha : a ≠ 0) {i j : ℕ} :
    monomialmonomial i a = monomial j a ↔ i = j := by
  simp only [← ofFinsupp_single, ofFinsupp.injEq, Finsupp.single_left_inj ha]

Monomial Equality Condition: $aX^i = aX^j \leftrightarrow i = j$ for $a \neq 0$

Informal description

For any nonzero element $a$ in a semiring $R$ and natural numbers $i$ and $j$, the monomials $aX^i$ and $aX^j$ are equal if and only if $i = j$.

Polynomial.binomial_eq_binomial theorem

 {k l m n : ℕ} {u v : R} (hu : u ≠ 0) (hv : v ≠ 0) :
  C u * X ^ k + C v * X ^ l = C u * X ^ m + C v * X ^ n ↔
    k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n

Full source

theorem binomial_eq_binomial {k l m n : ℕ} {u v : R} (hu : u ≠ 0) (hv : v ≠ 0) :
    CC u * X ^ k + C v * X ^ l = C u * X ^ m + C v * X ^ n ↔
      k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n := by
  simp_rw [C_mul_X_pow_eq_monomial, ← toFinsupp_inj, toFinsupp_add, toFinsupp_monomial]
  exact Finsupp.single_add_single_eq_single_add_single hu hv

Equality Condition for Binomials in Polynomial Ring $R[X]$

Informal description

For any natural numbers $k, l, m, n$ and nonzero elements $u, v$ in a semiring $R$, the equality of binomials $$ u X^k + v X^l = u X^m + v X^n $$ holds if and only if one of the following conditions is satisfied: 1. $k = m$ and $l = n$, or 2. $u = v$, $k = n$, and $l = m$, or 3. $u + v = 0$, $k = l$, and $m = n$.

Polynomial.natCast_mul theorem

(n : ℕ) (p : R[X]) : (n : R[X]) * p = n • p

Full source

theorem natCast_mul (n : ℕ) (p : R[X]) : (n : R[X]) * p = n • p :=
  (nsmul_eq_mul _ _).symm

Natural number cast multiplication equals scalar multiplication in $R[X]$: $(n) \cdot p = n \cdot p$

Informal description

For any natural number $n$ and any polynomial $p \in R[X]$ over a semiring $R$, the product of the constant polynomial $n$ with $p$ is equal to the scalar multiple $n \cdot p$.

Polynomial.sum definition

{S : Type*} [AddCommMonoid S] (p : R[X]) (f : ℕ → R → S) : S

Full source

/-- Summing the values of a function applied to the coefficients of a polynomial -/
def sum {S : Type*} [AddCommMonoid S] (p : R[X]) (f : ℕ → R → S) : S :=
  ∑ n ∈ p.support, f n (p.coeff n)

Sum over polynomial coefficients

Informal description

Given a polynomial $ p \in R[X] $ over a semiring $ R $, an additive commutative monoid $ S $, and a function $ f : \mathbb{N} \to R \to S $, the sum $ p.\text{sum} \, f $ is defined as the finite sum $ \sum_{n \in p.\text{support}} f \, n \, (p.\text{coeff} \, n) $, where $ p.\text{support} $ is the set of exponents with nonzero coefficients in $ p $.

Polynomial.sum_def theorem

{S : Type*} [AddCommMonoid S] (p : R[X]) (f : ℕ → R → S) : p.sum f = ∑ n ∈ p.support, f n (p.coeff n)

Full source

theorem sum_def {S : Type*} [AddCommMonoid S] (p : R[X]) (f : ℕ → R → S) :
    p.sum f = ∑ n ∈ p.support, f n (p.coeff n) :=
  rfl

Definition of Polynomial Sum via Support and Coefficients

Informal description

For any polynomial $p \in R[X]$ over a semiring $R$, any additive commutative monoid $S$, and any function $f \colon \mathbb{N} \to R \to S$, the sum $p.\text{sum}\, f$ is equal to the finite sum $\sum_{n \in p.\text{support}} f(n, p_n)$, where $p_n$ denotes the coefficient of $X^n$ in $p$.

Polynomial.sum_eq_of_subset theorem

 {S : Type*} [AddCommMonoid S] {p : R[X]} (f : ℕ → R → S) (hf : ∀ i, f i 0 = 0) {s : Finset ℕ} (hs : p.support ⊆ s) :
  p.sum f = ∑ n ∈ s, f n (p.coeff n)

Full source

theorem sum_eq_of_subset {S : Type*} [AddCommMonoid S] {p : R[X]} (f : ℕ → R → S)
    (hf : ∀ i, f i 0 = 0) {s : Finset ℕ} (hs : p.support ⊆ s) :
    p.sum f = ∑ n ∈ s, f n (p.coeff n) :=
  Finsupp.sum_of_support_subset _ hs f (fun i _ ↦ hf i)

Polynomial Sum Equality Under Support Containment

Informal description

Let $R$ be a semiring and $S$ an additive commutative monoid. For any polynomial $p \in R[X]$, function $f \colon \mathbb{N} \to R \to S$ satisfying $f(i, 0) = 0$ for all $i$, and finite set $s \subseteq \mathbb{N}$ containing the support of $p$, we have: \[ \sum_{n \in \text{supp}(p)} f(n, p_n) = \sum_{n \in s} f(n, p_n) \] where $p_n$ denotes the coefficient of $X^n$ in $p$ and $\text{supp}(p)$ is the support of $p$.

Polynomial.mul_eq_sum_sum theorem

: p * q = ∑ i ∈ p.support, q.sum fun j a => (monomial (i + j)) (p.coeff i * a)

Full source

/-- Expressing the product of two polynomials as a double sum. -/
theorem mul_eq_sum_sum :
    p * q = ∑ i ∈ p.support, q.sum fun j a => (monomial (i + j)) (p.coeff i * a) := by
  apply toFinsupp_injective
  rcases p with ⟨⟩; rcases q with ⟨⟩
  simp_rw [sum, coeff, toFinsupp_sum, support, toFinsupp_mul, toFinsupp_monomial,
    AddMonoidAlgebra.mul_def, Finsupp.sum]

Polynomial Multiplication as Double Sum of Monomials

Informal description

For any two polynomials $p$ and $q$ over a semiring $R$, their product $p \cdot q$ can be expressed as the double sum: \[ p \cdot q = \sum_{i \in \text{supp}(p)} \sum_{j \in \text{supp}(q)} a_{i} b_{j} X^{i+j} \] where $a_i$ is the coefficient of $X^i$ in $p$ (i.e., $a_i = p_i$), $b_j$ is the coefficient of $X^j$ in $q$ (i.e., $b_j = q_j$), and $\text{supp}(p)$ and $\text{supp}(q)$ are the supports of $p$ and $q$ respectively.

Polynomial.sum_zero_index theorem

{S : Type*} [AddCommMonoid S] (f : ℕ → R → S) : (0 : R[X]).sum f = 0

Full source

@[simp]
theorem sum_zero_index {S : Type*} [AddCommMonoid S] (f : ℕ → R → S) : (0 : R[X]).sum f = 0 := by
  simp [sum]

Sum over coefficients of the zero polynomial is zero

Informal description

For any additive commutative monoid $S$ and any function $f \colon \mathbb{N} \to R \to S$, the sum of the zero polynomial $0 \in R[X]$ over its coefficients with respect to $f$ is equal to the zero element of $S$, i.e., $\sum_{n \in \text{support}(0)} f(n, 0_n) = 0_S$.

Polynomial.sum_monomial_index theorem

 {S : Type*} [AddCommMonoid S] {n : ℕ} (a : R) (f : ℕ → R → S) (hf : f n 0 = 0) : (monomial n a : R[X]).sum f = f n a

Full source

@[simp]
theorem sum_monomial_index {S : Type*} [AddCommMonoid S] {n : ℕ} (a : R) (f : ℕ → R → S)
    (hf : f n 0 = 0) : (monomial n a : R[X]).sum f = f n a :=
  Finsupp.sum_single_index hf

Sum of Coefficients for Monomial $aX^n$

Informal description

Let $R$ be a semiring, $S$ an additive commutative monoid, $n \in \mathbb{N}$, $a \in R$, and $f \colon \mathbb{N} \to R \to S$ a function such that $f(n, 0) = 0$. Then the sum of coefficients of the monomial $aX^n$ with respect to $f$ equals $f(n, a)$, i.e., \[ \sum_{k \in \text{supp}(aX^n)} f(k, \text{coeff}(aX^n)_k) = f(n, a). \]

Polynomial.sum_C_index theorem

{a} {β} [AddCommMonoid β] {f : ℕ → R → β} (h : f 0 0 = 0) : (C a).sum f = f 0 a

Full source

@[simp]
theorem sum_C_index {a} {β} [AddCommMonoid β] {f : ℕ → R → β} (h : f 0 0 = 0) :
    (C a).sum f = f 0 a :=
  sum_monomial_index a f h

Sum of Coefficients for Constant Polynomial $a$

Informal description

Let $R$ be a semiring, $\beta$ an additive commutative monoid, $a \in R$, and $f \colon \mathbb{N} \to R \to \beta$ a function such that $f(0, 0) = 0$. Then the sum of coefficients of the constant polynomial $C(a) = a$ with respect to $f$ equals $f(0, a)$, i.e., \[ \sum_{n \in \text{supp}(a)} f(n, \text{coeff}(a)_n) = f(0, a). \]

Polynomial.sum_X_index theorem

{S : Type*} [AddCommMonoid S] {f : ℕ → R → S} (hf : f 1 0 = 0) : (X : R[X]).sum f = f 1 1

Full source

@[simp]
theorem sum_X_index {S : Type*} [AddCommMonoid S] {f : ℕ → R → S} (hf : f 1 0 = 0) :
    (X : R[X]).sum f = f 1 1 :=
  sum_monomial_index 1 f hf

Sum of Coefficients for Polynomial $X$

Informal description

Let $R$ be a semiring and $S$ an additive commutative monoid. For any function $f \colon \mathbb{N} \to R \to S$ such that $f(1, 0) = 0$, the sum of coefficients of the polynomial $X$ with respect to $f$ equals $f(1, 1)$. That is, \[ \sum_{n \in \text{supp}(X)} f(n, \text{coeff}(X)_n) = f(1, 1). \]

Polynomial.sum_add_index theorem

 {S : Type*} [AddCommMonoid S] (p q : R[X]) (f : ℕ → R → S) (hf : ∀ i, f i 0 = 0)
  (h_add : ∀ a b₁ b₂, f a (b₁ + b₂) = f a b₁ + f a b₂) : (p + q).sum f = p.sum f + q.sum f

Full source

theorem sum_add_index {S : Type*} [AddCommMonoid S] (p q : R[X]) (f : ℕ → R → S)
    (hf : ∀ i, f i 0 = 0) (h_add : ∀ a b₁ b₂, f a (b₁ + b₂) = f a b₁ + f a b₂) :
    (p + q).sum f = p.sum f + q.sum f := by
  rw [show p + q = ⟨p.toFinsupp + q.toFinsupp⟩ from add_def p q]
  exact Finsupp.sum_add_index (fun i _ ↦ hf i) (fun a _ b₁ b₂ ↦ h_add a b₁ b₂)

Additivity of Polynomial Summation under Addition of Polynomials

Informal description

Let $R$ be a semiring and $S$ an additive commutative monoid. For any polynomials $p, q \in R[X]$ and a function $f : \mathbb{N} \to R \to S$ such that: 1. $f(i, 0) = 0$ for all $i \in \mathbb{N}$, 2. $f(a, b_1 + b_2) = f(a, b_1) + f(a, b_2)$ for all $a \in \mathbb{N}$ and $b_1, b_2 \in R$, the sum of $f$ over the coefficients of $p + q$ equals the sum of $f$ over $p$ plus the sum of $f$ over $q$. That is, \[ \sum_{n \in \text{supp}(p+q)} f(n, (p + q)_n) = \left(\sum_{n \in \text{supp}(p)} f(n, p_n)\right) + \left(\sum_{n \in \text{supp}(q)} f(n, q_n)\right), \] where $(p + q)_n$ denotes the coefficient of $X^n$ in $p + q$, and $\text{supp}(p)$ is the support of $p$ (the set of exponents with nonzero coefficients).

Polynomial.sum_add' theorem

{S : Type*} [AddCommMonoid S] (p : R[X]) (f g : ℕ → R → S) : p.sum (f + g) = p.sum f + p.sum g

Full source

theorem sum_add' {S : Type*} [AddCommMonoid S] (p : R[X]) (f g : ℕ → R → S) :
    p.sum (f + g) = p.sum f + p.sum g := by simp [sum_def, Finset.sum_add_distrib]

Additivity of Polynomial Summation over Pointwise Addition of Functions

Informal description

Let $R$ be a semiring and $S$ be an additive commutative monoid. For any polynomial $p \in R[X]$ and functions $f, g : \mathbb{N} \to R \to S$, the sum over $p$ of the pointwise addition of $f$ and $g$ equals the sum of the individual sums of $f$ and $g$ over $p$. That is, \[ \sum_{n \in \text{supp}(p)} (f(n) + g(n))(p_n) = \left(\sum_{n \in \text{supp}(p)} f(n)(p_n)\right) + \left(\sum_{n \in \text{supp}(p)} g(n)(p_n)\right), \] where $p_n$ denotes the coefficient of $X^n$ in $p$ and $\text{supp}(p)$ is the support of $p$ (the set of exponents with nonzero coefficients).

Polynomial.sum_add theorem

{S : Type*} [AddCommMonoid S] (p : R[X]) (f g : ℕ → R → S) : (p.sum fun n x => f n x + g n x) = p.sum f + p.sum g

Full source

theorem sum_add {S : Type*} [AddCommMonoid S] (p : R[X]) (f g : ℕ → R → S) :
    (p.sum fun n x => f n x + g n x) = p.sum f + p.sum g :=
  sum_add' _ _ _

Additivity of Polynomial Summation over Coefficient-wise Addition

Informal description

Let $R$ be a semiring and $S$ an additive commutative monoid. For any polynomial $p \in R[X]$ and functions $f, g : \mathbb{N} \to R \to S$, the sum of $f(n)(x) + g(n)(x)$ over the coefficients of $p$ equals the sum of $f$ over $p$ plus the sum of $g$ over $p$. That is, \[ \sum_{n \in \text{supp}(p)} (f(n, p_n) + g(n, p_n)) = \left(\sum_{n \in \text{supp}(p)} f(n, p_n)\right) + \left(\sum_{n \in \text{supp}(p)} g(n, p_n)\right), \] where $p_n$ denotes the coefficient of $X^n$ in $p$ and $\text{supp}(p)$ is the support of $p$ (the set of exponents with nonzero coefficients).

Polynomial.sum_smul_index theorem

 {S : Type*} [AddCommMonoid S] (p : R[X]) (b : R) (f : ℕ → R → S) (hf : ∀ i, f i 0 = 0) :
  (b • p).sum f = p.sum fun n a => f n (b * a)

Full source

theorem sum_smul_index {S : Type*} [AddCommMonoid S] (p : R[X]) (b : R) (f : ℕ → R → S)
    (hf : ∀ i, f i 0 = 0) : (b • p).sum f = p.sum fun n a => f n (b * a) :=
  Finsupp.sum_smul_index hf

Linearity of Polynomial Summation under Scalar Multiplication

Informal description

Let $R$ be a semiring and $S$ an additive commutative monoid. For any polynomial $p \in R[X]$, scalar $b \in R$, and function $f \colon \mathbb{N} \to R \to S$ such that $f(i, 0) = 0$ for all $i \in \mathbb{N}$, the sum over the coefficients of the scalar multiple $b \cdot p$ satisfies: \[ \sum_{n \in \mathbb{N}} f(n, (b \cdot p)_n) = \sum_{n \in \mathbb{N}} f(n, b \cdot p_n), \] where $p_n$ denotes the coefficient of $X^n$ in $p$ and the sums are taken over the support of $p$ (i.e., only finitely many terms are nonzero).

Polynomial.sum_smul_index' theorem

 {S T : Type*} [DistribSMul T R] [AddCommMonoid S] (p : R[X]) (b : T) (f : ℕ → R → S) (hf : ∀ i, f i 0 = 0) :
  (b • p).sum f = p.sum fun n a => f n (b • a)

Full source

theorem sum_smul_index' {S T : Type*} [DistribSMul T R] [AddCommMonoid S] (p : R[X]) (b : T)
    (f : ℕ → R → S) (hf : ∀ i, f i 0 = 0) : (b • p).sum f = p.sum fun n a => f n (b • a) :=
  Finsupp.sum_smul_index' hf

Linearity of Summation under Scalar Multiplication in Polynomial Ring

Informal description

Let $R$ be a semiring, $S$ an additive commutative monoid, and $T$ a type with a distributive scalar multiplication action on $R$. For any polynomial $p \in R[X]$, scalar $b \in T$, and function $f \colon \mathbb{N} \to R \to S$ such that $f(i, 0) = 0$ for all $i \in \mathbb{N}$, we have: \[ \sum_{n \in \text{supp}(p)} f(n, (b \cdot p)_n) = \sum_{n \in \text{supp}(p)} f(n, b \cdot p_n), \] where $(b \cdot p)_n$ denotes the coefficient of $X^n$ in the scalar multiple $b \cdot p$, and $\text{supp}(p)$ is the support of $p$ (the set of exponents with nonzero coefficients).

Polynomial.smul_sum theorem

 {S T : Type*} [AddCommMonoid S] [DistribSMul T S] (p : R[X]) (b : T) (f : ℕ → R → S) :
  b • p.sum f = p.sum fun n a => b • f n a

Full source

protected theorem smul_sum {S T : Type*} [AddCommMonoid S] [DistribSMul T S] (p : R[X]) (b : T)
    (f : ℕ → R → S) : b • p.sum f = p.sum fun n a => b • f n a :=
  Finsupp.smul_sum

Scalar Multiplication Distributes over Polynomial Coefficient Summation

Informal description

Let $R$ be a semiring, $S$ an additive commutative monoid with a distributive scalar multiplication by $T$, and $p \in R[X]$ a polynomial. For any scalar $b \in T$ and any function $f \colon \mathbb{N} \to R \to S$, we have: \[ b \cdot \left( \sum_{n \in \mathbb{N}} f(n, p_n) \right) = \sum_{n \in \mathbb{N}} b \cdot f(n, p_n), \] where $p_n$ denotes the coefficient of $X^n$ in $p$ and the sums are taken over the support of $p$ (i.e., only finitely many terms are nonzero).

Polynomial.sum_monomial_eq theorem

: ∀ p : R[X], (p.sum fun n a => monomial n a) = p

Full source

@[simp]
theorem sum_monomial_eq : ∀ p : R[X], (p.sum fun n a => monomial n a) = p
  | ⟨_p⟩ => (ofFinsupp_sum _ _).symm.trans (congr_arg _ <| Finsupp.sum_single _)

Monomial Sum Representation of a Polynomial

Informal description

For any polynomial $p \in R[X]$, the sum over its support of the monomials $\text{monomial}(n, a_n)$ (where $a_n$ is the coefficient of $X^n$ in $p$) equals $p$ itself. That is, \[ \sum_{n \in \text{supp}(p)} a_n X^n = p. \]

Polynomial.sum_C_mul_X_pow_eq theorem

(p : R[X]) : (p.sum fun n a => C a * X ^ n) = p

Full source

theorem sum_C_mul_X_pow_eq (p : R[X]) : (p.sum fun n a => C a * X ^ n) = p := by
  simp_rw [C_mul_X_pow_eq_monomial, sum_monomial_eq]

Polynomial Representation as Sum of Monomials

Informal description

For any polynomial $p \in R[X]$, the sum over its support of the terms $a_n \cdot X^n$ (where $a_n$ is the coefficient of $X^n$ in $p$) equals $p$ itself. That is, \[ \sum_{n \in \text{supp}(p)} a_n X^n = p. \]

Polynomial.induction_on theorem

 {motive : R[X] → Prop} (p : R[X]) (C : ∀ a, motive (C a)) (add : ∀ p q, motive p → motive q → motive (p + q))
  (monomial : ∀ (n : ℕ) (a : R), motive (Polynomial.C a * X ^ n) → motive (Polynomial.C a * X ^ (n + 1))) : motive p

Full source

@[elab_as_elim]
protected theorem induction_on {motive : R[X] → Prop} (p : R[X]) (C : ∀ a, motive (C a))
    (add : ∀ p q, motive p → motive q → motive (p + q))
    (monomial : ∀ (n : ℕ) (a : R),
      motive (Polynomial.C a * X ^ n) → motive (Polynomial.C a * X ^ (n + 1))) : motive p := by
  have A : ∀ {n : ℕ} {a}, motive (Polynomial.C a * X ^ n) := by
    intro n a
    induction n with
    | zero => rw [pow_zero, mul_one]; exact C a
    | succ n ih => exact monomial _ _ ih
  have B : ∀ s : Finset ℕ, motive (s.sum fun n : ℕ => Polynomial.C (p.coeff n) * X ^ n) := by
    apply Finset.induction
    · convert C 0
      exact C_0.symm
    · intro n s ns ih
      rw [sum_insert ns]
      exact add _ _ A ih
  rw [← sum_C_mul_X_pow_eq p, Polynomial.sum]
  exact B (support p)

Induction Principle for Polynomials via Constants, Addition, and Monomials

Informal description

Let $R$ be a semiring and $R[X]$ be the polynomial ring over $R$. For any predicate $\text{motive}$ on $R[X]$, to prove that $\text{motive}(p)$ holds for all polynomials $p \in R[X]$, it suffices to: 1. Prove the base case for constant polynomials: $\text{motive}(C(a))$ holds for all $a \in R$. 2. Prove the additive closure: For any $p, q \in R[X]$, if $\text{motive}(p)$ and $\text{motive}(q)$ hold, then $\text{motive}(p + q)$ holds. 3. Prove the monomial step: For any $n \in \mathbb{N}$ and $a \in R$, if $\text{motive}(C(a) \cdot X^n)$ holds, then $\text{motive}(C(a) \cdot X^{n+1})$ holds.

Polynomial.induction_on' theorem

 {motive : R[X] → Prop} (p : R[X]) (add : ∀ p q, motive p → motive q → motive (p + q))
  (monomial : ∀ (n : ℕ) (a : R), motive (monomial n a)) : motive p

Full source

/-- To prove something about polynomials,
it suffices to show the condition is closed under taking sums,
and it holds for monomials.
-/
@[elab_as_elim]
protected theorem induction_on' {motive : R[X] → Prop} (p : R[X])
    (add : ∀ p q, motive p → motive q → motive (p + q))
    (monomial : ∀ (n : ℕ) (a : R), motive (monomial n a)) : motive p :=
  Polynomial.induction_on p (monomial 0) add fun n a _h =>
    by rw [C_mul_X_pow_eq_monomial]; exact monomial _ _

Induction Principle for Polynomials via Addition and Monomials

Informal description

Let $R$ be a semiring and $R[X]$ be the polynomial ring over $R$. For any predicate $\text{motive}$ on $R[X]$, to prove that $\text{motive}(p)$ holds for all polynomials $p \in R[X]$, it suffices to: 1. Prove the additive closure: For any $p, q \in R[X]$, if $\text{motive}(p)$ and $\text{motive}(q)$ hold, then $\text{motive}(p + q)$ holds. 2. Prove the monomial case: $\text{motive}(a X^n)$ holds for all $n \in \mathbb{N}$ and $a \in R$.

Polynomial.erase definition

Full source

/-- `erase p n` is the polynomial `p` in which the `X^n` term has been erased. -/
irreducible_def erase (n : ℕ) : R[X] → R[X]
  | ⟨p⟩ => ⟨p.erase n⟩

Polynomial term erasure

Informal description

For a polynomial $p \in R[X]$ and a natural number $n$, the operation $\operatorname{erase}(p, n)$ returns the polynomial obtained by removing the term of degree $n$ from $p$. In other words, if $p = \sum_{k} a_k X^k$, then $\operatorname{erase}(p, n) = \sum_{k \neq n} a_k X^k$.

Polynomial.erase_def theorem

: eta_helper Eq✝ @erase.{} @(delta% @definition✝)

Full source

/-- `erase p n` is the polynomial `p` in which the `X^n` term has been erased. -/
irreducible_def erase (n : ℕ) : R[X] → R[X]
  | ⟨p⟩ => ⟨p.erase n⟩

Definition of Polynomial Term Erasure Operation

Informal description

The operation `erase n` on a polynomial $p \in R[X]$ is defined such that for any natural number $n$, the polynomial $p.\text{erase}(n)$ is obtained by removing the term of degree $n$ from $p$. Specifically, if $p = \sum_{k} a_k X^k$, then $p.\text{erase}(n) = \sum_{k \neq n} a_k X^k$.

Polynomial.toFinsupp_erase theorem

(p : R[X]) (n : ℕ) : toFinsupp (p.erase n) = p.toFinsupp.erase n

Full source

@[simp]
theorem toFinsupp_erase (p : R[X]) (n : ℕ) : toFinsupp (p.erase n) = p.toFinsupp.erase n := by
  rcases p with ⟨⟩
  simp only [erase_def]

Commutativity of Erasure and Conversion: $\text{toFinsupp}(p.\text{erase}(n)) = \text{toFinsupp}(p).\text{erase}(n)$

Informal description

For any polynomial $p \in R[X]$ and any natural number $n$, the conversion of the erased polynomial $p.\text{erase}(n)$ to its additive monoid algebra representation equals the erasure of the $n$-th term in the additive monoid algebra representation of $p$. That is, $\text{toFinsupp}(p.\text{erase}(n)) = \text{toFinsupp}(p).\text{erase}(n)$.

Polynomial.ofFinsupp_erase theorem

(p : R[ℕ]) (n : ℕ) :
    (⟨p.erase n⟩ : R[X]) = (⟨p⟩ : R[X]).erase n

Full source

@[simp]
theorem ofFinsupp_erase (p : R[ℕ]) (n : ℕ) :
    (⟨p.erase n⟩ : R[X]) = (⟨p⟩ : R[X]).erase n := by
  rcases p with ⟨⟩
  simp only [erase_def]

Commutativity of Erasure and Polynomial Conversion: $\langle p \text{ erase } n \rangle = \langle p \rangle \text{ erase } n$

Informal description

For any polynomial $p$ in the additive monoid algebra $R[\mathbb{N}]$ and any natural number $n$, the polynomial obtained by first erasing the term of degree $n$ from $p$ and then converting it to a univariate polynomial $R[X]$ is equal to first converting $p$ to a univariate polynomial and then erasing the term of degree $n$. In other words, the erasure operation commutes with the conversion from $R[\mathbb{N}]$ to $R[X]$.

Polynomial.support_erase theorem

(p : R[X]) (n : ℕ) : support (p.erase n) = (support p).erase n

Full source

@[simp]
theorem support_erase (p : R[X]) (n : ℕ) : support (p.erase n) = (support p).erase n := by
  rcases p with ⟨⟩
  simp only [support, erase_def, Finsupp.support_erase]

Support of Polynomial After Term Erasure Equals Support Minus Degree

Informal description

For any polynomial $p \in R[X]$ and any natural number $n$, the support of the polynomial $p.\text{erase}(n)$ (obtained by removing the term of degree $n$ from $p$) is equal to the set obtained by removing $n$ from the support of $p$. That is, $\text{support}(p.\text{erase}(n)) = \text{support}(p) \setminus \{n\}$.

Polynomial.monomial_add_erase theorem

(p : R[X]) (n : ℕ) : monomial n (coeff p n) + p.erase n = p

Full source

theorem monomial_add_erase (p : R[X]) (n : ℕ) : monomial n (coeff p n) + p.erase n = p :=
  toFinsupp_injective <| by
    rcases p with ⟨⟩
    rw [toFinsupp_add, toFinsupp_monomial, toFinsupp_erase, coeff]
    exact Finsupp.single_add_erase _ _

Polynomial Decomposition: $p = a_nX^n + p \setminus X^n$

Informal description

For any polynomial $p \in R[X]$ and any natural number $n$, the sum of the monomial $(\text{coeff } p n) X^n$ and the polynomial obtained by erasing the $n$-th degree term from $p$ equals $p$ itself. That is, $$ \text{monomial}_n (p_n) + \text{erase}(p, n) = p $$ where $p_n$ denotes the coefficient of $X^n$ in $p$.

Polynomial.coeff_erase theorem

(p : R[X]) (n i : ℕ) : (p.erase n).coeff i = if i = n then 0 else p.coeff i

Full source

theorem coeff_erase (p : R[X]) (n i : ℕ) :
    (p.erase n).coeff i = if i = n then 0 else p.coeff i := by
  rcases p with ⟨⟩
  simp only [erase_def, coeff]
  exact ite_congr rfl (fun _ => rfl) (fun _ => rfl)

Coefficient of Polynomial After Term Erasure: $\text{coeff}(\text{erase}(p, n), i) = \text{coeff}(p, i)$ for $i \neq n$ and $0$ otherwise

Informal description

For any polynomial $p \in R[X]$, natural numbers $n$ and $i$, the coefficient of $X^i$ in the polynomial obtained by erasing the term of degree $n$ from $p$ is given by: \[ (p.\text{erase}(n)).\text{coeff}(i) = \begin{cases} 0 & \text{if } i = n, \\ p.\text{coeff}(i) & \text{otherwise.} \end{cases} \]

Polynomial.erase_zero theorem

(n : ℕ) : (0 : R[X]).erase n = 0

Full source

@[simp]
theorem erase_zero (n : ℕ) : (0 : R[X]).erase n = 0 :=
  toFinsupp_injective <| by simp

Erasure of Zero Polynomial Yields Zero

Informal description

For any natural number $n$, the operation of erasing the term of degree $n$ from the zero polynomial $0 \in R[X]$ results in the zero polynomial, i.e., $\operatorname{erase}(0, n) = 0$.

Polynomial.erase_monomial theorem

{n : ℕ} {a : R} : erase n (monomial n a) = 0

Full source

@[simp]
theorem erase_monomial {n : ℕ} {a : R} : erase n (monomial n a) = 0 :=
  toFinsupp_injective <| by simp

Erasure of Monomial Yields Zero: $\operatorname{erase}(n, aX^n) = 0$

Informal description

For any natural number $n$ and coefficient $a$ in a semiring $R$, the polynomial obtained by erasing the term of degree $n$ from the monomial $aX^n$ is the zero polynomial, i.e., $\operatorname{erase}(n, aX^n) = 0$.

Polynomial.erase_same theorem

(p : R[X]) (n : ℕ) : coeff (p.erase n) n = 0

Full source

@[simp]
theorem erase_same (p : R[X]) (n : ℕ) : coeff (p.erase n) n = 0 := by simp [coeff_erase]

Coefficient Vanishing After Term Erasure: $\text{coeff}(\text{erase}(p, n), n) = 0$

Informal description

For any polynomial $p \in R[X]$ and natural number $n$, the coefficient of $X^n$ in the polynomial obtained by erasing the term of degree $n$ from $p$ is zero, i.e., $(p.\text{erase}(n)).\text{coeff}(n) = 0$.

Polynomial.erase_ne theorem

(p : R[X]) (n i : ℕ) (h : i ≠ n) : coeff (p.erase n) i = coeff p i

Full source

@[simp]
theorem erase_ne (p : R[X]) (n i : ℕ) (h : i ≠ n) : coeff (p.erase n) i = coeff p i := by
  simp [coeff_erase, h]

Coefficient Preservation Under Polynomial Term Erasure for Unequal Degrees

Informal description

For any polynomial $p \in R[X]$, natural numbers $n$ and $i$ with $i \neq n$, the coefficient of $X^i$ in the polynomial obtained by erasing the term of degree $n$ from $p$ is equal to the coefficient of $X^i$ in $p$. That is, \[ (p.\text{erase}(n)).\text{coeff}(i) = p.\text{coeff}(i). \]

Polynomial.update definition

(p : R[X]) (n : ℕ) (a : R) : R[X]

Full source

/-- Replace the coefficient of a `p : R[X]` at a given degree `n : ℕ`
by a given value `a : R`. If `a = 0`, this is equal to `p.erase n`
If `p.natDegree < n` and `a ≠ 0`, this increases the degree to `n`. -/
def update (p : R[X]) (n : ℕ) (a : R) : R[X] :=
  Polynomial.ofFinsupp (p.toFinsupp.update n a)

Update coefficient of a polynomial at a given degree

Informal description

Given a polynomial $p \in R[X]$, a natural number $n$, and an element $a \in R$, the function `Polynomial.update p n a` returns a new polynomial obtained by replacing the coefficient of $X^n$ in $p$ with $a$. If $a = 0$, this is equivalent to removing the term of degree $n$ from $p$ (if it exists). If $a \neq 0$ and $p$ has no term of degree $n$, this operation adds a new term $aX^n$ to the polynomial, potentially increasing its degree to $n$.

Polynomial.coeff_update theorem

(p : R[X]) (n : ℕ) (a : R) : (p.update n a).coeff = Function.update p.coeff n a

Full source

theorem coeff_update (p : R[X]) (n : ℕ) (a : R) :
    (p.update n a).coeff = Function.update p.coeff n a := by
  ext
  cases p
  simp only [coeff, update, Function.update_apply, coe_update]

Coefficient Function of Updated Polynomial Equals Pointwise Update

Informal description

For any polynomial $p \in R[X]$, natural number $n$, and element $a \in R$, the coefficient function of the updated polynomial $p.\text{update}\,n\,a$ is equal to the pointwise update of the coefficient function of $p$ at $n$ with value $a$. That is, for all $i \in \mathbb{N}$, \[ (p.\text{update}\,n\,a).\text{coeff}\,i = \begin{cases} a & \text{if } i = n, \\ p.\text{coeff}\,i & \text{otherwise.} \end{cases} \]

Polynomial.coeff_update_apply theorem

(p : R[X]) (n : ℕ) (a : R) (i : ℕ) : (p.update n a).coeff i = if i = n then a else p.coeff i

Full source

theorem coeff_update_apply (p : R[X]) (n : ℕ) (a : R) (i : ℕ) :
    (p.update n a).coeff i = if i = n then a else p.coeff i := by
  rw [coeff_update, Function.update_apply]

Coefficient of Updated Polynomial at Degree $i$

Informal description

For any polynomial $p \in R[X]$, natural numbers $n$ and $i$, and element $a \in R$, the coefficient of $X^i$ in the updated polynomial $p.\text{update}\,n\,a$ is given by: \[ (p.\text{update}\,n\,a).\text{coeff}\,i = \begin{cases} a & \text{if } i = n, \\ p.\text{coeff}\,i & \text{otherwise.} \end{cases} \]

Polynomial.coeff_update_same theorem

(p : R[X]) (n : ℕ) (a : R) : (p.update n a).coeff n = a

Full source

@[simp]
theorem coeff_update_same (p : R[X]) (n : ℕ) (a : R) : (p.update n a).coeff n = a := by
  rw [p.coeff_update_apply, if_pos rfl]

Coefficient Update Identity: $(p.\text{update}\,n\,a).\text{coeff}\,n = a$

Informal description

For any polynomial $p \in R[X]$, natural number $n$, and element $a \in R$, the coefficient of $X^n$ in the updated polynomial $p.\text{update}\,n\,a$ is equal to $a$.

Polynomial.coeff_update_ne theorem

(p : R[X]) {n : ℕ} (a : R) {i : ℕ} (h : i ≠ n) : (p.update n a).coeff i = p.coeff i

Full source

theorem coeff_update_ne (p : R[X]) {n : ℕ} (a : R) {i : ℕ} (h : i ≠ n) :
    (p.update n a).coeff i = p.coeff i := by rw [p.coeff_update_apply, if_neg h]

Coefficient Preservation in Polynomial Update for $i \neq n$

Informal description

For any polynomial $p \in R[X]$, natural number $n$, element $a \in R$, and natural number $i \neq n$, the coefficient of $X^i$ in the updated polynomial $p.\text{update}\,n\,a$ is equal to the coefficient of $X^i$ in the original polynomial $p$, i.e., \[ (p.\text{update}\,n\,a).\text{coeff}\,i = p.\text{coeff}\,i. \]

Polynomial.update_zero_eq_erase theorem

(p : R[X]) (n : ℕ) : p.update n 0 = p.erase n

Full source

@[simp]
theorem update_zero_eq_erase (p : R[X]) (n : ℕ) : p.update n 0 = p.erase n := by
  ext
  rw [coeff_update_apply, coeff_erase]

Equivalence of Zero Update and Term Erasure in Polynomials

Informal description

For any polynomial $p \in R[X]$ and natural number $n$, updating the coefficient of $X^n$ in $p$ to zero is equivalent to erasing the term of degree $n$ from $p$, i.e., \[ p.\text{update}(n, 0) = p.\text{erase}(n). \]

Polynomial.support_update theorem

 (p : R[X]) (n : ℕ) (a : R) [Decidable (a = 0)] :
  support (p.update n a) = if a = 0 then p.support.erase n else insert n p.support

Full source

theorem support_update (p : R[X]) (n : ℕ) (a : R) [Decidable (a = 0)] :
    support (p.update n a) = if a = 0 then p.support.erase n else insert n p.support := by
  classical
    cases p
    simp only [support, update, Finsupp.support_update]
    congr

Support of Updated Polynomial: $\text{support}(p.\text{update}(n, a)) = \text{if } a = 0 \text{ then } \text{support}(p) \setminus \{n\} \text{ else } \{n\} \cup \text{support}(p)$

Informal description

For a polynomial $p \in R[X]$, a natural number $n$, and an element $a \in R$, the support of the updated polynomial $p.\text{update}(n, a)$ is given by: \[ \text{support}(p.\text{update}(n, a)) = \begin{cases} \text{support}(p) \setminus \{n\} & \text{if } a = 0 \\ \{n\} \cup \text{support}(p) & \text{otherwise} \end{cases} \]

Polynomial.support_update_zero theorem

(p : R[X]) (n : ℕ) : support (p.update n 0) = p.support.erase n

Full source

theorem support_update_zero (p : R[X]) (n : ℕ) : support (p.update n 0) = p.support.erase n := by
  rw [update_zero_eq_erase, support_erase]

Support After Zero Update Equals Support Minus Degree

Informal description

For any polynomial $p \in R[X]$ and natural number $n$, the support of the polynomial obtained by updating the coefficient of $X^n$ to zero is equal to the support of $p$ with $n$ removed. That is, \[ \text{support}(p.\text{update}(n, 0)) = \text{support}(p) \setminus \{n\}. \]

Polynomial.support_update_ne_zero theorem

(p : R[X]) (n : ℕ) {a : R} (ha : a ≠ 0) : support (p.update n a) = insert n p.support

Full source

theorem support_update_ne_zero (p : R[X]) (n : ℕ) {a : R} (ha : a ≠ 0) :
    support (p.update n a) = insert n p.support := by classical rw [support_update, if_neg ha]

Support of Polynomial Update with Nonzero Coefficient: $\text{support}(p.\text{update}(n, a)) = \{n\} \cup \text{support}(p)$ for $a \neq 0$

Informal description

For a polynomial $p \in R[X]$, a natural number $n$, and a nonzero element $a \in R$, the support of the updated polynomial $p.\text{update}(n, a)$ is equal to the union of $\{n\}$ with the support of $p$, i.e., \[ \text{support}(p.\text{update}(n, a)) = \{n\} \cup \text{support}(p). \]

Polynomial.coeffs definition

(p : R[X]) : Finset R

Full source

/-- The finset of nonzero coefficients of a polynomial. -/
def coeffs (p : R[X]) : Finset R :=
  letI := Classical.decEq R
  Finset.image (fun n => p.coeff n) p.support

Set of nonzero coefficients of a polynomial

Informal description

For a polynomial $ p \in R[X] $, the set of coefficients of $ p $ is the finite set of all nonzero coefficients $ a_n $ of $ p $, where $ a_n $ is the coefficient of the term $ X^n $. This set is obtained by applying the coefficient function to each exponent in the support of $ p $ (the set of exponents with nonzero coefficients).

Polynomial.coeffs_zero theorem

: coeffs (0 : R[X]) = ∅

Full source

@[simp]
theorem coeffs_zero : coeffs (0 : R[X]) = ∅ :=
  rfl

Zero Polynomial Has No Nonzero Coefficients

Informal description

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

Polynomial.mem_coeffs_iff theorem

{p : R[X]} {c : R} : c ∈ p.coeffs ↔ ∃ n ∈ p.support, c = p.coeff n

Full source

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

Characterization of Membership in Polynomial Coefficients

Informal description

For any polynomial $p \in R[X]$ and any coefficient $c \in R$, the coefficient $c$ belongs to the set of nonzero coefficients of $p$ if and only if there exists a natural number $n$ in the support of $p$ such that $c$ is the coefficient of the term $X^n$ in $p$.

Polynomial.coeffs_one theorem

: coeffs (1 : R[X]) ⊆ { 1 }

Full source

theorem coeffs_one : coeffscoeffs (1 : R[X]) ⊆ {1} := by
  classical
  simp_rw [coeffs, Finset.image_subset_iff]
  simp_all [coeff_one]

Coefficient Set of Constant Polynomial 1 is Subset of $\{1\}$

Informal description

The set of nonzero coefficients of the constant polynomial $1 \in R[X]$ is a subset of the singleton set $\{1\}$.

Polynomial.coeff_mem_coeffs theorem

(p : R[X]) (n : ℕ) (h : p.coeff n ≠ 0) : p.coeff n ∈ p.coeffs

Full source

theorem coeff_mem_coeffs (p : R[X]) (n : ℕ) (h : p.coeff n ≠ 0) : p.coeff n ∈ p.coeffs := by
  classical
  simp only [coeffs, exists_prop, mem_support_iff, Finset.mem_image, Ne]
  exact ⟨n, h, rfl⟩

Nonzero Coefficients Belong to Coefficient Set

Informal description

For any polynomial $p \in R[X]$ and natural number $n$, if the coefficient of $X^n$ in $p$ is nonzero (i.e., $p_n \neq 0$), then $p_n$ belongs to the set of nonzero coefficients of $p$.

Polynomial.coeffs_monomial theorem

(n : ℕ) {c : R} (hc : c ≠ 0) : (monomial n c).coeffs = { c }

Full source

theorem coeffs_monomial (n : ℕ) {c : R} (hc : c ≠ 0) : (monomial n c).coeffs = {c} := by
  rw [coeffs, support_monomial n hc]
  simp

Nonzero Coefficients of Monomial Form Singleton Set

Informal description

For any natural number $n$ and nonzero element $c$ in a semiring $R$, the set of nonzero coefficients of the monomial $c X^n$ is the singleton set $\{c\}$.

Polynomial.commSemiring instance

: CommSemiring R[X]

Full source

instance commSemiring : CommSemiring R[X] :=
  fast_instance% { Function.Injective.commSemigroup toFinsupp toFinsupp_injective toFinsupp_mul with
    toSemiring := Polynomial.semiring }

Commutative Semiring Structure on Polynomial Ring $R[X]$

Informal description

The ring of univariate polynomials $R[X]$ over a commutative semiring $R$ forms a commutative semiring, where addition and multiplication are defined in the usual way for polynomials and multiplication is commutative.

Polynomial.instZSMul instance

: SMul ℤ R[X]

Full source

instance instZSMul : SMul ℤ R[X] where
  smul r p := ⟨r • p.toFinsupp⟩

Integer Scalar Multiplication on Polynomials

Informal description

The ring of univariate polynomials $R[X]$ over a semiring $R$ is equipped with a scalar multiplication operation by integers, where for any integer $a \in \mathbb{Z}$ and polynomial $p \in R[X]$, the scalar multiplication $a \cdot p$ is defined componentwise on the coefficients of $p$.

Polynomial.ofFinsupp_zsmul theorem

(a : ℤ) (b) : (⟨a • b⟩ : R[X]) = (a • ⟨b⟩ : R[X])

Full source

@[simp]
theorem ofFinsupp_zsmul (a : ℤ) (b) :
    (⟨a • b⟩ : R[X]) = (a • ⟨b⟩ : R[X]) :=
  rfl

Compatibility of Polynomial Construction with Integer Scalar Multiplication

Informal description

For any integer $a \in \mathbb{Z}$ and any element $b$ of the additive monoid algebra $R[\mathbb{N}]$, the polynomial constructed from the scalar multiple $a \cdot b$ is equal to the scalar multiple $a$ applied to the polynomial constructed from $b$. In other words, the construction of polynomials from additive monoid algebra elements commutes with integer scalar multiplication.

Polynomial.toFinsupp_zsmul theorem

(a : ℤ) (b : R[X]) : (a • b).toFinsupp = a • b.toFinsupp

Full source

@[simp]
theorem toFinsupp_zsmul (a : ℤ) (b : R[X]) :
    (a • b).toFinsupp = a • b.toFinsupp :=
  rfl

Compatibility of Integer Scalar Multiplication with Polynomial-to-AddMonoidAlgebra Conversion

Informal description

For any integer $a$ and any polynomial $b \in R[X]$, the image of the scalar multiple $a \cdot b$ under the conversion to the additive monoid algebra $R[\mathbb{N}]$ is equal to the scalar multiple $a \cdot b$ in $R[\mathbb{N}]$, where $b$ is considered as an element of $R[\mathbb{N}]$.

Polynomial.instIntCast instance

: IntCast R[X]

Full source

instance instIntCast : IntCast R[X] where intCast n := ofFinsupp n

Integer Casting in Polynomial Rings

Informal description

The ring of univariate polynomials $R[X]$ over a semiring $R$ has a canonical integer casting operation, where each integer $z \in \mathbb{Z}$ is mapped to the constant polynomial $z \cdot 1_R$ in $R[X]$.

Polynomial.ofFinsupp_intCast theorem

(z : ℤ) : (⟨z⟩ : R[X]) = z

Full source

@[simp]
theorem ofFinsupp_intCast (z : ℤ) : (⟨z⟩ : R[X]) = z := rfl

Integer Casting via `ofFinsupp` Yields Constant Polynomial

Informal description

For any integer $z \in \mathbb{Z}$, the polynomial obtained by casting $z$ into the polynomial ring $R[X]$ via the `ofFinsupp` construction is equal to the constant polynomial $z$.

Polynomial.toFinsupp_intCast theorem

(z : ℤ) : (z : R[X]).toFinsupp = z

Full source

@[simp]
theorem toFinsupp_intCast (z : ℤ) : (z : R[X]).toFinsupp = z := rfl

Integer Casting Correspondence in Polynomial Rings: $(z : R[X]) \leftrightarrow z$ in $R[\mathbb{N}]$

Informal description

For any integer $z \in \mathbb{Z}$, the image of $z$ under the canonical map from $\mathbb{Z}$ to the polynomial ring $R[X]$ corresponds to $z$ when viewed in the additive monoid algebra $R[\mathbb{N}]$ via the `toFinsupp` isomorphism. In other words, the coefficient function representation of the constant polynomial $z$ in $R[X]$ is exactly the integer $z$ itself.

Polynomial.ring instance

: Ring R[X]

Full source

instance ring : Ring R[X] :=
  fast_instance% Function.Injective.ring toFinsupp toFinsupp_injective (toFinsupp_zero (R := R))
      toFinsupp_one toFinsupp_add
      toFinsupp_mul toFinsupp_neg toFinsupp_sub (fun _ _ => toFinsupp_nsmul _ _)
      (fun _ _ => toFinsupp_zsmul _ _) toFinsupp_pow (fun _ => rfl) fun _ => rfl

Polynomial Ring Structure

Informal description

For any ring $R$, the polynomial ring $R[X]$ forms a ring under the usual addition and multiplication of polynomials.

Polynomial.coeff_neg theorem

(p : R[X]) (n : ℕ) : coeff (-p) n = -coeff p n

Full source

@[simp]
theorem coeff_neg (p : R[X]) (n : ℕ) : coeff (-p) n = -coeff p n := by
  rcases p with ⟨⟩
  rw [← ofFinsupp_neg, coeff, coeff, Finsupp.neg_apply]

Negation of Polynomial Coefficients: $(-p)_n = -p_n$

Informal description

For any polynomial $p \in R[X]$ over a ring $R$ and any natural number $n$, the coefficient of $X^n$ in the negated polynomial $-p$ is equal to the negation of the coefficient of $X^n$ in $p$, i.e., $$(-p)_n = -p_n.$$

Polynomial.coeff_sub theorem

(p q : R[X]) (n : ℕ) : coeff (p - q) n = coeff p n - coeff q n

Full source

@[simp]
theorem coeff_sub (p q : R[X]) (n : ℕ) : coeff (p - q) n = coeff p n - coeff q n := by
  rcases p with ⟨⟩
  rcases q with ⟨⟩
  rw [← ofFinsupp_sub, coeff, coeff, coeff, Finsupp.sub_apply]

Coefficient-wise subtraction of polynomials: $(p - q)_n = p_n - q_n$

Informal description

For any polynomials $p, q \in R[X]$ over a ring $R$ and any natural number $n$, the coefficient of $X^n$ in the difference polynomial $p - q$ is equal to the difference of the coefficients of $X^n$ in $p$ and $q$, i.e., $$(p - q)_n = p_n - q_n.$$

Polynomial.monomial_neg theorem

(n : ℕ) (a : R) : monomial n (-a) = -monomial n a

Full source

@[simp]
theorem monomial_neg (n : ℕ) (a : R) : monomial n (-a) = -monomial n a := by
  rw [eq_neg_iff_add_eq_zero, ← monomial_add, neg_add_cancel, monomial_zero_right]

Negation of Monomial: $(-a)X^n = -(a X^n)$

Informal description

For any natural number $n$ and element $a$ in a ring $R$, the monomial $-a X^n$ is equal to the negation of the monomial $a X^n$ in the polynomial ring $R[X]$, i.e., $$(-a)X^n = -(a X^n).$$

Polynomial.monomial_sub theorem

(n : ℕ) : monomial n (a - b) = monomial n a - monomial n b

Full source

theorem monomial_sub (n : ℕ) : monomial n (a - b) = monomial n a - monomial n b := by
  rw [sub_eq_add_neg, monomial_add, monomial_neg, sub_eq_add_neg]

Subtraction of Monomials: $(a - b)X^n = aX^n - bX^n$

Informal description

For any natural number $n$ and elements $a, b$ in a ring $R$, the monomial $(a - b)X^n$ is equal to the difference of the monomials $aX^n$ and $bX^n$ in the polynomial ring $R[X]$, i.e., $$(a - b)X^n = aX^n - bX^n.$$

Polynomial.support_neg theorem

{p : R[X]} : (-p).support = p.support

Full source

@[simp]
theorem support_neg {p : R[X]} : (-p).support = p.support := by
  rcases p with ⟨⟩
  rw [← ofFinsupp_neg, support, support, Finsupp.support_neg]

Support Invariance under Negation: $\text{supp}(-p) = \text{supp}(p)$

Informal description

For any polynomial $p \in R[X]$ over a ring $R$, the support of the negated polynomial $-p$ is equal to the support of $p$. That is, the set of exponents with nonzero coefficients remains unchanged under negation.

Polynomial.C_eq_intCast theorem

(n : ℤ) : C (n : R) = n

Full source

theorem C_eq_intCast (n : ℤ) : C (n : R) = n := by simp

Constant Polynomial Equals Integer Cast: $C(n) = n$ in $R[X]$

Informal description

For any integer $n \in \mathbb{Z}$ and any ring $R$, the constant polynomial $C(n)$ in the polynomial ring $R[X]$ is equal to the integer $n$ cast as an element of $R[X]$. That is, $C(n) = n$ in $R[X]$.

Polynomial.C_neg theorem

: C (-a) = -C a

Full source

theorem C_neg : C (-a) = -C a :=
  RingHom.map_neg C a

Negation of Constant Polynomials: $C(-a) = -C(a)$

Informal description

For any element $a$ in a ring $R$, the constant polynomial $C(-a)$ is equal to the negation of the constant polynomial $C(a)$, i.e., $C(-a) = -C(a)$.

Polynomial.C_sub theorem

: C (a - b) = C a - C b

Full source

theorem C_sub : C (a - b) = C a - C b :=
  RingHom.map_sub C a b

Subtraction Preservation by Constant Polynomial Homomorphism: $C(a - b) = C(a) - C(b)$

Informal description

For any ring $R$ and elements $a, b \in R$, the constant polynomial homomorphism $C$ satisfies $C(a - b) = C(a) - C(b)$ in the polynomial ring $R[X]$.

Polynomial.commRing instance

[CommRing R] : CommRing R[X]

Full source

instance commRing [CommRing R] : CommRing R[X] :=
  --TODO: add reference to library note in PR https://github.com/leanprover-community/mathlib4/pull/7432
  { toRing := Polynomial.ring
    mul_comm := mul_comm }

Commutative Ring Structure on Polynomial Rings

Informal description

For any commutative ring $R$, the polynomial ring $R[X]$ is also a commutative ring.

Polynomial.nontrivial instance

[Nontrivial R] : Nontrivial R[X]

Full source

instance nontrivial [Nontrivial R] : Nontrivial R[X] := by
  have h : Nontrivial R[ℕ] := by infer_instance
  rcases h.exists_pair_ne with ⟨x, y, hxy⟩
  refine ⟨⟨⟨x⟩, ⟨y⟩, ?_⟩⟩
  simp [hxy]

Nontriviality of Polynomial Rings

Informal description

For any nontrivial semiring $R$, the polynomial ring $R[X]$ is also nontrivial.

Polynomial.X_ne_zero theorem

[Nontrivial R] : (X : R[X]) ≠ 0

Full source

@[simp]
theorem X_ne_zero [Nontrivial R] : (X : R[X]) ≠ 0 :=
  mt (congr_arg fun p => coeff p 1) (by simp)

Nonzero Property of the Polynomial Variable $X$ in Nontrivial Semirings

Informal description

For any nontrivial semiring $R$, the polynomial variable $X$ in the polynomial ring $R[X]$ is not equal to the zero polynomial, i.e., $X \neq 0$.

Polynomial.nnqsmul_eq_C_mul theorem

(q : ℚ≥0) (f : R[X]) : q • f = Polynomial.C (q : R) * f

Full source

lemma nnqsmul_eq_C_mul (q : ℚ≥0) (f : R[X]) : q • f = Polynomial.C (q : R) * f := by
  rw [← NNRat.smul_one_eq_cast, ← Polynomial.smul_C, C_1, smul_one_mul]

Scalar Multiplication by Nonnegative Rationals as Constant Polynomial Multiplication: $q \cdot f = C(q) * f$

Informal description

For any nonnegative rational number $q$ and any polynomial $f \in R[X]$ over a division semiring $R$, the scalar multiplication $q \cdot f$ is equal to the product of the constant polynomial $C(q)$ and $f$, i.e., $$ q \cdot f = C(q) * f. $$

Polynomial.qsmul_eq_C_mul theorem

(a : ℚ) (f : R[X]) : a • f = Polynomial.C (a : R) * f

Full source

theorem qsmul_eq_C_mul (a : ℚ) (f : R[X]) : a • f = Polynomial.C (a : R) * f := by
  rw [← Rat.smul_one_eq_cast, ← Polynomial.smul_C, C_1, smul_one_mul]

Scalar Multiplication by Rationals as Constant Polynomial Multiplication: $a \cdot f = C(a) * f$

Informal description

For any rational number $a$ and any polynomial $f \in R[X]$, the scalar multiplication $a \cdot f$ is equal to the product of the constant polynomial $C(a)$ and $f$, i.e., $$ a \cdot f = C(a) * f. $$

Polynomial.nontrivial_iff theorem

[Semiring R] : Nontrivial R[X] ↔ Nontrivial R

Full source

@[simp]
theorem nontrivial_iff [Semiring R] : NontrivialNontrivial R[X] ↔ Nontrivial R :=
  ⟨fun h =>
    let ⟨_r, _s, hrs⟩ := @exists_pair_ne _ h
    Nontrivial.of_polynomial_ne hrs,
    fun h => @Polynomial.nontrivial _ _ h⟩

Nontriviality Equivalence between Semiring and its Polynomial Ring

Informal description

For any semiring $R$, the polynomial ring $R[X]$ is nontrivial if and only if $R$ is nontrivial.

Polynomial.repr instance

[Repr R] [DecidableEq R] : Repr R[X]

Full source

protected instance repr [Repr R] [DecidableEq R] : Repr R[X] :=
  ⟨fun p prec =>
    let termPrecAndReprs : List (WithTop ℕ × Lean.Format) :=
      List.map (fun
        | 0 => (max_prec, "C " ++ reprArg (coeff p 0))
        | 1 => if coeff p 1 = 1
          then (⊤, "X")
          else (70, "C " ++ reprArg (coeff p 1) ++ " * X")
        | n =>
          if coeff p n = 1
          then (80, "X ^ " ++ Nat.repr n)
          else (70, "C " ++ reprArg (coeff p n) ++ " * X ^ " ++ Nat.repr n))
      (p.support.sort (· ≤ ·))
    match termPrecAndReprs with
    | [] => "0"
    | [(tprec, t)] => if prec ≥ tprec then Lean.Format.paren t else t
    | ts =>
      -- multiple terms, use `+` precedence
      (if prec ≥ 65 then Lean.Format.paren else id)
      (Lean.Format.fill
        (Lean.Format.joinSep (ts.map Prod.snd) (" +" ++ Lean.Format.line)))⟩

Representation of Polynomials over a Semiring with Decidable Equality

Informal description

For any semiring $R$ with a decidable equality and a representation of its elements, the polynomial ring $R[X]$ has a canonical representation of its elements.

Mathlib.Algebra.Polynomial.Basic

Main definitions

Implementation