doc-next-gen

Mathlib.Algebra.Polynomial.Coeff

Module docstring

{"# Theory of univariate polynomials

The theorems include formulas for computing coefficients, such as coeff_add, coeff_sum, coeff_mul

"}

Polynomial.coeff_add theorem
(p q : R[X]) (n : ℕ) : coeff (p + q) n = coeff p n + coeff q n
Full source 
@[simp]
theorem coeff_add (p q : R[X]) (n : ℕ) : coeff (p + q) n = coeff p n + coeff q n := by
  rcases p with ⟨⟩
  rcases q with ⟨⟩
  simp_rw [← ofFinsupp_add, coeff]
  exact Finsupp.add_apply _ _ _
Coefficient-wise Addition of Polynomials: $(p + q)_n = p_n + q_n$
Informal description
For any polynomials $p, q \in R[X]$ and any natural number $n$, the coefficient of $X^n$ in the sum $p + q$ is equal to the sum of the coefficients of $X^n$ in $p$ and $q$, i.e., $$(p + q)_n = p_n + q_n.$$
Polynomial.coeff_smul theorem
[SMulZeroClass S R] (r : S) (p : R[X]) (n : ℕ) : coeff (r • p) n = r • coeff p n
Full source 
@[simp]
theorem coeff_smul [SMulZeroClass S R] (r : S) (p : R[X]) (n : ℕ) :
    coeff (r • p) n = r • coeff p n := by
  rcases p with ⟨⟩
  simp_rw [← ofFinsupp_smul, coeff]
  exact Finsupp.smul_apply _ _ _
Coefficient-wise Scalar Multiplication of Polynomials: $(r \cdot p)_n = r \cdot p_n$
Informal description
Let $R$ be a semiring and $S$ a type with a scalar multiplication action on $R$ that preserves zero. For any scalar $r \in S$, polynomial $p \in R[X]$, and natural number $n$, the coefficient of $X^n$ in the scalar multiple $r \cdot p$ is equal to the scalar multiple of the coefficient of $X^n$ in $p$, i.e., $$(r \cdot p)_n = r \cdot p_n.$$
Polynomial.support_smul theorem
[SMulZeroClass S R] (r : S) (p : R[X]) : support (r • p) ⊆ support p
Full source 
theorem support_smul [SMulZeroClass S R] (r : S) (p : R[X]) :
    supportsupport (r • p) ⊆ support p := by
  intro i hi
  simp? [mem_support_iff] at hi ⊢ says simp only [mem_support_iff, coeff_smul, ne_eq] at hi ⊢
  contrapose! hi
  simp [hi]
Support Inclusion under Scalar Multiplication: $\text{support}(r \cdot p) \subseteq \text{support}(p)$
Informal description
Let $R$ be a semiring and $S$ a type with a scalar multiplication action on $R$ that preserves zero. For any scalar $r \in S$ and polynomial $p \in R[X]$, the support of the scalar multiple $r \cdot p$ is a subset of the support of $p$, i.e., $$\text{support}(r \cdot p) \subseteq \text{support}(p).$$
Polynomial.card_support_mul_le theorem
: #(p * q).support ≤ #p.support * #q.support
Full source 
theorem card_support_mul_le : #(p * q).support ≤ #p.support * #q.support := by
  calc #(p * q).support
   _ = #(p.toFinsupp * q.toFinsupp).support := by rw [← support_toFinsupp, toFinsupp_mul]
   _ ≤ #(p.toFinsupp.support + q.toFinsupp.support) :=
    Finset.card_le_card (AddMonoidAlgebra.support_mul p.toFinsupp q.toFinsupp)
   _ ≤ #p.support * #q.support := Finset.card_image₂_le ..
Cardinality Bound for Support of Polynomial Product: $\#(p \cdot q).\text{support} \leq \#p.\text{support} \cdot \#q.\text{support}$
Informal description
For any two polynomials $p$ and $q$ over a semiring $R$, the cardinality of the support of their product is at most the product of the cardinalities of their supports, i.e., \[ \#(p \cdot q).\text{support} \leq \#p.\text{support} \cdot \#q.\text{support}. \]
Polynomial.lsum definition
{R A M : Type*} [Semiring R] [Semiring A] [AddCommMonoid M] [Module R A] [Module R M] (f : ℕ → A →ₗ[R] M) : A[X] →ₗ[R] M
Full source 
/-- `Polynomial.sum` as a linear map. -/
@[simps]
def lsum {R A M : Type*} [Semiring R] [Semiring A] [AddCommMonoid M] [Module R A] [Module R M]
    (f : ℕ → A →ₗ[R] M) : A[X]A[X] →ₗ[R] M where
  toFun p := p.sum (f · ·)
  map_add' p q := sum_add_index p q _ (fun n => (f n).map_zero) fun n _ _ => (f n).map_add _ _
  map_smul' c p := by
    rw [sum_eq_of_subset (f · ·) (fun n => (f n).map_zero) (support_smul c p)]
    simp only [sum_def, Finset.smul_sum, coeff_smul, LinearMap.map_smul, RingHom.id_apply]
Linear sum map on polynomials
Informal description
Given a semiring $R$, a semiring $A$, and an additive commutative monoid $M$ equipped with $R$-module structures on both $A$ and $M$, and given a family of $R$-linear maps $f_n : A \to M$ indexed by natural numbers, the function `Polynomial.lsum` constructs an $R$-linear map from the polynomial ring $A[X]$ to $M$. For any polynomial $p \in A[X]$, this map evaluates to the finite sum $\sum_{n \in \text{support}(p)} f_n (a_n)$, where $a_n$ is the coefficient of $X^n$ in $p$.
Polynomial.lcoeff definition
(n : ℕ) : R[X] →ₗ[R] R
Full source 
/-- The nth coefficient, as a linear map. -/
def lcoeff (n : ℕ) : R[X]R[X] →ₗ[R] R where
  toFun p := coeff p n
  map_add' p q := coeff_add p q n
  map_smul' r p := coeff_smul r p n
Linear coefficient extraction map at degree $n$
Informal description
For a given natural number $n$, the linear map $\text{lcoeff}_n \colon R[X] \to R$ sends a polynomial $p$ to its coefficient of $X^n$, denoted $\text{coeff}(p, n)$. This map is linear with respect to the semiring $R$, meaning it satisfies: 1. Additivity: $\text{lcoeff}_n(p + q) = \text{lcoeff}_n(p) + \text{lcoeff}_n(q)$ for all polynomials $p, q \in R[X]$ 2. Homogeneity: $\text{lcoeff}_n(r \cdot p) = r \cdot \text{lcoeff}_n(p)$ for all $r \in R$ and $p \in R[X]$
Polynomial.lcoeff_apply theorem
(n : ℕ) (f : R[X]) : lcoeff R n f = coeff f n
Full source 
@[simp]
theorem lcoeff_apply (n : ℕ) (f : R[X]) : lcoeff R n f = coeff f n :=
  rfl
Coefficient Extraction Equality: $\text{lcoeff}_n(f) = \text{coeff}(f, n)$
Informal description
For any natural number $n$ and polynomial $f \in R[X]$, the linear coefficient extraction map $\text{lcoeff}_n$ applied to $f$ equals the coefficient of $X^n$ in $f$, i.e., $\text{lcoeff}_n(f) = \text{coeff}(f, n)$.
Polynomial.finset_sum_coeff theorem
{ι : Type*} (s : Finset ι) (f : ι → R[X]) (n : ℕ) : coeff (∑ b ∈ s, f b) n = ∑ b ∈ s, coeff (f b) n
Full source 
@[simp]
theorem finset_sum_coeff {ι : Type*} (s : Finset ι) (f : ι → R[X]) (n : ℕ) :
    coeff (∑ b ∈ s, f b) n = ∑ b ∈ s, coeff (f b) n :=
  map_sum (lcoeff R n) _ _
Coefficient of Sum of Polynomials Equals Sum of Coefficients
Informal description
For any finite set $s$ of indices of type $\iota$, any family of polynomials $f \colon \iota \to R[X]$, and any natural number $n$, the coefficient of $X^n$ in the sum of polynomials $\sum_{b \in s} f(b)$ is equal to the sum of the coefficients of $X^n$ in each polynomial $f(b)$, i.e., \[ \text{coeff}\left(\sum_{b \in s} f(b), n\right) = \sum_{b \in s} \text{coeff}(f(b), n). \]
Polynomial.coeff_list_sum theorem
(l : List R[X]) (n : ℕ) : l.sum.coeff n = (l.map (lcoeff R n)).sum
Full source 
lemma coeff_list_sum (l : List R[X]) (n : ℕ) :
    l.sum.coeff n = (l.map (lcoeff R n)).sum :=
  map_list_sum (lcoeff R n) _
Coefficient of Sum of Polynomials in a List
Informal description
For any list $l$ of polynomials in $R[X]$ and any natural number $n$, the coefficient of $X^n$ in the sum of the polynomials in $l$ is equal to the sum of the coefficients of $X^n$ in each polynomial in $l$. In other words: \[ \text{coeff}\left(\sum_{p \in l} p, n\right) = \sum_{p \in l} \text{coeff}(p, n) \]
Polynomial.coeff_list_sum_map theorem
{ι : Type*} (l : List ι) (f : ι → R[X]) (n : ℕ) : (l.map f).sum.coeff n = (l.map (fun a => (f a).coeff n)).sum
Full source 
lemma coeff_list_sum_map {ι : Type*} (l : List ι) (f : ι → R[X]) (n : ℕ) :
    (l.map f).sum.coeff n = (l.map (fun a => (f a).coeff n)).sum := by
  simp_rw [coeff_list_sum, List.map_map, Function.comp_def, lcoeff_apply]
Coefficient of Sum of Mapped Polynomials Equals Sum of Coefficients
Informal description
For any list $l$ of elements of type $\iota$, any function $f \colon \iota \to R[X]$ mapping elements to polynomials, and any natural number $n$, the coefficient of $X^n$ in the sum of the polynomials obtained by applying $f$ to each element of $l$ is equal to the sum of the coefficients of $X^n$ in each polynomial $f(a)$ for $a \in l$. In other words: \[ \text{coeff}\left(\sum_{a \in l} f(a), n\right) = \sum_{a \in l} \text{coeff}(f(a), n). \]
Polynomial.coeff_sum theorem
[Semiring S] (n : ℕ) (f : ℕ → R → S[X]) : coeff (p.sum f) n = p.sum fun a b => coeff (f a b) n
Full source 
@[simp]
theorem coeff_sum [Semiring S] (n : ℕ) (f : ℕ → R → S[X]) :
    coeff (p.sum f) n = p.sum fun a b => coeff (f a b) n := by
  rcases p with ⟨⟩
  simp [Polynomial.sum, support_ofFinsupp, coeff_ofFinsupp]
Coefficient of Sum of Polynomial-Valued Functions Equals Sum of Coefficients
Informal description
Let $R$ and $S$ be semirings, and let $p \in R[X]$ be a univariate polynomial over $R$. For any natural number $n$ and any function $f \colon \mathbb{N} \to R \to S[X]$, the coefficient of $X^n$ in the sum $\sum_{a \in p.\text{support}} f(a, p_a)$ is equal to the sum $\sum_{a \in p.\text{support}} \text{coeff}(f(a, p_a), n)$, where $p_a$ denotes the coefficient of $X^a$ in $p$.
Polynomial.coeff_mul theorem
(p q : R[X]) (n : ℕ) : coeff (p * q) n = ∑ x ∈ antidiagonal n, coeff p x.1 * coeff q x.2
Full source 
/-- Decomposes the coefficient of the product `p * q` as a sum
over `antidiagonal`. A version which sums over `range (n + 1)` can be obtained
by using `Finset.Nat.sum_antidiagonal_eq_sum_range_succ`. -/
theorem coeff_mul (p q : R[X]) (n : ℕ) :
    coeff (p * q) n = ∑ x ∈ antidiagonal n, coeff p x.1 * coeff q x.2 := by
  rcases p with ⟨p⟩; rcases q with ⟨q⟩
  simp_rw [← ofFinsupp_mul, coeff]
  exact AddMonoidAlgebra.mul_apply_antidiagonal p q n _ Finset.mem_antidiagonal
Coefficient Formula for Polynomial Multiplication via Antidiagonal Sum
Informal description
Let $R$ be a semiring and let $p, q \in R[X]$ be univariate polynomials over $R$. For any natural number $n$, the coefficient of $X^n$ in the product $p \cdot q$ is given by the sum over all pairs $(i,j)$ in the antidiagonal of $n$ (i.e., pairs where $i + j = n$) of the product of the coefficient of $X^i$ in $p$ and the coefficient of $X^j$ in $q$. Mathematically, this can be written as: $$(p \cdot q)_n = \sum_{\substack{(i,j) \in \mathbb{N} \times \mathbb{N} \\ i + j = n}} p_i \cdot q_j.$$
Polynomial.mul_coeff_zero theorem
(p q : R[X]) : coeff (p * q) 0 = coeff p 0 * coeff q 0
Full source 
@[simp]
theorem mul_coeff_zero (p q : R[X]) : coeff (p * q) 0 = coeff p 0 * coeff q 0 := by simp [coeff_mul]
Constant Term of Polynomial Product: $(p \cdot q)_0 = p_0 \cdot q_0$
Informal description
For any two univariate polynomials $p$ and $q$ over a semiring $R$, the coefficient of $X^0$ in their product $p \cdot q$ is equal to the product of their constant terms, i.e., $(p \cdot q)_0 = p_0 \cdot q_0$.
Polynomial.mul_coeff_one theorem
(p q : R[X]) : coeff (p * q) 1 = coeff p 0 * coeff q 1 + coeff p 1 * coeff q 0
Full source 
theorem mul_coeff_one (p q : R[X]) :
    coeff (p * q) 1 = coeff p 0 * coeff q 1 + coeff p 1 * coeff q 0 := by
  rw [coeff_mul, Nat.antidiagonal_eq_map]
  simp [sum_range_succ]
Coefficient of $X^1$ in Polynomial Product: $(p \cdot q)_1 = p_0 q_1 + p_1 q_0$
Informal description
For any univariate polynomials $p$ and $q$ over a semiring $R$, the coefficient of $X^1$ in the product $p \cdot q$ is given by: $$(p \cdot q)_1 = p_0 \cdot q_1 + p_1 \cdot q_0,$$ where $p_i$ and $q_i$ denote the coefficients of $X^i$ in $p$ and $q$ respectively.
Polynomial.constantCoeff definition
: R[X] →+* R
Full source 
/-- `constantCoeff p` returns the constant term of the polynomial `p`,
  defined as `coeff p 0`. This is a ring homomorphism. -/
@[simps]
def constantCoeff : R[X]R[X] →+* R where
  toFun p := coeff p 0
  map_one' := coeff_one_zero
  map_mul' := mul_coeff_zero
  map_zero' := coeff_zero 0
  map_add' p q := coeff_add p q 0
Constant term ring homomorphism of a polynomial
Informal description
The function `constantCoeff` maps a polynomial $p \in R[X]$ to its constant term, defined as the coefficient of $X^0$ in $p$. This function is a ring homomorphism, meaning it satisfies: - $\text{constantCoeff}(1) = 1$ (preservation of multiplicative identity) - $\text{constantCoeff}(p \cdot q) = \text{constantCoeff}(p) \cdot \text{constantCoeff}(q)$ (multiplicative preservation) - $\text{constantCoeff}(0) = 0$ (preservation of zero) - $\text{constantCoeff}(p + q) = \text{constantCoeff}(p) + \text{constantCoeff}(q)$ (additive preservation)
Polynomial.coeff_mul_X_zero theorem
(p : R[X]) : coeff (p * X) 0 = 0
Full source 
theorem coeff_mul_X_zero (p : R[X]) : coeff (p * X) 0 = 0 := by simp
Vanishing Constant Term in $p \cdot X$: $(p \cdot X)_0 = 0$
Informal description
For any univariate polynomial $p$ over a semiring $R$, the coefficient of $X^0$ in the product $p \cdot X$ is $0$.
Polynomial.coeff_X_mul_zero theorem
(p : R[X]) : coeff (X * p) 0 = 0
Full source 
theorem coeff_X_mul_zero (p : R[X]) : coeff (X * p) 0 = 0 := by simp
Vanishing Constant Term in $X \cdot p$: $(X \cdot p)_0 = 0$
Informal description
For any univariate polynomial $p$ over a semiring $R$, the coefficient of $X^0$ in the product $X \cdot p$ is $0$.
Polynomial.coeff_C_mul_X_pow theorem
(x : R) (k n : ℕ) : coeff (C x * X ^ k : R[X]) n = if n = k then x else 0
Full source 
theorem coeff_C_mul_X_pow (x : R) (k n : ℕ) :
    coeff (C x * X ^ k : R[X]) n = if n = k then x else 0 := by
  rw [C_mul_X_pow_eq_monomial, coeff_monomial]
  congr 1
  simp [eq_comm]
Coefficient Formula for Monomial $x X^k$: $\text{coeff}(x X^k, n) = x \delta_{n,k}$
Informal description
For any element $x$ in a semiring $R$ and natural numbers $k, n$, the coefficient of $X^n$ in the polynomial $x \cdot X^k$ is equal to $x$ if $n = k$, and $0$ otherwise. In mathematical notation: $$\text{coeff}(x X^k, n) = \begin{cases} x & \text{if } n = k \\ 0 & \text{otherwise} \end{cases}$$
Polynomial.coeff_C_mul_X theorem
(x : R) (n : ℕ) : coeff (C x * X : R[X]) n = if n = 1 then x else 0
Full source 
theorem coeff_C_mul_X (x : R) (n : ℕ) : coeff (C x * X : R[X]) n = if n = 1 then x else 0 := by
  rw [← pow_one X, coeff_C_mul_X_pow]
Coefficient Formula for Linear Monomial: $\text{coeff}(x X, n) = x \delta_{n,1}$
Informal description
For any element $x$ in a semiring $R$ and any natural number $n$, the coefficient of $X^n$ in the polynomial $x \cdot X$ is equal to $x$ if $n = 1$, and $0$ otherwise. In mathematical notation: $$\text{coeff}(x X, n) = \begin{cases} x & \text{if } n = 1 \\ 0 & \text{otherwise} \end{cases}$$
Polynomial.coeff_C_mul theorem
(p : R[X]) : coeff (C a * p) n = a * coeff p n
Full source 
@[simp]
theorem coeff_C_mul (p : R[X]) : coeff (C a * p) n = a * coeff p n := by
  rcases p with ⟨p⟩
  simp_rw [← monomial_zero_left, ← ofFinsupp_single, ← ofFinsupp_mul, coeff]
  exact AddMonoidAlgebra.single_zero_mul_apply p a n
Coefficient of Constant Multiple: $\text{coeff}(C(a) \cdot p, n) = a \cdot \text{coeff}(p, n)$
Informal description
For any polynomial $p \in R[X]$ and natural number $n$, the coefficient of $X^n$ in the product of the constant polynomial $C(a)$ and $p$ is equal to $a$ multiplied by the coefficient of $X^n$ in $p$. That is, $$\text{coeff}(C(a) \cdot p, n) = a \cdot \text{coeff}(p, n).$$
Polynomial.C_mul' theorem
(a : R) (f : R[X]) : C a * f = a • f
Full source 
theorem C_mul' (a : R) (f : R[X]) : C a * f = a • f := by
  ext
  rw [coeff_C_mul, coeff_smul, smul_eq_mul]
Constant Polynomial Multiplication as Scalar Multiplication: $C(a) \cdot f = a \cdot f$
Informal description
For any element $a$ in a semiring $R$ and any polynomial $f \in R[X]$, the product of the constant polynomial $C(a)$ and $f$ is equal to the scalar multiplication of $a$ and $f$, i.e., $$C(a) \cdot f = a \cdot f.$$
Polynomial.coeff_mul_C theorem
(p : R[X]) (n : ℕ) (a : R) : coeff (p * C a) n = coeff p n * a
Full source 
@[simp]
theorem coeff_mul_C (p : R[X]) (n : ℕ) (a : R) : coeff (p * C a) n = coeff p n * a := by
  rcases p with ⟨p⟩
  simp_rw [← monomial_zero_left, ← ofFinsupp_single, ← ofFinsupp_mul, coeff]
  exact AddMonoidAlgebra.mul_single_zero_apply p a n
Coefficient of Polynomial Multiplied by Constant: $[X^n](p \cdot a) = [X^n]p \cdot a$
Informal description
For any polynomial $p \in R[X]$, natural number $n \in \mathbb{N}$, and element $a \in R$, the coefficient of $X^n$ in the product $p \cdot C(a)$ equals the coefficient of $X^n$ in $p$ multiplied by $a$, i.e., $$[X^n](p \cdot a) = [X^n]p \cdot a.$$
Polynomial.coeff_mul_natCast theorem
{a k : ℕ} : coeff (p * (a : R[X])) k = coeff p k * (↑a : R)
Full source 
@[simp] lemma coeff_mul_natCast {a k : ℕ} :
  coeff (p * (a : R[X])) k = coeff p k * (↑a : R) := coeff_mul_C _ _ _
Coefficient of Polynomial Multiplied by Natural Number: $[X^k](p \cdot a) = [X^k]p \cdot a$
Informal description
For any polynomial $p \in R[X]$, natural numbers $a, k \in \mathbb{N}$, the coefficient of $X^k$ in the product $p \cdot a$ equals the coefficient of $X^k$ in $p$ multiplied by the image of $a$ in $R$, i.e., $$[X^k](p \cdot a) = [X^k]p \cdot a.$$
Polynomial.coeff_natCast_mul theorem
{a k : ℕ} : coeff ((a : R[X]) * p) k = a * coeff p k
Full source 
@[simp] lemma coeff_natCast_mul {a k : ℕ} :
  coeff ((a : R[X]) * p) k = a * coeff p k := coeff_C_mul _
Coefficient of Natural Number Multiple: $[X^k](a \cdot p) = a \cdot [X^k]p$
Informal description
For any natural numbers $a$ and $k$, and any polynomial $p \in R[X]$, the coefficient of $X^k$ in the product of the constant polynomial $a$ and $p$ is equal to $a$ multiplied by the coefficient of $X^k$ in $p$, i.e., $$[X^k](a \cdot p) = a \cdot [X^k]p.$$
Polynomial.coeff_mul_ofNat theorem
{a k : ℕ} [Nat.AtLeastTwo a] : coeff (p * (ofNat(a) : R[X])) k = coeff p k * ofNat(a)
Full source 
@[simp] lemma coeff_mul_ofNat {a k : ℕ} [Nat.AtLeastTwo a] :
  coeff (p * (ofNat(a) : R[X])) k = coeff p k * ofNat(a) := coeff_mul_C _ _ _
Coefficient of Polynomial Multiplied by Numeric Literal ≥ 2: $[X^k](p \cdot a) = [X^k]p \cdot a$
Informal description
For any polynomial $p \in R[X]$, natural numbers $a \geq 2$ and $k \in \mathbb{N}$, the coefficient of $X^k$ in the product $p \cdot a$ equals the coefficient of $X^k$ in $p$ multiplied by $a$, i.e., $$[X^k](p \cdot a) = [X^k]p \cdot a.$$
Polynomial.coeff_ofNat_mul theorem
{a k : ℕ} [Nat.AtLeastTwo a] : coeff ((ofNat(a) : R[X]) * p) k = ofNat(a) * coeff p k
Full source 
@[simp] lemma coeff_ofNat_mul {a k : ℕ} [Nat.AtLeastTwo a] :
  coeff ((ofNat(a) : R[X]) * p) k = ofNat(a) * coeff p k := coeff_C_mul _
Coefficient of Scalar Multiple by Numerals $\geq 2$: $\text{coeff}(a \cdot p, k) = a \cdot \text{coeff}(p, k)$
Informal description
For any natural number $a \geq 2$ and any polynomial $p \in R[X]$, the coefficient of $X^k$ in the product $(a \cdot p)$ is equal to $a$ multiplied by the coefficient of $X^k$ in $p$. That is, $$\text{coeff}(a \cdot p, k) = a \cdot \text{coeff}(p, k).$$
Polynomial.coeff_mul_intCast theorem
[Ring S] {p : S[X]} {a : ℤ} {k : ℕ} : coeff (p * (a : S[X])) k = coeff p k * (↑a : S)
Full source 
@[simp] lemma coeff_mul_intCast [Ring S] {p : S[X]} {a : ℤ} {k : ℕ} :
  coeff (p * (a : S[X])) k = coeff p k * (↑a : S) := coeff_mul_C _ _ _
Coefficient of Polynomial Multiplied by Integer Scalar: $[X^k](p \cdot a) = [X^k]p \cdot a$
Informal description
Let $S$ be a ring, $p \in S[X]$ a polynomial, $a \in \mathbb{Z}$ an integer, and $k \in \mathbb{N}$ a natural number. Then the coefficient of $X^k$ in the product $p \cdot (a \cdot 1_{S[X]})$ equals the coefficient of $X^k$ in $p$ multiplied by the image of $a$ in $S$, i.e., $$[X^k](p \cdot a) = [X^k]p \cdot a.$$
Polynomial.coeff_intCast_mul theorem
[Ring S] {p : S[X]} {a : ℤ} {k : ℕ} : coeff ((a : S[X]) * p) k = a * coeff p k
Full source 
@[simp] lemma coeff_intCast_mul [Ring S] {p : S[X]} {a : ℤ} {k : ℕ} :
  coeff ((a : S[X]) * p) k = a * coeff p k := coeff_C_mul _
Coefficient of Integer-Scaled Polynomial: $\text{coeff}(a \cdot p, k) = a \cdot \text{coeff}(p, k)$
Informal description
Let $S$ be a ring, $p \in S[X]$ a polynomial, $a \in \mathbb{Z}$ an integer, and $k \in \mathbb{N}$ a natural number. Then the coefficient of $X^k$ in the product of the constant polynomial $a$ and $p$ is equal to $a$ multiplied by the coefficient of $X^k$ in $p$, i.e., $$\text{coeff}(a \cdot p, k) = a \cdot \text{coeff}(p, k).$$
Polynomial.coeff_X_pow theorem
(k n : ℕ) : coeff (X ^ k : R[X]) n = if n = k then 1 else 0
Full source 
@[simp]
theorem coeff_X_pow (k n : ℕ) : coeff (X ^ k : R[X]) n = if n = k then 1 else 0 := by
  simp only [one_mul, RingHom.map_one, ← coeff_C_mul_X_pow]
Coefficient of Monomial $X^k$: $\text{coeff}(X^k, n) = \delta_{nk}$
Informal description
For any natural numbers $k$ and $n$, the coefficient of $X^n$ in the polynomial $X^k$ is $1$ if $n = k$ and $0$ otherwise. In other words, $\text{coeff}(X^k, n) = \begin{cases} 1 & \text{if } n = k \\ 0 & \text{otherwise} \end{cases}$.
Polynomial.coeff_X_pow_self theorem
(n : ℕ) : coeff (X ^ n : R[X]) n = 1
Full source 
theorem coeff_X_pow_self (n : ℕ) : coeff (X ^ n : R[X]) n = 1 := by simp
Coefficient of $X^n$ in $X^n$ is 1
Informal description
For any natural number $n$, the coefficient of $X^n$ in the polynomial $X^n$ is $1$. That is, $\text{coeff}(X^n, n) = 1$.
Polynomial.support_binomial theorem
{k m : ℕ} (hkm : k ≠ m) {x y : R} (hx : x ≠ 0) (hy : y ≠ 0) : support (C x * X ^ k + C y * X ^ m) = { k, m }
Full source 
theorem support_binomial {k m : ℕ} (hkm : k ≠ m) {x y : R} (hx : x ≠ 0) (hy : y ≠ 0) :
    support (C x * X ^ k + C y * X ^ m) = {k, m} := by
  apply subset_antisymm (support_binomial' k m x y)
  simp_rw [insert_subset_iff, singleton_subset_iff, mem_support_iff, coeff_add, coeff_C_mul,
    coeff_X_pow_self, mul_one, coeff_X_pow, if_neg hkm, if_neg hkm.symm, mul_zero, zero_add,
    add_zero, Ne, hx, hy, not_false_eq_true, and_true]
Support of Binomial Polynomial with Distinct Exponents and Nonzero Coefficients is $\{k, m\}$
Informal description
For any distinct natural numbers $k$ and $m$, and any nonzero elements $x$ and $y$ in a semiring $R$, the support of the binomial polynomial $x X^k + y X^m$ is exactly the set $\{k, m\}$.
Polynomial.support_trinomial theorem
{k m n : ℕ} (hkm : k < m) (hmn : m < n) {x y z : R} (hx : x ≠ 0) (hy : y ≠ 0) (hz : z ≠ 0) : support (C x * X ^ k + C y * X ^ m + C z * X ^ n) = { k, m, n }
Full source 
theorem support_trinomial {k m n : ℕ} (hkm : k < m) (hmn : m < n) {x y z : R} (hx : x ≠ 0)
    (hy : y ≠ 0) (hz : z ≠ 0) :
    support (C x * X ^ k + C y * X ^ m + C z * X ^ n) = {k, m, n} := by
  apply subset_antisymm (support_trinomial' k m n x y z)
  simp_rw [insert_subset_iff, singleton_subset_iff, mem_support_iff, coeff_add, coeff_C_mul,
    coeff_X_pow_self, mul_one, coeff_X_pow, if_neg hkm.ne, if_neg hkm.ne', if_neg hmn.ne,
    if_neg hmn.ne', if_neg (hkm.trans hmn).ne, if_neg (hkm.trans hmn).ne', mul_zero, add_zero,
    zero_add, Ne, hx, hy, hz, not_false_eq_true, and_true]
Support of Trinomial Polynomial with Distinct Exponents and Nonzero Coefficients
Informal description
For any natural numbers $k < m < n$ and nonzero coefficients $x, y, z$ in a semiring $R$, the support of the trinomial polynomial $x X^k + y X^m + z X^n$ is exactly the set $\{k, m, n\}$.
Polynomial.card_support_binomial theorem
{k m : ℕ} (h : k ≠ m) {x y : R} (hx : x ≠ 0) (hy : y ≠ 0) : #(support (C x * X ^ k + C y * X ^ m)) = 2
Full source 
theorem card_support_binomial {k m : ℕ} (h : k ≠ m) {x y : R} (hx : x ≠ 0) (hy : y ≠ 0) :
    #(support (C x * X ^ k + C y * X ^ m)) = 2 := by
  rw [support_binomial h hx hy, card_insert_of_not_mem (mt mem_singleton.mp h), card_singleton]
Cardinality of Support of Binomial Polynomial is 2
Informal description
For any distinct natural numbers $k$ and $m$, and any nonzero elements $x$ and $y$ in a semiring $R$, the cardinality of the support of the binomial polynomial $x X^k + y X^m$ is equal to 2.
Polynomial.card_support_trinomial theorem
{k m n : ℕ} (hkm : k < m) (hmn : m < n) {x y z : R} (hx : x ≠ 0) (hy : y ≠ 0) (hz : z ≠ 0) : #(support (C x * X ^ k + C y * X ^ m + C z * X ^ n)) = 3
Full source 
theorem card_support_trinomial {k m n : ℕ} (hkm : k < m) (hmn : m < n) {x y z : R} (hx : x ≠ 0)
    (hy : y ≠ 0) (hz : z ≠ 0) : #(support (C x * X ^ k + C y * X ^ m + C z * X ^ n)) = 3 := by
  rw [support_trinomial hkm hmn hx hy hz,
    card_insert_of_not_mem
      (mt mem_insert.mp (not_or_intro hkm.ne (mt mem_singleton.mp (hkm.trans hmn).ne))),
    card_insert_of_not_mem (mt mem_singleton.mp hmn.ne), card_singleton]
Cardinality of Support of Trinomial Polynomial with Distinct Exponents and Nonzero Coefficients is 3
Informal description
For any natural numbers $k < m < n$ and nonzero elements $x, y, z$ in a semiring $R$, the support of the trinomial polynomial $x X^k + y X^m + z X^n$ has cardinality 3, i.e., $\#\{n \in \mathbb{N} \mid (x X^k + y X^m + z X^n)_n \neq 0\} = 3$.
Polynomial.coeff_mul_X_pow theorem
(p : R[X]) (n d : ℕ) : coeff (p * Polynomial.X ^ n) (d + n) = coeff p d
Full source 
@[simp]
theorem coeff_mul_X_pow (p : R[X]) (n d : ℕ) :
    coeff (p * Polynomial.X ^ n) (d + n) = coeff p d := by
  rw [coeff_mul, Finset.sum_eq_single (d, n), coeff_X_pow, if_pos rfl, mul_one]
  · rintro ⟨i, j⟩ h1 h2
    rw [coeff_X_pow, if_neg, mul_zero]
    rintro rfl
    apply h2
    rw [mem_antidiagonal, add_right_cancel_iff] at h1
    subst h1
    rfl
  · exact fun h1 => (h1 (mem_antidiagonal.2 rfl)).elim
Coefficient Shift Formula for Polynomial Multiplication by $X^n$
Informal description
Let $R$ be a semiring and let $p \in R[X]$ be a univariate polynomial over $R$. For any natural numbers $n$ and $d$, the coefficient of $X^{d+n}$ in the product $p \cdot X^n$ is equal to the coefficient of $X^d$ in $p$. In other words, $$(p \cdot X^n)_{d+n} = p_d.$$
Polynomial.coeff_X_pow_mul theorem
(p : R[X]) (n d : ℕ) : coeff (Polynomial.X ^ n * p) (d + n) = coeff p d
Full source 
@[simp]
theorem coeff_X_pow_mul (p : R[X]) (n d : ℕ) :
    coeff (Polynomial.X ^ n * p) (d + n) = coeff p d := by
  rw [(commute_X_pow p n).eq, coeff_mul_X_pow]
Coefficient Shift Formula for Polynomial Multiplication by $X^n$ from the Left
Informal description
Let $R$ be a semiring and let $p \in R[X]$ be a univariate polynomial over $R$. For any natural numbers $n$ and $d$, the coefficient of $X^{d+n}$ in the product $X^n \cdot p$ is equal to the coefficient of $X^d$ in $p$. In other words, $$(X^n \cdot p)_{d+n} = p_d.$$
Polynomial.coeff_mul_X_pow' theorem
(p : R[X]) (n d : ℕ) : (p * X ^ n).coeff d = ite (n ≤ d) (p.coeff (d - n)) 0
Full source 
theorem coeff_mul_X_pow' (p : R[X]) (n d : ℕ) :
    (p * X ^ n).coeff d = ite (n ≤ d) (p.coeff (d - n)) 0 := by
  split_ifs with h
  · rw [← tsub_add_cancel_of_le h, coeff_mul_X_pow, add_tsub_cancel_right]
  · refine (coeff_mul _ _ _).trans (Finset.sum_eq_zero fun x hx => ?_)
    rw [coeff_X_pow, if_neg, mul_zero]
    exact ((le_of_add_le_right (mem_antidiagonal.mp hx).le).trans_lt <| not_le.mp h).ne
Coefficient Formula for Polynomial Multiplication by $X^n$: $(p \cdot X^n)_d = p_{d-n}$ if $n \leq d$ else $0$
Informal description
Let $R$ be a semiring and let $p \in R[X]$ be a univariate polynomial over $R$. For any natural numbers $n$ and $d$, the coefficient of $X^d$ in the product $p \cdot X^n$ is equal to the coefficient of $X^{d-n}$ in $p$ if $n \leq d$, and $0$ otherwise. In other words, $$(p \cdot X^n)_d = \begin{cases} p_{d-n} & \text{if } n \leq d \\ 0 & \text{otherwise} \end{cases}.$$
Polynomial.coeff_X_pow_mul' theorem
(p : R[X]) (n d : ℕ) : (X ^ n * p).coeff d = ite (n ≤ d) (p.coeff (d - n)) 0
Full source 
theorem coeff_X_pow_mul' (p : R[X]) (n d : ℕ) :
    (X ^ n * p).coeff d = ite (n ≤ d) (p.coeff (d - n)) 0 := by
  rw [(commute_X_pow p n).eq, coeff_mul_X_pow']
Coefficient Formula for $X^n \cdot p$: $(X^n \cdot p)_d = p_{d-n}$ if $n \leq d$ else $0$
Informal description
For any polynomial $p \in R[X]$ and natural numbers $n, d$, the coefficient of $X^d$ in the product $X^n \cdot p$ is given by: $$(X^n \cdot p)_d = \begin{cases} p_{d-n} & \text{if } n \leq d \\ 0 & \text{otherwise} \end{cases}.$$
Polynomial.coeff_mul_X theorem
(p : R[X]) (n : ℕ) : coeff (p * X) (n + 1) = coeff p n
Full source 
@[simp]
theorem coeff_mul_X (p : R[X]) (n : ℕ) : coeff (p * X) (n + 1) = coeff p n := by
  simpa only [pow_one] using coeff_mul_X_pow p 1 n
Coefficient Shift Formula for Polynomial Multiplication by $X$: $(p \cdot X)_{n+1} = p_n$
Informal description
Let $R$ be a semiring and let $p \in R[X]$ be a univariate polynomial over $R$. For any natural number $n$, the coefficient of $X^{n+1}$ in the product $p \cdot X$ is equal to the coefficient of $X^n$ in $p$. In other words, $$(p \cdot X)_{n+1} = p_n.$$
Polynomial.coeff_X_mul theorem
(p : R[X]) (n : ℕ) : coeff (X * p) (n + 1) = coeff p n
Full source 
@[simp]
theorem coeff_X_mul (p : R[X]) (n : ℕ) : coeff (X * p) (n + 1) = coeff p n := by
  rw [(commute_X p).eq, coeff_mul_X]
Coefficient Shift Formula for Polynomial Multiplication by $X$: $[X^{n+1}](X \cdot p) = [X^n]p$
Informal description
For any polynomial $p \in R[X]$ over a semiring $R$ and any natural number $n$, the coefficient of $X^{n+1}$ in the product $X \cdot p$ is equal to the coefficient of $X^n$ in $p$, i.e., $$[X^{n+1}](X \cdot p) = [X^n]p.$$
Polynomial.coeff_mul_monomial theorem
(p : R[X]) (n d : ℕ) (r : R) : coeff (p * monomial n r) (d + n) = coeff p d * r
Full source 
theorem coeff_mul_monomial (p : R[X]) (n d : ℕ) (r : R) :
    coeff (p * monomial n r) (d + n) = coeff p d * r := by
  rw [← C_mul_X_pow_eq_monomial, ← X_pow_mul, ← mul_assoc, coeff_mul_C, coeff_mul_X_pow]
Coefficient Formula for Polynomial Multiplication by Monomial: $[X^{d+n}](p \cdot (r X^n)) = [X^d]p \cdot r$
Informal description
For any polynomial $p \in R[X]$, natural numbers $n, d \in \mathbb{N}$, and coefficient $r \in R$, the coefficient of $X^{d+n}$ in the product $p \cdot (r X^n)$ is equal to the coefficient of $X^d$ in $p$ multiplied by $r$, i.e., $$[X^{d+n}](p \cdot (r X^n)) = [X^d]p \cdot r.$$
Polynomial.coeff_monomial_mul theorem
(p : R[X]) (n d : ℕ) (r : R) : coeff (monomial n r * p) (d + n) = r * coeff p d
Full source 
theorem coeff_monomial_mul (p : R[X]) (n d : ℕ) (r : R) :
    coeff (monomial n r * p) (d + n) = r * coeff p d := by
  rw [← C_mul_X_pow_eq_monomial, mul_assoc, coeff_C_mul, X_pow_mul, coeff_mul_X_pow]
Coefficient Formula for Monomial Multiplication: $(r X^n \cdot p)_{d+n} = r \cdot p_d$
Informal description
For any polynomial $p \in R[X]$, natural numbers $n, d \in \mathbb{N}$, and coefficient $r \in R$, the coefficient of $X^{d+n}$ in the product of the monomial $r X^n$ and $p$ is equal to $r$ multiplied by the coefficient of $X^d$ in $p$. That is, $$(r X^n \cdot p)_{d+n} = r \cdot p_d.$$
Polynomial.coeff_mul_monomial_zero theorem
(p : R[X]) (d : ℕ) (r : R) : coeff (p * monomial 0 r) d = coeff p d * r
Full source 
theorem coeff_mul_monomial_zero (p : R[X]) (d : ℕ) (r : R) :
    coeff (p * monomial 0 r) d = coeff p d * r :=
  coeff_mul_monomial p 0 d r
Coefficient formula for polynomial multiplication by constant term: $[X^d](p \cdot r) = [X^d]p \cdot r$
Informal description
For any polynomial $p \in R[X]$, natural number $d \in \mathbb{N}$, and coefficient $r \in R$, the coefficient of $X^d$ in the product $p \cdot (r X^0)$ is equal to the coefficient of $X^d$ in $p$ multiplied by $r$, i.e., $$[X^d](p \cdot r) = [X^d]p \cdot r.$$
Polynomial.coeff_monomial_zero_mul theorem
(p : R[X]) (d : ℕ) (r : R) : coeff (monomial 0 r * p) d = r * coeff p d
Full source 
theorem coeff_monomial_zero_mul (p : R[X]) (d : ℕ) (r : R) :
    coeff (monomial 0 r * p) d = r * coeff p d :=
  coeff_monomial_mul p 0 d r
Coefficient Formula for Constant Monomial Multiplication: $(r \cdot p)_d = r \cdot p_d$
Informal description
For any polynomial $p \in R[X]$, natural number $d \in \mathbb{N}$, and coefficient $r \in R$, the coefficient of $X^d$ in the product of the constant monomial $r$ (i.e., $r X^0$) and $p$ is equal to $r$ multiplied by the coefficient of $X^d$ in $p$. That is, $$(r \cdot p)_d = r \cdot p_d.$$
Polynomial.mul_X_pow_eq_zero theorem
{p : R[X]} {n : ℕ} (H : p * X ^ n = 0) : p = 0
Full source 
theorem mul_X_pow_eq_zero {p : R[X]} {n : ℕ} (H : p * X ^ n = 0) : p = 0 :=
  ext fun k => (coeff_mul_X_pow p n k).symm.trans <| ext_iff.1 H (k + n)
Vanishing of Polynomial Multiplied by $X^n$ Implies Vanishing of Polynomial
Informal description
For any polynomial $p \in R[X]$ and natural number $n$, if the product $p \cdot X^n$ is equal to the zero polynomial, then $p$ must be the zero polynomial.
Polynomial.isRegular_X_pow theorem
(n : ℕ) : IsRegular (X ^ n : R[X])
Full source 
theorem isRegular_X_pow (n : ℕ) : IsRegular (X ^ n : R[X]) := by
  suffices IsLeftRegular (X^n : R[X]) from
    ⟨this, this.right_of_commute (fun p => commute_X_pow p n)⟩
  intro P Q (hPQ : X^n * P = X^n * Q)
  ext i
  rw [← coeff_X_pow_mul P n i, hPQ, coeff_X_pow_mul Q n i]
Regularity of Monomial $X^n$ in Polynomial Ring $R[X]$
Informal description
For any natural number $n$, the monomial $X^n$ in the polynomial ring $R[X]$ is a regular element. That is, for any polynomials $p, q \in R[X]$, if $X^n \cdot p = X^n \cdot q$, then $p = q$ (left regularity), and if $p \cdot X^n = q \cdot X^n$, then $p = q$ (right regularity).
Polynomial.isRegular_X theorem
: IsRegular (X : R[X])
Full source 
@[simp] theorem isRegular_X : IsRegular (X : R[X]) := pow_one (X : R[X]) ▸ isRegular_X_pow 1
Regularity of the Polynomial Variable $X$ in $R[X]$
Informal description
The polynomial variable $X$ in the polynomial ring $R[X]$ is a regular element. That is, for any polynomials $p, q \in R[X]$, if $X \cdot p = X \cdot q$, then $p = q$ (left regularity), and if $p \cdot X = q \cdot X$, then $p = q$ (right regularity).
Polynomial.coeff_X_add_C_pow theorem
(r : R) (n k : ℕ) : ((X + C r) ^ n).coeff k = r ^ (n - k) * (n.choose k : R)
Full source 
theorem coeff_X_add_C_pow (r : R) (n k : ℕ) :
    ((X + C r) ^ n).coeff k = r ^ (n - k) * (n.choose k : R) := by
  rw [(commute_X (C r : R[X])).add_pow, ← lcoeff_apply, map_sum]
  simp only [one_pow, mul_one, lcoeff_apply, ← C_eq_natCast, ← C_pow, coeff_mul_C, Nat.cast_id]
  rw [Finset.sum_eq_single k, coeff_X_pow_self, one_mul]
  · intro _ _ h
    simp [coeff_X_pow, h.symm]
  · simp only [coeff_X_pow_self, one_mul, not_lt, Finset.mem_range]
    intro h
    rw [Nat.choose_eq_zero_of_lt h, Nat.cast_zero, mul_zero]
Binomial Expansion Coefficient Formula for $(X + r)^n$
Informal description
For any polynomial ring $R[X]$ over a semiring $R$, given an element $r \in R$ and natural numbers $n, k \in \mathbb{N}$, the coefficient of $X^k$ in the expansion of $(X + r)^n$ is given by: \[ \text{coeff}((X + r)^n, k) = r^{n-k} \cdot \binom{n}{k} \] where $\binom{n}{k}$ is the binomial coefficient.
Polynomial.coeff_X_add_one_pow theorem
(R : Type*) [Semiring R] (n k : ℕ) : ((X + 1) ^ n).coeff k = (n.choose k : R)
Full source 
theorem coeff_X_add_one_pow (R : Type*) [Semiring R] (n k : ℕ) :
    ((X + 1) ^ n).coeff k = (n.choose k : R) := by rw [← C_1, coeff_X_add_C_pow, one_pow, one_mul]
Binomial Coefficient Formula for $(X + 1)^n$ Expansion
Informal description
For any semiring $R$ and natural numbers $n, k \in \mathbb{N}$, the coefficient of $X^k$ in the expansion of the polynomial $(X + 1)^n$ in $R[X]$ is equal to the binomial coefficient $\binom{n}{k}$ interpreted in $R$, i.e., \[ \text{coeff}((X + 1)^n, k) = \binom{n}{k}. \]
Polynomial.coeff_one_add_X_pow theorem
(R : Type*) [Semiring R] (n k : ℕ) : ((1 + X) ^ n).coeff k = (n.choose k : R)
Full source 
theorem coeff_one_add_X_pow (R : Type*) [Semiring R] (n k : ℕ) :
    ((1 + X) ^ n).coeff k = (n.choose k : R) := by rw [add_comm _ X, coeff_X_add_one_pow]
Binomial Coefficient Formula for $(1 + X)^n$ Expansion
Informal description
For any semiring $R$ and natural numbers $n, k \in \mathbb{N}$, the coefficient of $X^k$ in the expansion of the polynomial $(1 + X)^n$ in $R[X]$ is equal to the binomial coefficient $\binom{n}{k}$ interpreted in $R$, i.e., \[ \text{coeff}((1 + X)^n, k) = \binom{n}{k}. \]
Polynomial.C_dvd_iff_dvd_coeff theorem
(r : R) (φ : R[X]) : C r ∣ φ ↔ ∀ i, r ∣ φ.coeff i
Full source 
theorem C_dvd_iff_dvd_coeff (r : R) (φ : R[X]) : CC r ∣ φC r ∣ φ ↔ ∀ i, r ∣ φ.coeff i := by
  constructor
  · rintro ⟨φ, rfl⟩ c
    rw [coeff_C_mul]
    apply dvd_mul_right
  · intro h
    choose c hc using h
    classical
      let c' : ℕ → R := fun i => if i ∈ φ.support then c i else 0
      let ψ : R[X] := ∑ i ∈ φ.support, monomial i (c' i)
      use ψ
      ext i
      simp only [c', ψ, coeff_C_mul, mem_support_iff, coeff_monomial, finset_sum_coeff,
        Finset.sum_ite_eq']
      split_ifs with hi
      · rw [hc]
      · rw [Classical.not_not] at hi
        rwa [mul_zero]
Divisibility of Polynomial by Constant Polynomial via Coefficient-wise Divisibility
Informal description
For any element $r$ in a semiring $R$ and any polynomial $\varphi \in R[X]$, the constant polynomial $C(r)$ divides $\varphi$ if and only if $r$ divides every coefficient of $\varphi$. In other words, $$ C(r) \mid \varphi \leftrightarrow \forall i, \, r \mid \text{coeff}(\varphi, i). $$
Polynomial.smul_eq_C_mul theorem
(a : R) : a • p = C a * p
Full source 
theorem smul_eq_C_mul (a : R) : a • p = C a * p := by simp [ext_iff]
Scalar Multiplication as Constant Polynomial Multiplication: $a \cdot p = C(a) * p$
Informal description
For any element $a$ in a semiring $R$ and any polynomial $p \in R[X]$, the scalar multiplication $a \cdot p$ is equal to the product of the constant polynomial $C(a)$ and $p$, i.e., $$ a \cdot p = C(a) * p. $$
Polynomial.update_eq_add_sub_coeff theorem
{R : Type*} [Ring R] (p : R[X]) (n : ℕ) (a : R) : p.update n a = p + Polynomial.C (a - p.coeff n) * Polynomial.X ^ n
Full source 
theorem update_eq_add_sub_coeff {R : Type*} [Ring R] (p : R[X]) (n : ℕ) (a : R) :
    p.update n a = p + Polynomial.C (a - p.coeff n) * Polynomial.X ^ n := by
  ext
  rw [coeff_update_apply, coeff_add, coeff_C_mul_X_pow]
  split_ifs with h <;> simp [h]
Polynomial Update Formula: $p.\text{update}\,n\,a = p + (a - p_n) X^n$
Informal description
For any polynomial $p \in R[X]$ over a ring $R$, natural number $n$, and element $a \in R$, the updated polynomial $p.\text{update}\,n\,a$ is equal to the original polynomial $p$ plus the monomial $(a - p_n) X^n$, where $p_n$ is the coefficient of $X^n$ in $p$. In other words: $$ p.\text{update}\,n\,a = p + (a - p_n) X^n. $$
Polynomial.natCast_coeff_zero theorem
{n : ℕ} {R : Type*} [Semiring R] : (n : R[X]).coeff 0 = n
Full source 
theorem natCast_coeff_zero {n : ℕ} {R : Type*} [Semiring R] : (n : R[X]).coeff 0 = n := by
  simp only [coeff_natCast_ite, ite_true]
Constant Polynomial Coefficient at Zero: $(n : R[X])_0 = n$
Informal description
For any natural number $n$ and any semiring $R$, the coefficient of $X^0$ in the constant polynomial $n \in R[X]$ is equal to $n$, i.e., $(n : R[X]).\text{coeff}\,0 = n$.
Polynomial.natCast_inj theorem
{m n : ℕ} {R : Type*} [Semiring R] [CharZero R] : (↑m : R[X]) = ↑n ↔ m = n
Full source 
@[norm_cast]
theorem natCast_inj {m n : ℕ} {R : Type*} [Semiring R] [CharZero R] :
    (↑m : R[X]) = ↑n ↔ m = n := by
  constructor
  · intro h
    apply_fun fun p => p.coeff 0 at h
    simpa using h
  · rintro rfl
    rfl
Injectivity of Natural Number Cast in Polynomial Semiring: $\uparrow m = \uparrow n \leftrightarrow m = n$
Informal description
For any natural numbers $m$ and $n$ and any semiring $R$ of characteristic zero, the equality of the constant polynomials $\uparrow m$ and $\uparrow n$ in $R[X]$ holds if and only if $m = n$.
Polynomial.intCast_coeff_zero theorem
{i : ℤ} {R : Type*} [Ring R] : (i : R[X]).coeff 0 = i
Full source 
@[simp]
theorem intCast_coeff_zero {i : ℤ} {R : Type*} [Ring R] : (i : R[X]).coeff 0 = i := by
  cases i <;> simp
Constant Term of Integer Polynomial: $\text{coeff}(i, 0) = i$
Informal description
For any integer $i$ and any ring $R$, the coefficient of the constant term (degree 0) in the constant polynomial $i \in R[X]$ is equal to $i$, i.e., $\text{coeff}(i, 0) = i$.
Polynomial.intCast_inj theorem
{m n : ℤ} {R : Type*} [Ring R] [CharZero R] : (↑m : R[X]) = ↑n ↔ m = n
Full source 
@[norm_cast]
theorem intCast_inj {m n : ℤ} {R : Type*} [Ring R] [CharZero R] : (↑m : R[X]) = ↑n ↔ m = n := by
  constructor
  · intro h
    apply_fun fun p => p.coeff 0 at h
    simpa using h
  · rintro rfl
    rfl
Injectivity of Integer Polynomial Casting: $m = n \leftrightarrow m = n$ in $R[X]$ for characteristic zero rings
Informal description
For any integers $m$ and $n$ and any ring $R$ of characteristic zero, the equality of the constant polynomials $m$ and $n$ in the polynomial ring $R[X]$ holds if and only if $m = n$.
Polynomial.charZero instance
[CharZero R] : CharZero R[X]
Full source 
instance charZero [CharZero R] : CharZero R[X] where cast_injective _x _y := natCast_inj.mp
Polynomial Rings Preserve Characteristic Zero
Informal description
For any semiring $R$ of characteristic zero, the polynomial ring $R[X]$ also has characteristic zero. This means the canonical map from the natural numbers $\mathbb{N}$ to $R[X]$ is injective.