Mathlib.Algebra.Polynomial.EraseLead

Polynomial.eraseLead definition

(f : R[X]) : R[X]

Full source

/-- `eraseLead f` for a polynomial `f` is the polynomial obtained by
subtracting from `f` the leading term of `f`. -/
def eraseLead (f : R[X]) : R[X] :=
  Polynomial.erase f.natDegree f

Polynomial with leading term erased

Informal description

For a polynomial $f \in R[X]$, the operation $\operatorname{eraseLead}(f)$ returns the polynomial obtained by subtracting the leading term of $f$ from $f$ itself. Specifically, if $f = \sum_{k=0}^n a_k X^k$ with $a_n \neq 0$, then $\operatorname{eraseLead}(f) = f - a_n X^n$.

Polynomial.eraseLead_support theorem

(f : R[X]) : f.eraseLead.support = f.support.erase f.natDegree

Full source

theorem eraseLead_support (f : R[X]) : f.eraseLead.support = f.support.erase f.natDegree := by
  simp only [eraseLead, support_erase]

Support of Polynomial After Erasing Leading Term Equals Support Minus Leading Degree

Informal description

For any polynomial $f \in R[X]$, the support of the polynomial obtained by erasing the leading term of $f$ is equal to the support of $f$ with the degree of the leading term removed. That is, $\operatorname{support}(\operatorname{eraseLead}(f)) = \operatorname{support}(f) \setminus \{\operatorname{natDegree}(f)\}$.

Polynomial.eraseLead_coeff theorem

(i : ℕ) : f.eraseLead.coeff i = if i = f.natDegree then 0 else f.coeff i

Full source

theorem eraseLead_coeff (i : ℕ) :
    f.eraseLead.coeff i = if i = f.natDegree then 0 else f.coeff i := by
  simp only [eraseLead, coeff_erase]

Coefficient Formula for Polynomial with Erased Leading Term: $(\operatorname{eraseLead}(f)).\text{coeff}(i) = f.\text{coeff}(i)$ if $i \neq \deg(f)$, $0$ otherwise

Informal description

For any polynomial $f \in R[X]$ and natural number $i$, the coefficient of $X^i$ in $\operatorname{eraseLead}(f)$ is given by: \[ (\operatorname{eraseLead}(f)).\text{coeff}(i) = \begin{cases} 0 & \text{if } i = \operatorname{natDegree}(f), \\ f.\text{coeff}(i) & \text{otherwise.} \end{cases} \]

Polynomial.eraseLead_coeff_natDegree theorem

: f.eraseLead.coeff f.natDegree = 0

Full source

@[simp]
theorem eraseLead_coeff_natDegree : f.eraseLead.coeff f.natDegree = 0 := by simp [eraseLead_coeff]

Vanishing Leading Coefficient After Erasure: $(\operatorname{eraseLead}(f))_{\deg(f)} = 0$

Informal description

For any polynomial $f \in R[X]$, the coefficient of the term $X^{\deg(f)}$ in $\operatorname{eraseLead}(f)$ is zero, i.e., \[ (\operatorname{eraseLead}(f)).\text{coeff}(\deg(f)) = 0. \]

Polynomial.eraseLead_coeff_of_ne theorem

(i : ℕ) (hi : i ≠ f.natDegree) : f.eraseLead.coeff i = f.coeff i

Full source

theorem eraseLead_coeff_of_ne (i : ℕ) (hi : i ≠ f.natDegree) : f.eraseLead.coeff i = f.coeff i := by
  simp [eraseLead_coeff, hi]

Coefficient Preservation in Polynomial Erasure for Non-Leading Terms

Informal description

For any polynomial $f \in R[X]$ and natural number $i \neq \deg(f)$, the coefficient of $X^i$ in $\operatorname{eraseLead}(f)$ equals the coefficient of $X^i$ in $f$, i.e., \[ (\operatorname{eraseLead}(f)).\text{coeff}(i) = f.\text{coeff}(i). \]

Polynomial.eraseLead_zero theorem

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

Full source

@[simp]
theorem eraseLead_zero : eraseLead (0 : R[X]) = 0 := by simp only [eraseLead, erase_zero]

Erasing the Leading Term of the Zero Polynomial Yields Zero

Informal description

For the zero polynomial $0 \in R[X]$, the operation of erasing the leading term yields the zero polynomial, i.e., $\operatorname{eraseLead}(0) = 0$.

Polynomial.eraseLead_add_monomial_natDegree_leadingCoeff theorem

(f : R[X]) : f.eraseLead + monomial f.natDegree f.leadingCoeff = f

Full source

@[simp]
theorem eraseLead_add_monomial_natDegree_leadingCoeff (f : R[X]) :
    f.eraseLead + monomial f.natDegree f.leadingCoeff = f :=
  (add_comm _ _).trans (f.monomial_add_erase _)

Polynomial Decomposition: $f = \operatorname{eraseLead}(f) + a_n X^n$

Informal description

For any polynomial $f \in R[X]$, the sum of the polynomial obtained by erasing the leading term of $f$ and the monomial formed by the leading coefficient and degree of $f$ equals $f$ itself. That is, \[ \operatorname{eraseLead}(f) + a_n X^n = f \] where $n = \deg(f)$ is the degree of $f$ and $a_n$ is its leading coefficient.

Polynomial.eraseLead_add_C_mul_X_pow theorem

(f : R[X]) : f.eraseLead + C f.leadingCoeff * X ^ f.natDegree = f

Full source

@[simp]
theorem eraseLead_add_C_mul_X_pow (f : R[X]) :
    f.eraseLead + C f.leadingCoeff * X ^ f.natDegree = f := by
  rw [C_mul_X_pow_eq_monomial, eraseLead_add_monomial_natDegree_leadingCoeff]

Polynomial Decomposition: $f = \operatorname{eraseLead}(f) + a_n X^n$

Informal description

For any polynomial $f \in R[X]$, the sum of the polynomial obtained by erasing the leading term of $f$ and the monomial formed by the leading coefficient and degree of $f$ equals $f$ itself. That is, \[ \operatorname{eraseLead}(f) + a_n X^n = f \] where $a_n$ is the leading coefficient of $f$ and $n$ is its degree.

Polynomial.self_sub_monomial_natDegree_leadingCoeff theorem

{R : Type*} [Ring R] (f : R[X]) : f - monomial f.natDegree f.leadingCoeff = f.eraseLead

Full source

@[simp]
theorem self_sub_monomial_natDegree_leadingCoeff {R : Type*} [Ring R] (f : R[X]) :
    f - monomial f.natDegree f.leadingCoeff = f.eraseLead :=
  (eq_sub_iff_add_eq.mpr (eraseLead_add_monomial_natDegree_leadingCoeff f)).symm

Polynomial Decomposition via Leading Term Subtraction: $f - a_n X^n = \operatorname{eraseLead}(f)$

Informal description

For any polynomial $f$ over a ring $R$, the difference between $f$ and its leading term (given by the monomial $a_n X^n$ where $n$ is the degree of $f$ and $a_n$ is its leading coefficient) equals the polynomial obtained by erasing the leading term of $f$. That is, \[ f - a_n X^n = \operatorname{eraseLead}(f). \]

