natDegree_derivative_lt — Mathlib

English

If natDegree(p) ≠ 0, then natDegree(p') < natDegree(p).

Русский

Если natDegree(p) ≠ 0, то natDegree(p') < natDegree(p).

LaTeX

$$$\text{natDegree}(p') < \text{natDegree}(p)$ whenever $\text{natDegree}(p) \neq 0$$$

Lean4

theorem natDegree_derivative_lt {p : R[X]} (hp : p.natDegree ≠ 0) : p.derivative.natDegree < p.natDegree :=
  by
  rcases eq_or_ne (derivative p) 0 with hp' | hp'
  · rw [hp', Polynomial.natDegree_zero]
    exact hp.bot_lt
  · rw [natDegree_lt_natDegree_iff hp']
    exact degree_derivative_lt fun h => hp (h.symm ▸ natDegree_zero)

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