Mathlib.Algebra.Polynomial.Degree.Monomial

Polynomial.natDegree_le_pred theorem

(hf : p.natDegree ≤ n) (hn : p.coeff n = 0) : p.natDegree ≤ n - 1

Full source

lemma natDegree_le_pred (hf : p.natDegree ≤ n) (hn : p.coeff n = 0) : p.natDegree ≤ n - 1 := by
  obtain _ | n := n
  · exact hf
  · refine (Nat.le_succ_iff_eq_or_le.1 hf).resolve_left fun h ↦ ?_
    rw [← Nat.succ_eq_add_one, ← h, coeff_natDegree, leadingCoeff_eq_zero] at hn
    aesop

Degree Bound When Leading Coefficient Vanishes: $\deg(p) \leq n \land p_n = 0 \implies \deg(p) \leq n-1$

Informal description

For a univariate polynomial $p$ over a semiring $R$, if the degree of $p$ is at most $n$ and the coefficient of $X^n$ in $p$ is zero, then the degree of $p$ is at most $n-1$.

Polynomial.monomial_natDegree_leadingCoeff_eq_self theorem

(h : #p.support ≤ 1) : monomial p.natDegree p.leadingCoeff = p

Full source

theorem monomial_natDegree_leadingCoeff_eq_self (h : #p.support ≤ 1) :
    monomial p.natDegree p.leadingCoeff = p := by
  classical
  rcases card_support_le_one_iff_monomial.1 h with ⟨n, a, rfl⟩
  by_cases ha : a = 0 <;> simp [ha]

Monomial Characterization via Degree and Leading Coefficient: $p = aX^{\deg p}$ when $\#\text{supp}(p) \leq 1$

Informal description

For any polynomial $p$ over a semiring $R$ with at most one nonzero coefficient (i.e., $\#\text{supp}(p) \leq 1$), $p$ is equal to the monomial $aX^n$, where $n$ is the degree of $p$ and $a$ is its leading coefficient.

Polynomial.C_mul_X_pow_eq_self theorem

(h : #p.support ≤ 1) : C p.leadingCoeff * X ^ p.natDegree = p

Full source

theorem C_mul_X_pow_eq_self (h : #p.support ≤ 1) : C p.leadingCoeff * X ^ p.natDegree = p := by
  rw [C_mul_X_pow_eq_monomial, monomial_natDegree_leadingCoeff_eq_self h]

Monomial Characterization: $p = aX^n$ when $\#\mathrm{supp}(p) \leq 1$

Informal description

For any polynomial $p$ over a semiring $R$ with at most one nonzero coefficient (i.e., $\#\mathrm{supp}(p) \leq 1$), $p$ is equal to the monomial formed by its leading coefficient and degree, i.e., $$ p = aX^n $$ where $a$ is the leading coefficient of $p$ and $n$ is its degree.