Polynomial.self_sub_C_mul_X_pow theorem

{R : Type*} [Ring R] (f : R[X]) : f - C f.leadingCoeff * X ^ f.natDegree = f.eraseLead

Full source

@[simp]
theorem self_sub_C_mul_X_pow {R : Type*} [Ring R] (f : R[X]) :
    f - C f.leadingCoeff * X ^ f.natDegree = f.eraseLead := by
  rw [C_mul_X_pow_eq_monomial, self_sub_monomial_natDegree_leadingCoeff]

Polynomial decomposition via leading term subtraction: $f - a_n X^n = \operatorname{eraseLead}(f)$

Informal description

For any polynomial $f$ over a ring $R$, the difference between $f$ and its leading term (given by $a_n X^n$ where $a_n$ is the leading coefficient and $n$ is the degree of $f$) equals the polynomial obtained by erasing the leading term of $f$. That is, \[ f - a_n X^n = \operatorname{eraseLead}(f). \]

Polynomial.eraseLead_ne_zero theorem

(f0 : 2 ≤ #f.support) : eraseLead f ≠ 0

Full source

theorem eraseLead_ne_zero (f0 : 2 ≤ #f.support) : eraseLeaderaseLead f ≠ 0 := by
  rw [Ne, ← card_support_eq_zero, eraseLead_support]
  exact
    (zero_lt_one.trans_le <| (tsub_le_tsub_right f0 1).trans Finset.pred_card_le_card_erase).ne.symm

Non-vanishing of Polynomial After Leading Term Removal

Informal description

For any polynomial $f \in R[X]$ with at least two nonzero coefficients (i.e., $|\operatorname{support}(f)| \geq 2$), the polynomial obtained by removing its leading term is nonzero, i.e., $\operatorname{eraseLead}(f) \neq 0$.

Polynomial.lt_natDegree_of_mem_eraseLead_support theorem

{a : ℕ} (h : a ∈ (eraseLead f).support) : a < f.natDegree

Full source

theorem lt_natDegree_of_mem_eraseLead_support {a : ℕ} (h : a ∈ (eraseLead f).support) :
    a < f.natDegree := by
  rw [eraseLead_support, mem_erase] at h
  exact (le_natDegree_of_mem_supp a h.2).lt_of_ne h.1

Support elements of erased polynomial have degree strictly less than original polynomial's degree

Informal description

For any polynomial $f \in R[X]$ and natural number $a$, if $a$ is in the support of the polynomial obtained by erasing the leading term of $f$ (i.e., $a \in \operatorname{support}(\operatorname{eraseLead}(f))$), then $a$ is strictly less than the natural degree of $f$ (i.e., $a < \operatorname{natDegree}(f)$).

Polynomial.ne_natDegree_of_mem_eraseLead_support theorem

{a : ℕ} (h : a ∈ (eraseLead f).support) : a ≠ f.natDegree

Full source

theorem ne_natDegree_of_mem_eraseLead_support {a : ℕ} (h : a ∈ (eraseLead f).support) :
    a ≠ f.natDegree :=
  (lt_natDegree_of_mem_eraseLead_support h).ne

Support elements of erased polynomial differ from original polynomial's degree

Informal description

For any polynomial $f \in R[X]$ and natural number $a$, if $a$ belongs to the support of $\operatorname{eraseLead}(f)$, then $a$ is not equal to the natural degree of $f$.

Polynomial.natDegree_not_mem_eraseLead_support theorem

: f.natDegree ∉ (eraseLead f).support

Full source

theorem natDegree_not_mem_eraseLead_support : f.natDegree ∉ (eraseLead f).support := fun h =>
  ne_natDegree_of_mem_eraseLead_support h rfl

Natural Degree Excluded from Erased Polynomial's Support

Informal description

For any polynomial $f \in R[X]$, the natural degree of $f$ does not belong to the support of the polynomial obtained by erasing the leading term of $f$, i.e., $\operatorname{natDegree}(f) \notin \operatorname{support}(\operatorname{eraseLead}(f))$.

Polynomial.eraseLead_support_card_lt theorem

(h : f ≠ 0) : #(eraseLead f).support < #f.support

Full source

theorem eraseLead_support_card_lt (h : f ≠ 0) : #(eraseLead f).support < #f.support := by
  rw [eraseLead_support]
  exact card_lt_card (erase_ssubset <| natDegree_mem_support_of_nonzero h)

Support Cardinality Decreases After Erasing Leading Term

Informal description

For any nonzero polynomial $f \in R[X]$, the cardinality of the support of $\operatorname{eraseLead}(f)$ is strictly less than the cardinality of the support of $f$. That is, $\#\operatorname{support}(\operatorname{eraseLead}(f)) < \#\operatorname{support}(f)$.

Polynomial.card_support_eraseLead_add_one theorem

(h : f ≠ 0) : #f.eraseLead.support + 1 = #f.support

Full source

theorem card_support_eraseLead_add_one (h : f ≠ 0) : #f.eraseLead.support + 1 = #f.support := by
  set c := #f.support with hc
  cases h₁ : c
  case zero =>
    by_contra
    exact h (card_support_eq_zero.mp h₁)
  case succ =>
    rw [eraseLead_support, card_erase_of_mem (natDegree_mem_support_of_nonzero h), ← hc, h₁]
    rfl

Cardinality Relation Between Polynomial Support and Its Erased-Lead Version: $|\operatorname{support}(f - \text{lead}(f))| + 1 = |\operatorname{support}(f)|$ for $f \neq 0$

Informal description

For any nonzero polynomial $f \in R[X]$, the cardinality of the support of $\operatorname{eraseLead}(f)$ plus one equals the cardinality of the support of $f$, i.e., $|\operatorname{support}(\operatorname{eraseLead}(f))| + 1 = |\operatorname{support}(f)|$.

Polynomial.card_support_eraseLead theorem

: #f.eraseLead.support = #f.support - 1

Full source

@[simp]
theorem card_support_eraseLead : #f.eraseLead.support = #f.support - 1 := by
  by_cases hf : f = 0
  · rw [hf, eraseLead_zero, support_zero, card_empty]
  · rw [← card_support_eraseLead_add_one hf, add_tsub_cancel_right]

Support Cardinality Decrement After Erasing Leading Term: $|\operatorname{support}(\operatorname{eraseLead}(f))| = |\operatorname{support}(f)| - 1$

Informal description

For any polynomial $f \in R[X]$, the cardinality of the support of $\operatorname{eraseLead}(f)$ is equal to the cardinality of the support of $f$ minus one, i.e., $|\operatorname{support}(\operatorname{eraseLead}(f))| = |\operatorname{support}(f)| - 1$.

Polynomial.card_support_eraseLead' theorem

{c : ℕ} (fc : #f.support = c + 1) : #f.eraseLead.support = c

Full source

theorem card_support_eraseLead' {c : ℕ} (fc : #f.support = c + 1) :
    #f.eraseLead.support = c := by
  rw [card_support_eraseLead, fc, add_tsub_cancel_right]

Support Cardinality Reduction by One After Erasing Leading Term: $|\operatorname{support}(\operatorname{eraseLead}(f))| = c$ when $|\operatorname{support}(f)| = c + 1$

Informal description

For any polynomial $f \in R[X]$ and natural number $c$, if the cardinality of the support of $f$ is $c + 1$, then the cardinality of the support of $\operatorname{eraseLead}(f)$ is $c$.

Polynomial.card_support_eq_one_of_eraseLead_eq_zero theorem

(h₀ : f ≠ 0) (h₁ : f.eraseLead = 0) : #f.support = 1

Full source

theorem card_support_eq_one_of_eraseLead_eq_zero (h₀ : f ≠ 0) (h₁ : f.eraseLead = 0) :
    #f.support = 1 :=
  (card_support_eq_zero.mpr h₁ ▸ card_support_eraseLead_add_one h₀).symm

Support Cardinality of Polynomial with Vanishing Erased-Lead Term: $\#\operatorname{support}(f) = 1$ when $f \neq 0$ and $\operatorname{eraseLead}(f) = 0$

Informal description

For any nonzero polynomial $f \in R[X]$, if the polynomial obtained by erasing the leading term of $f$ is the zero polynomial, then the support of $f$ has exactly one element, i.e., $\#\operatorname{support}(f) = 1$.

Polynomial.card_support_le_one_of_eraseLead_eq_zero theorem

(h : f.eraseLead = 0) : #f.support ≤ 1

Full source

theorem card_support_le_one_of_eraseLead_eq_zero (h : f.eraseLead = 0) : #f.support ≤ 1 := by
  by_cases hpz : f = 0
  case pos => simp [hpz]
  case neg => exact le_of_eq (card_support_eq_one_of_eraseLead_eq_zero hpz h)

Support Cardinality Bound for Polynomial with Vanishing Erased-Lead Term: $\#\operatorname{support}(f) \leq 1$ when $\operatorname{eraseLead}(f) = 0$

Informal description

For any polynomial $f \in R[X]$, if the polynomial obtained by erasing the leading term of $f$ is the zero polynomial, then the support of $f$ has at most one element, i.e., $\#\operatorname{support}(f) \leq 1$.

Polynomial.eraseLead_monomial theorem

(i : ℕ) (r : R) : eraseLead (monomial i r) = 0

Full source

@[simp]
theorem eraseLead_monomial (i : ℕ) (r : R) : eraseLead (monomial i r) = 0 := by
  classical
  by_cases hr : r = 0
  · subst r
    simp only [monomial_zero_right, eraseLead_zero]
  · rw [eraseLead, natDegree_monomial, if_neg hr, erase_monomial]

Erasing the Leading Term of a Monomial Yields Zero: $\operatorname{eraseLead}(rX^i) = 0$

Informal description

For any natural number $i$ and coefficient $r$ in a semiring $R$, the polynomial obtained by erasing the leading term of the monomial $rX^i$ is the zero polynomial, i.e., $\operatorname{eraseLead}(rX^i) = 0$.

Polynomial.eraseLead_C theorem

(r : R) : eraseLead (C r) = 0

Full source

@[simp]
theorem eraseLead_C (r : R) : eraseLead (C r) = 0 :=
  eraseLead_monomial _ _

Erasing the Leading Term of a Constant Polynomial Yields Zero: $\operatorname{eraseLead}(r) = 0$

Informal description

For any element $r$ in a semiring $R$, the polynomial obtained by erasing the leading term of the constant polynomial $r$ is the zero polynomial, i.e., $\operatorname{eraseLead}(r) = 0$.

Polynomial.eraseLead_X theorem

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

Full source

@[simp]
theorem eraseLead_X : eraseLead (X : R[X]) = 0 :=
  eraseLead_monomial _ _

Erasing the Leading Term of $X$ Yields Zero: $\operatorname{eraseLead}(X) = 0$

Informal description

For the polynomial variable $X$ in the polynomial ring $R[X]$, erasing its leading term yields the zero polynomial, i.e., $\operatorname{eraseLead}(X) = 0$.

Polynomial.eraseLead_X_pow theorem

(n : ℕ) : eraseLead (X ^ n : R[X]) = 0

Full source

@[simp]
theorem eraseLead_X_pow (n : ℕ) : eraseLead (X ^ n : R[X]) = 0 := by
  rw [X_pow_eq_monomial, eraseLead_monomial]

Erasing the Leading Term of $X^n$ Yields Zero: $\operatorname{eraseLead}(X^n) = 0$

Informal description

For any natural number $n$, the polynomial obtained by erasing the leading term of $X^n$ in the polynomial ring $R[X]$ is the zero polynomial, i.e., $\operatorname{eraseLead}(X^n) = 0$.

Polynomial.eraseLead_C_mul_X_pow theorem

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

Full source

@[simp]
theorem eraseLead_C_mul_X_pow (r : R) (n : ℕ) : eraseLead (C r * X ^ n) = 0 := by
  rw [C_mul_X_pow_eq_monomial, eraseLead_monomial]

Erasing the Leading Term of a Monomial Yields Zero: $\operatorname{eraseLead}(r X^n) = 0$

Informal description

For any coefficient $r$ in a semiring $R$ and any natural number $n$, the polynomial obtained by erasing the leading term of $r X^n$ is the zero polynomial, i.e., \[ \operatorname{eraseLead}(r X^n) = 0. \]

Polynomial.eraseLead_C_mul_X theorem

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

Full source

@[simp] lemma eraseLead_C_mul_X (r : R) : eraseLead (C r * X) = 0 := by
  simpa using eraseLead_C_mul_X_pow _ 1

Erasing the Leading Term of a Linear Monomial Yields Zero: $\operatorname{eraseLead}(rX) = 0$

Informal description

For any coefficient $r$ in a semiring $R$, the polynomial obtained by erasing the leading term of the monomial $rX$ is the zero polynomial, i.e., \[ \operatorname{eraseLead}(rX) = 0. \]

Polynomial.eraseLead_add_of_degree_lt_left theorem

{p q : R[X]} (pq : q.degree < p.degree) : (p + q).eraseLead = p.eraseLead + q

Full source

theorem eraseLead_add_of_degree_lt_left {p q : R[X]} (pq : q.degree < p.degree) :
    (p + q).eraseLead = p.eraseLead + q := by
  ext n
  by_cases nd : n = p.natDegree
  · rw [nd, eraseLead_coeff, if_pos (natDegree_add_eq_left_of_degree_lt pq).symm]
    simpa using (coeff_eq_zero_of_degree_lt (lt_of_lt_of_le pq degree_le_natDegree)).symm
  · rw [eraseLead_coeff, coeff_add, coeff_add, eraseLead_coeff, if_neg, if_neg nd]
    rintro rfl
    exact nd (natDegree_add_eq_left_of_degree_lt pq)

Erasing Leading Term Preserves Addition under Degree Condition: $\operatorname{eraseLead}(p + q) = \operatorname{eraseLead}(p) + q$ when $\deg(q) < \deg(p)$

Informal description

For any two polynomials $p, q \in R[X]$, if the degree of $q$ is strictly less than the degree of $p$, then the polynomial obtained by erasing the leading term of $p + q$ is equal to the sum of the polynomial obtained by erasing the leading term of $p$ and $q$, i.e., \[ \operatorname{eraseLead}(p + q) = \operatorname{eraseLead}(p) + q. \]

Polynomial.eraseLead_add_of_natDegree_lt_left theorem

{p q : R[X]} (pq : q.natDegree < p.natDegree) : (p + q).eraseLead = p.eraseLead + q

Full source

theorem eraseLead_add_of_natDegree_lt_left {p q : R[X]} (pq : q.natDegree < p.natDegree) :
    (p + q).eraseLead = p.eraseLead + q :=
  eraseLead_add_of_degree_lt_left (degree_lt_degree pq)

Erasing Leading Term Preserves Addition under Natural Degree Condition: $\operatorname{eraseLead}(p + q) = \operatorname{eraseLead}(p) + q$ when $\operatorname{natDegree}(q) < \operatorname{natDegree}(p)$

Informal description

For any two polynomials $p, q \in R[X]$, if the natural degree of $q$ is strictly less than the natural degree of $p$, then the polynomial obtained by erasing the leading term of $p + q$ is equal to the sum of the polynomial obtained by erasing the leading term of $p$ and $q$, i.e., \[ \operatorname{eraseLead}(p + q) = \operatorname{eraseLead}(p) + q. \]

Polynomial.eraseLead_add_of_degree_lt_right theorem

{p q : R[X]} (pq : p.degree < q.degree) : (p + q).eraseLead = p + q.eraseLead

Full source

theorem eraseLead_add_of_degree_lt_right {p q : R[X]} (pq : p.degree < q.degree) :
    (p + q).eraseLead = p + q.eraseLead := by
  ext n
  by_cases nd : n = q.natDegree
  · rw [nd, eraseLead_coeff, if_pos (natDegree_add_eq_right_of_degree_lt pq).symm]
    simpa using (coeff_eq_zero_of_degree_lt (lt_of_lt_of_le pq degree_le_natDegree)).symm
  · rw [eraseLead_coeff, coeff_add, coeff_add, eraseLead_coeff, if_neg, if_neg nd]
    rintro rfl
    exact nd (natDegree_add_eq_right_of_degree_lt pq)

Erasing Leading Term Preserves Addition When $\deg(p) < \deg(q)$

Informal description

For any two polynomials $p, q \in R[X]$ such that the degree of $p$ is strictly less than the degree of $q$, the polynomial obtained by erasing the leading term of $p + q$ is equal to $p$ plus the polynomial obtained by erasing the leading term of $q$. That is, \[ \operatorname{eraseLead}(p + q) = p + \operatorname{eraseLead}(q). \]

Polynomial.eraseLead_add_of_natDegree_lt_right theorem

{p q : R[X]} (pq : p.natDegree < q.natDegree) : (p + q).eraseLead = p + q.eraseLead

Full source

theorem eraseLead_add_of_natDegree_lt_right {p q : R[X]} (pq : p.natDegree < q.natDegree) :
    (p + q).eraseLead = p + q.eraseLead :=
  eraseLead_add_of_degree_lt_right (degree_lt_degree pq)

Erasing Leading Term Preserves Addition under Natural Degree Condition: $\operatorname{eraseLead}(p + q) = p + \operatorname{eraseLead}(q)$ when $\operatorname{natDegree}(p) < \operatorname{natDegree}(q)$

Informal description

For any two polynomials $p, q \in R[X]$ such that the natural degree of $p$ is strictly less than the natural degree of $q$, the polynomial obtained by erasing the leading term of $p + q$ is equal to $p$ plus the polynomial obtained by erasing the leading term of $q$. That is, \[ \operatorname{eraseLead}(p + q) = p + \operatorname{eraseLead}(q). \]

Polynomial.eraseLead_degree_le theorem

: (eraseLead f).degree ≤ f.degree

Full source

theorem eraseLead_degree_le : (eraseLead f).degree ≤ f.degree :=
  f.degree_erase_le _

Degree Bound After Erasing Leading Term

Informal description

For any polynomial $f \in R[X]$, the degree of the polynomial obtained by erasing the leading term of $f$ is less than or equal to the degree of $f$. That is, $\deg(\operatorname{eraseLead}(f)) \leq \deg(f)$.

Polynomial.degree_eraseLead_lt theorem

(hf : f ≠ 0) : (eraseLead f).degree < f.degree

Full source

theorem degree_eraseLead_lt (hf : f ≠ 0) : (eraseLead f).degree < f.degree :=
  f.degree_erase_lt hf

Strict Degree Reduction After Erasing Leading Term

Informal description

For any nonzero polynomial $f \in R[X]$, the degree of the polynomial obtained by erasing the leading term of $f$ is strictly less than the degree of $f$, i.e., $\deg(\operatorname{eraseLead}(f)) < \deg(f)$.

Polynomial.eraseLead_natDegree_le_aux theorem

: (eraseLead f).natDegree ≤ f.natDegree

Full source

theorem eraseLead_natDegree_le_aux : (eraseLead f).natDegree ≤ f.natDegree :=
  natDegree_le_natDegree eraseLead_degree_le

Natural Degree Bound After Erasing Leading Term

Informal description

For any polynomial $f \in R[X]$, the natural degree of the polynomial obtained by erasing the leading term of $f$ is less than or equal to the natural degree of $f$. That is, $\operatorname{natDegree}(\operatorname{eraseLead}(f)) \leq \operatorname{natDegree}(f)$.

Polynomial.eraseLead_natDegree_lt theorem

(f0 : 2 ≤ #f.support) : (eraseLead f).natDegree < f.natDegree

Full source

theorem eraseLead_natDegree_lt (f0 : 2 ≤ #f.support) : (eraseLead f).natDegree < f.natDegree :=
  lt_of_le_of_ne eraseLead_natDegree_le_aux <|
    ne_natDegree_of_mem_eraseLead_support <|
      natDegree_mem_support_of_nonzero <| eraseLead_ne_zero f0

Strict Natural Degree Reduction After Erasing Leading Term of Polynomial with Multiple Nonzero Coefficients

Informal description

For any polynomial $f \in R[X]$ with at least two nonzero coefficients (i.e., $|\operatorname{support}(f)| \geq 2$), the natural degree of the polynomial obtained by erasing its leading term is strictly less than the natural degree of $f$, i.e., $\operatorname{natDegree}(\operatorname{eraseLead}(f)) < \operatorname{natDegree}(f)$.

Polynomial.natDegree_pos_of_eraseLead_ne_zero theorem

(h : f.eraseLead ≠ 0) : 0 < f.natDegree

Full source

theorem natDegree_pos_of_eraseLead_ne_zero (h : f.eraseLead ≠ 0) : 0 < f.natDegree := by
  by_contra h₂
  rw [eq_C_of_natDegree_eq_zero (Nat.eq_zero_of_not_pos h₂)] at h
  simp at h

Nonzero Erased Lead Implies Positive Degree

Informal description

For a polynomial $f \in R[X]$, if the polynomial obtained by erasing the leading term of $f$ is nonzero, then the natural degree of $f$ is positive, i.e., $\operatorname{eraseLead}(f) \neq 0$ implies $0 < \operatorname{natDegree}(f)$.

Polynomial.eraseLead_natDegree_lt_or_eraseLead_eq_zero theorem

(f : R[X]) : (eraseLead f).natDegree < f.natDegree ∨ f.eraseLead = 0

Full source

theorem eraseLead_natDegree_lt_or_eraseLead_eq_zero (f : R[X]) :
    (eraseLead f).natDegree < f.natDegree ∨ f.eraseLead = 0 := by
  by_cases h : #f.support ≤ 1
  · right
    rw [← C_mul_X_pow_eq_self h]
    simp
  · left
    apply eraseLead_natDegree_lt (lt_of_not_ge h)

Natural Degree Reduction or Zero After Erasing Leading Term of a Polynomial

Informal description

For any polynomial $f \in R[X]$, either the natural degree of $\operatorname{eraseLead}(f)$ is strictly less than that of $f$, or $\operatorname{eraseLead}(f)$ is the zero polynomial. That is, \[ \operatorname{natDegree}(\operatorname{eraseLead}(f)) < \operatorname{natDegree}(f) \quad \text{or} \quad \operatorname{eraseLead}(f) = 0. \]

Polynomial.eraseLead_natDegree_le theorem

(f : R[X]) : (eraseLead f).natDegree ≤ f.natDegree - 1

Full source

theorem eraseLead_natDegree_le (f : R[X]) : (eraseLead f).natDegree ≤ f.natDegree - 1 := by
  rcases f.eraseLead_natDegree_lt_or_eraseLead_eq_zero with (h | h)
  · exact Nat.le_sub_one_of_lt h
  · simp only [h, natDegree_zero, zero_le]

Degree Bound After Erasing Leading Term of a Polynomial

Informal description

For any polynomial $f \in R[X]$, the natural degree of the polynomial obtained by erasing the leading term of $f$ satisfies $\operatorname{natDegree}(\operatorname{eraseLead}(f)) \leq \operatorname{natDegree}(f) - 1$.

Polynomial.natDegree_eraseLead theorem

(h : f.nextCoeff ≠ 0) : f.eraseLead.natDegree = f.natDegree - 1

Full source

lemma natDegree_eraseLead (h : f.nextCoeff ≠ 0) : f.eraseLead.natDegree = f.natDegree - 1 := by
  have := natDegree_pos_of_nextCoeff_ne_zero h
  refine f.eraseLead_natDegree_le.antisymm <| le_natDegree_of_ne_zero ?_
  rwa [eraseLead_coeff_of_ne _ (tsub_lt_self _ _).ne, ← nextCoeff_of_natDegree_pos]
  all_goals positivity

Degree Reduction by One When Erasing Leading Term of a Polynomial with Non-Zero Next Coefficient

Informal description

For a polynomial $f \in R[X]$ with non-zero next coefficient (i.e., the coefficient of $X^{\deg(f)-1}$ is non-zero), the degree of the polynomial obtained by erasing the leading term of $f$ is exactly one less than the degree of $f$, i.e., \[ \deg(\operatorname{eraseLead}(f)) = \deg(f) - 1. \]

Polynomial.natDegree_eraseLead_add_one theorem

(h : f.nextCoeff ≠ 0) : f.eraseLead.natDegree + 1 = f.natDegree

Full source

lemma natDegree_eraseLead_add_one (h : f.nextCoeff ≠ 0) :
    f.eraseLead.natDegree + 1 = f.natDegree := by
  rw [natDegree_eraseLead h, tsub_add_cancel_of_le]
  exact natDegree_pos_of_nextCoeff_ne_zero h

Degree relation after erasing leading term: $\deg(\text{eraseLead}(f)) + 1 = \deg(f)$ when next coefficient is non-zero

Informal description

For a polynomial $f \in R[X]$ with non-zero next coefficient (i.e., the coefficient of $X^{\deg(f)-1}$ is non-zero), the degree of the polynomial obtained by erasing the leading term of $f$ satisfies \[ \deg(\operatorname{eraseLead}(f)) + 1 = \deg(f). \]

Polynomial.natDegree_eraseLead_le_of_nextCoeff_eq_zero theorem

(h : f.nextCoeff = 0) : f.eraseLead.natDegree ≤ f.natDegree - 2

Full source

theorem natDegree_eraseLead_le_of_nextCoeff_eq_zero (h : f.nextCoeff = 0) :
    f.eraseLead.natDegree ≤ f.natDegree - 2 := by
  refine natDegree_le_pred (n := f.natDegree - 1) (eraseLead_natDegree_le f) ?_
  rw [nextCoeff_eq_zero, natDegree_eq_zero] at h
  obtain ⟨a, rfl⟩ | ⟨hf, h⟩ := h
  · simp
  rw [eraseLead_coeff_of_ne _ (tsub_lt_self hf zero_lt_one).ne, ← nextCoeff_of_natDegree_pos hf]
  simp [nextCoeff_eq_zero, h, eq_zero_or_pos]

Degree bound after erasing leading term when next coefficient is zero: $\deg(\text{eraseLead}(f)) \leq \deg(f) - 2$

Informal description

For any polynomial $f \in R[X]$, if the next coefficient after the leading term is zero (i.e., $\text{nextCoeff}(f) = 0$), then the degree of the polynomial obtained by erasing the leading term satisfies $\deg(\text{eraseLead}(f)) \leq \deg(f) - 2$.

Polynomial.two_le_natDegree_of_nextCoeff_eraseLead theorem

(hlead : f.eraseLead ≠ 0) (hnext : f.nextCoeff = 0) : 2 ≤ f.natDegree

Full source

lemma two_le_natDegree_of_nextCoeff_eraseLead (hlead : f.eraseLead ≠ 0)
    (hnext : f.nextCoeff = 0) : 2 ≤ f.natDegree := by
  contrapose! hlead
  rw [Nat.lt_succ_iff, Nat.le_one_iff_eq_zero_or_eq_one, natDegree_eq_zero, natDegree_eq_one]
    at hlead
  obtain ⟨a, rfl⟩ | ⟨a, ha, b, rfl⟩ := hlead
  · simp
  · rw [nextCoeff_C_mul_X_add_C ha] at hnext
    subst b
    simp

Degree Bound for Polynomials with Zero Next Coefficient and Nonzero Erased Lead: $\deg(f) \geq 2$

Informal description

For any nonzero polynomial $f \in R[X]$, if the polynomial obtained by erasing its leading term is nonzero (i.e., $\operatorname{eraseLead}(f) \neq 0$) and the next coefficient after the leading term is zero (i.e., $\operatorname{nextCoeff}(f) = 0$), then the degree of $f$ is at least 2, i.e., $\deg(f) \geq 2$.

Polynomial.leadingCoeff_eraseLead_eq_nextCoeff theorem

(h : f.nextCoeff ≠ 0) : f.eraseLead.leadingCoeff = f.nextCoeff

Full source

theorem leadingCoeff_eraseLead_eq_nextCoeff (h : f.nextCoeff ≠ 0) :
    f.eraseLead.leadingCoeff = f.nextCoeff := by
  have := natDegree_pos_of_nextCoeff_ne_zero h
  rw [leadingCoeff, nextCoeff, natDegree_eraseLead h, if_neg,
    eraseLead_coeff_of_ne _ (tsub_lt_self _ _).ne]
  all_goals positivity

Leading Coefficient of Erased Polynomial Equals Next Coefficient When Non-Zero: $\text{lead}(\text{eraseLead}(f)) = \text{nextCoeff}(f)$

Informal description

For any polynomial $f \in R[X]$ with a non-zero next coefficient (i.e., the coefficient of $X^{\deg(f)-1}$ is non-zero), the leading coefficient of the polynomial obtained by erasing the leading term of $f$ equals the next coefficient of $f$, i.e., \[ \text{lead}(\text{eraseLead}(f)) = \text{nextCoeff}(f). \]

Polynomial.nextCoeff_eq_zero_of_eraseLead_eq_zero theorem

(h : f.eraseLead = 0) : f.nextCoeff = 0

Full source

theorem nextCoeff_eq_zero_of_eraseLead_eq_zero (h : f.eraseLead = 0) : f.nextCoeff = 0 := by
  by_contra h₂
  exact leadingCoeff_ne_zero.mp (leadingCoeff_eraseLead_eq_nextCoeff h₂ ▸ h₂) h

Vanishing Next Coefficient Condition for Zero Erased-Lead Polynomial: $\text{nextCoeff}(f) = 0$ when $\text{eraseLead}(f) = 0$

Informal description

For any polynomial $f \in R[X]$, if the polynomial obtained by erasing the leading term of $f$ is zero (i.e., $\operatorname{eraseLead}(f) = 0$), then the next coefficient of $f$ (the coefficient of $X^{\deg(f)-1}$) is zero, i.e., $\operatorname{nextCoeff}(f) = 0$.

Polynomial.induction_with_natDegree_le theorem

 (P : R[X] → Prop) (N : ℕ) (P_0 : P 0) (P_C_mul_pow : ∀ n : ℕ, ∀ r : R, r ≠ 0 → n ≤ N → P (C r * X ^ n))
  (P_C_add : ∀ f g : R[X], f.natDegree < g.natDegree → g.natDegree ≤ N → P f → P g → P (f + g)) :
  ∀ f : R[X], f.natDegree ≤ N → P f

Full source

/-- An induction lemma for polynomials. It takes a natural number `N` as a parameter, that is
required to be at least as big as the `nat_degree` of the polynomial.  This is useful to prove
results where you want to change each term in a polynomial to something else depending on the
`nat_degree` of the polynomial itself and not on the specific `nat_degree` of each term. -/
theorem induction_with_natDegree_le (P : R[X] → Prop) (N : ℕ) (P_0 : P 0)
    (P_C_mul_pow : ∀ n : ℕ, ∀ r : R, r ≠ 0 → n ≤ N → P (C r * X ^ n))
    (P_C_add : ∀ f g : R[X], f.natDegree < g.natDegree → g.natDegree ≤ N → P f → P g → P (f + g)) :
    ∀ f : R[X], f.natDegree ≤ N → P f := by
  intro f df
  generalize hd : #f.support = c
  revert f
  induction' c with c hc
  · intro f _ f0
    convert P_0
    simpa [support_eq_empty, card_eq_zero] using f0
  · intro f df f0
    rw [← eraseLead_add_C_mul_X_pow f]
    cases c
    · convert P_C_mul_pow f.natDegree f.leadingCoeff ?_ df using 1
      · convert zero_add (C (leadingCoeff f) * X ^ f.natDegree)
        rw [← card_support_eq_zero, card_support_eraseLead' f0]
      · rw [leadingCoeff_ne_zero, Ne, ← card_support_eq_zero, f0]
        exact zero_ne_one.symm
    refine P_C_add f.eraseLead _ ?_ ?_ ?_ ?_
    · refine (eraseLead_natDegree_lt ?_).trans_le (le_of_eq ?_)
      · exact (Nat.succ_le_succ (Nat.succ_le_succ (Nat.zero_le _))).trans f0.ge
      · rw [natDegree_C_mul_X_pow _ _ (leadingCoeff_ne_zero.mpr _)]
        rintro rfl
        simp at f0
    · exact (natDegree_C_mul_X_pow_le f.leadingCoeff f.natDegree).trans df
    · exact hc _ (eraseLead_natDegree_le_aux.trans df) (card_support_eraseLead' f0)
    · refine P_C_mul_pow _ _ ?_ df
      rw [Ne, leadingCoeff_eq_zero, ← card_support_eq_zero, f0]
      exact Nat.succ_ne_zero _

Polynomial Induction Principle with Degree Bound $N$

Informal description

Let $P$ be a predicate on polynomials over a semiring $R$, and let $N$ be a natural number. Suppose the following conditions hold: 1. $P$ holds for the zero polynomial. 2. For any natural number $n \leq N$ and any nonzero coefficient $r \in R$, $P$ holds for the monomial $r X^n$. 3. For any polynomials $f$ and $g$ such that the degree of $f$ is strictly less than that of $g$, the degree of $g$ is at most $N$, and $P$ holds for both $f$ and $g$, then $P$ holds for their sum $f + g$. Then, $P$ holds for all polynomials $f$ with degree at most $N$.

Polynomial.mono_map_natDegree_eq theorem

 {S F : Type*} [Semiring S] [FunLike F R[X] S[X]] [AddMonoidHomClass F R[X] S[X]] {φ : F} {p : R[X]} (k : ℕ)
  (fu : ℕ → ℕ) (fu0 : ∀ {n}, n ≤ k → fu n = 0) (fc : ∀ {n m}, k ≤ n → n < m → fu n < fu m)
  (φ_k : ∀ {f : R[X]}, f.natDegree < k → φ f = 0) (φ_mon_nat : ∀ n c, c ≠ 0 → (φ (monomial n c)).natDegree = fu n) :
  (φ p).natDegree = fu p.natDegree

Full source

/-- Let `φ : R[x] → S[x]` be an additive map, `k : ℕ` a bound, and `fu : ℕ → ℕ` a
"sufficiently monotone" map.  Assume also that
* `φ` maps to `0` all monomials of degree less than `k`,
* `φ` maps each monomial `m` in `R[x]` to a polynomial `φ m` of degree `fu (deg m)`.
Then, `φ` maps each polynomial `p` in `R[x]` to a polynomial of degree `fu (deg p)`. -/
theorem mono_map_natDegree_eq {S F : Type*} [Semiring S]
    [FunLike F R[X] S[X]] [AddMonoidHomClass F R[X] S[X]] {φ : F}
    {p : R[X]} (k : ℕ) (fu : ℕ → ℕ) (fu0 : ∀ {n}, n ≤ k → fu n = 0)
    (fc : ∀ {n m}, k ≤ n → n < m → fu n < fu m) (φ_k : ∀ {f : R[X]}, f.natDegree < k → φ f = 0)
    (φ_mon_nat : ∀ n c, c ≠ 0 → (φ (monomial n c)).natDegree = fu n) :
    (φ p).natDegree = fu p.natDegree := by
  refine induction_with_natDegree_le (fun p => (φ p).natDegree = fu p.natDegree)
    p.natDegree (by simp [fu0]) ?_ ?_ _ rfl.le
  · intro n r r0 _
    rw [natDegree_C_mul_X_pow _ _ r0, C_mul_X_pow_eq_monomial, φ_mon_nat _ _ r0]
  · intro f g fg _ fk gk
    rw [natDegree_add_eq_right_of_natDegree_lt fg, map_add]
    by_cases FG : k ≤ f.natDegree
    · rw [natDegree_add_eq_right_of_natDegree_lt, gk]
      rw [fk, gk]
      exact fc FG fg
    · cases k
      · exact (FG (Nat.zero_le _)).elim
      · rwa [φ_k (not_le.mp FG), zero_add]

Degree Preservation under Monomial-Compatible Additive Maps

Informal description

Let $R$ and $S$ be semirings, and let $\varphi \colon R[X] \to S[X]$ be an additive map between their polynomial rings. Given a natural number $k$ and a function $f_u \colon \mathbb{N} \to \mathbb{N}$ satisfying: 1. $f_u(n) = 0$ for all $n \leq k$, 2. $f_u$ is strictly increasing on $n \geq k$ (i.e., $f_u(n) < f_u(m)$ whenever $k \leq n < m$), 3. $\varphi$ maps all polynomials of degree less than $k$ to zero, 4. For any monomial $c X^n$ with $c \neq 0$, the degree of $\varphi(c X^n)$ is $f_u(n)$. Then, for any polynomial $p \in R[X]$, the degree of $\varphi(p)$ is equal to $f_u(\deg p)$.

Polynomial.map_natDegree_eq_sub theorem

 {S F : Type*} [Semiring S] [FunLike F R[X] S[X]] [AddMonoidHomClass F R[X] S[X]] {φ : F} {p : R[X]} {k : ℕ}
  (φ_k : ∀ f : R[X], f.natDegree < k → φ f = 0) (φ_mon : ∀ n c, c ≠ 0 → (φ (monomial n c)).natDegree = n - k) :
  (φ p).natDegree = p.natDegree - k

Full source

theorem map_natDegree_eq_sub {S F : Type*} [Semiring S]
    [FunLike F R[X] S[X]] [AddMonoidHomClass F R[X] S[X]] {φ : F}
    {p : R[X]} {k : ℕ} (φ_k : ∀ f : R[X], f.natDegree < k → φ f = 0)
    (φ_mon : ∀ n c, c ≠ 0 → (φ (monomial n c)).natDegree = n - k) :
    (φ p).natDegree = p.natDegree - k :=
  mono_map_natDegree_eq k (fun j => j - k) (by simp_all)
    (@fun _ _ h => (tsub_lt_tsub_iff_right h).mpr)
    (φ_k _) φ_mon

Degree Shift under Monomial-Compatible Additive Maps: $\deg(\varphi(p)) = \deg p - k$

Informal description

Let $R$ and $S$ be semirings, and let $\varphi \colon R[X] \to S[X]$ be an additive map between their polynomial rings. Suppose that: 1. $\varphi$ maps all polynomials of degree less than $k$ to zero. 2. For any monomial $c X^n$ with $c \neq 0$, the degree of $\varphi(c X^n)$ is $n - k$. Then, for any polynomial $p \in R[X]$, the degree of $\varphi(p)$ is equal to $\deg p - k$.

Polynomial.map_natDegree_eq_natDegree theorem

 {S F : Type*} [Semiring S] [FunLike F R[X] S[X]] [AddMonoidHomClass F R[X] S[X]] {φ : F} (p)
  (φ_mon_nat : ∀ n c, c ≠ 0 → (φ (monomial n c)).natDegree = n) : (φ p).natDegree = p.natDegree

Full source

theorem map_natDegree_eq_natDegree {S F : Type*} [Semiring S]
    [FunLike F R[X] S[X]] [AddMonoidHomClass F R[X] S[X]]
    {φ : F} (p) (φ_mon_nat : ∀ n c, c ≠ 0 → (φ (monomial n c)).natDegree = n) :
    (φ p).natDegree = p.natDegree :=
  (map_natDegree_eq_sub (fun _ h => (Nat.not_lt_zero _ h).elim) (by simpa)).trans
    p.natDegree.sub_zero

Degree Preservation under Monomial-Preserving Additive Maps: $\deg(\varphi(p)) = \deg p$

Informal description

Let $R$ and $S$ be semirings, and let $\varphi \colon R[X] \to S[X]$ be an additive map between their polynomial rings. Suppose that for every monomial $c X^n$ with $c \neq 0$, the degree of $\varphi(c X^n)$ is equal to $n$. Then, for any polynomial $p \in R[X]$, the degree of $\varphi(p)$ is equal to the degree of $p$.

Polynomial.card_support_eq' theorem

 {n : ℕ} (k : Fin n → ℕ) (x : Fin n → R) (hk : Function.Injective k) (hx : ∀ i, x i ≠ 0) :
  #(∑ i, C (x i) * X ^ k i).support = n

Full source

theorem card_support_eq' {n : ℕ} (k : Fin n → ℕ) (x : Fin n → R) (hk : Function.Injective k)
    (hx : ∀ i, x i ≠ 0) : #(∑ i, C (x i) * X ^ k i).support = n := by
  suffices (∑ i, C (x i) * X ^ k i).support = image k univ by
    rw [this, univ.card_image_of_injective hk, card_fin]
  simp_rw [Finset.ext_iff, mem_support_iff, finset_sum_coeff, coeff_C_mul_X_pow, mem_image,
    mem_univ, true_and]
  refine fun i => ⟨fun h => ?_, ?_⟩
  · obtain ⟨j, _, h⟩ := exists_ne_zero_of_sum_ne_zero h
    exact ⟨j, (ite_ne_right_iff.mp h).1.symm⟩
  · rintro ⟨j, _, rfl⟩
    rw [sum_eq_single_of_mem j (mem_univ j), if_pos rfl]
    · exact hx j
    · exact fun m _ hmj => if_neg fun h => hmj.symm (hk h)

Cardinality of Support of Polynomial with Distinct Monomials: $|\mathrm{supp}(\sum_i x_i X^{k(i)})| = n$

Informal description

For any natural number $n$, injective function $k \colon \mathrm{Fin}(n) \to \mathbb{N}$, and sequence of nonzero elements $(x_i)_{i \in \mathrm{Fin}(n)}$ in a semiring $R$, the support of the polynomial $\sum_{i} x_i X^{k(i)}$ has cardinality $n$.

Polynomial.card_support_eq theorem

 {n : ℕ} :
  #f.support = n ↔ ∃ (k : Fin n → ℕ) (x : Fin n → R) (_ : StrictMono k) (_ : ∀ i, x i ≠ 0), f = ∑ i, C (x i) * X ^ k i

Full source

theorem card_support_eq {n : ℕ} :
    #f.support#f.support = n ↔
      ∃ (k : Fin n → ℕ) (x : Fin n → R) (_ : StrictMono k) (_ : ∀ i, x i ≠ 0),
        f = ∑ i, C (x i) * X ^ k i := by
  refine ⟨?_, fun ⟨k, x, hk, hx, hf⟩ => hf.symm ▸ card_support_eq' k x hk.injective hx⟩
  induction n generalizing f with
  | zero => exact fun hf => ⟨0, 0, fun x => x.elim0, fun x => x.elim0, card_support_eq_zero.mp hf⟩
  | succ n hn =>
    intro h
    obtain ⟨k, x, hk, hx, hf⟩ := hn (card_support_eraseLead' h)
    have H : ¬∃ k : Fin n, Fin.castSucc k = Fin.last n := by
      rintro ⟨i, hi⟩
      exact i.castSucc_lt_last.ne hi
    refine
      ⟨Function.extend Fin.castSucc k fun _ => f.natDegree,
        Function.extend Fin.castSucc x fun _ => f.leadingCoeff, ?_, ?_, ?_⟩
    · intro i j hij
      have hi : i ∈ Set.range (Fin.castSucc : Fin n → Fin (n + 1)) := by
        rw [Fin.range_castSucc, Set.mem_def]
        exact lt_of_lt_of_le hij (Nat.lt_succ_iff.mp j.2)
      obtain ⟨i, rfl⟩ := hi
      rw [Fin.strictMono_castSucc.injective.extend_apply]
      by_cases hj : ∃ j₀, Fin.castSucc j₀ = j
      · obtain ⟨j, rfl⟩ := hj
        rwa [Fin.strictMono_castSucc.injective.extend_apply, hk.lt_iff_lt,
          ← Fin.castSucc_lt_castSucc_iff]
      · rw [Function.extend_apply' _ _ _ hj]
        apply lt_natDegree_of_mem_eraseLead_support
        rw [mem_support_iff, hf, finset_sum_coeff]
        rw [sum_eq_single, coeff_C_mul, coeff_X_pow_self, mul_one]
        · exact hx i
        · intro j _ hji
          rw [coeff_C_mul, coeff_X_pow, if_neg (hk.injective.ne hji.symm), mul_zero]
        · exact fun hi => (hi (mem_univ i)).elim
    · intro i
      by_cases hi : ∃ i₀, Fin.castSucc i₀ = i
      · obtain ⟨i, rfl⟩ := hi
        rw [Fin.strictMono_castSucc.injective.extend_apply]
        exact hx i
      · rw [Function.extend_apply' _ _ _ hi, Ne, leadingCoeff_eq_zero, ← card_support_eq_zero, h]
        exact n.succ_ne_zero
    · rw [Fin.sum_univ_castSucc]
      simp only [Fin.strictMono_castSucc.injective.extend_apply]
      rw [← hf, Function.extend_apply', Function.extend_apply', eraseLead_add_C_mul_X_pow]
      all_goals exact H

Characterization of Polynomials with Support Cardinality $n$: $|\text{supp}(f)| = n \leftrightarrow f = \sum_{i=0}^{n-1} x_i X^{k(i)}$ with Strictly Increasing $k$ and Nonzero $x_i$

Informal description

For a polynomial $f \in R[X]$ and a natural number $n$, the support of $f$ has cardinality $n$ if and only if there exists a strictly increasing function $k \colon \{0,\dots,n-1\} \to \mathbb{N}$ and a sequence of nonzero coefficients $(x_i)_{i=0}^{n-1}$ in $R$ such that $f$ can be expressed as the sum $\sum_{i=0}^{n-1} x_i X^{k(i)}$.

Polynomial.card_support_eq_one theorem

: #f.support = 1 ↔ ∃ (k : ℕ) (x : R) (_ : x ≠ 0), f = C x * X ^ k

Full source

theorem card_support_eq_one : #f.support#f.support = 1 ↔
    ∃ (k : ℕ) (x : R) (_ : x ≠ 0), f = C x * X ^ k := by
  refine ⟨fun h => ?_, ?_⟩
  · obtain ⟨k, x, _, hx, rfl⟩ := card_support_eq.mp h
    exact ⟨k 0, x 0, hx 0, Fin.sum_univ_one _⟩
  · rintro ⟨k, x, hx, rfl⟩
    rw [support_C_mul_X_pow k hx, card_singleton]

Characterization of Monic Monomials: $|\text{supp}(f)| = 1 \leftrightarrow f = x X^k$ with $x \neq 0$

Informal description

For a polynomial $f \in R[X]$, the support of $f$ has cardinality 1 if and only if there exists a natural number $k$ and a nonzero element $x \in R$ such that $f = x X^k$.

Polynomial.card_support_eq_two theorem

: #f.support = 2 ↔ ∃ (k m : ℕ) (_ : k < m) (x y : R) (_ : x ≠ 0) (_ : y ≠ 0), f = C x * X ^ k + C y * X ^ m

Full source

theorem card_support_eq_two :
    #f.support#f.support = 2 ↔
      ∃ (k m : ℕ) (_ : k < m) (x y : R) (_ : x ≠ 0) (_ : y ≠ 0),
        f = C x * X ^ k + C y * X ^ m := by
  refine ⟨fun h => ?_, ?_⟩
  · obtain ⟨k, x, hk, hx, rfl⟩ := card_support_eq.mp h
    refine ⟨k 0, k 1, hk Nat.zero_lt_one, x 0, x 1, hx 0, hx 1, ?_⟩
    rw [Fin.sum_univ_castSucc, Fin.sum_univ_one]
    rfl
  · rintro ⟨k, m, hkm, x, y, hx, hy, rfl⟩
    exact card_support_binomial hkm.ne hx hy

Characterization of Binomial Polynomials: $|\text{supp}(f)| = 2 \leftrightarrow f = x X^k + y X^m$ with $k < m$ and $x, y \neq 0$

Informal description

For a polynomial $f \in R[X]$ over a semiring $R$, the support of $f$ has cardinality 2 if and only if there exist natural numbers $k < m$ and nonzero elements $x, y \in R$ such that $f = x X^k + y X^m$.

Polynomial.card_support_eq_three theorem

 :
  #f.support = 3 ↔
    ∃ (k m n : ℕ) (_ : k < m) (_ : m < n) (x y z : R) (_ : x ≠ 0) (_ : y ≠ 0) (_ : z ≠ 0),
      f = C x * X ^ k + C y * X ^ m + C z * X ^ n

Full source

theorem card_support_eq_three :
    #f.support#f.support = 3 ↔
      ∃ (k m n : ℕ) (_ : k < m) (_ : m < n) (x y z : R) (_ : x ≠ 0) (_ : y ≠ 0) (_ : z ≠ 0),
        f = C x * X ^ k + C y * X ^ m + C z * X ^ n := by
  refine ⟨fun h => ?_, ?_⟩
  · obtain ⟨k, x, hk, hx, rfl⟩ := card_support_eq.mp h
    refine
      ⟨k 0, k 1, k 2, hk Nat.zero_lt_one, hk (Nat.lt_succ_self 1), x 0, x 1, x 2, hx 0, hx 1, hx 2,
        ?_⟩
    rw [Fin.sum_univ_castSucc, Fin.sum_univ_castSucc, Fin.sum_univ_one]
    rfl
  · rintro ⟨k, m, n, hkm, hmn, x, y, z, hx, hy, hz, rfl⟩
    exact card_support_trinomial hkm hmn hx hy hz

Characterization of Trinomials: $|\text{supp}(f)| = 3 \leftrightarrow f$ is a trinomial with distinct exponents and nonzero coefficients

Informal description

For a polynomial $f \in R[X]$, the support of $f$ has cardinality 3 if and only if there exist natural numbers $k < m < n$ and nonzero elements $x, y, z \in R$ such that $f = x X^k + y X^m + z X^n$.

Definition