natDegree_le_pred — Mathlib

English

If n is such that coeff p n ≠ 0, then n ≤ natDegree p.

Русский

Если коэффициент p на позиции n не равен нулю, то n ≤ natDegree p.

LaTeX

$$$p.\\text{coeff}(n) \\neq 0 \\Rightarrow n \\leq \\operatorname{natDegree}(p)$$$

Lean4

theorem 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
    simp_all

Похожие утверждения