degree_derivative_lt — Mathlib

English

If p ≠ 0, then the degree of the derivative is strictly less than the degree of p: deg(p') < deg(p).

Русский

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

LaTeX

$$$\deg(p') < \deg(p)$ for p \neq 0$$

Lean4

theorem degree_derivative_lt {p : R[X]} (hp : p ≠ 0) : p.derivative.degree < p.degree :=
  (Finset.sup_lt_iff <| bot_lt_iff_ne_bot.2 <| mt degree_eq_bot.1 hp).2 fun n hp =>
    lt_of_lt_of_le (WithBot.coe_lt_coe.2 n.lt_succ_self) <| Finset.le_sup <| of_mem_support_derivative hp

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