iterate_derivative_eq_zero — Mathlib

English

If the natDegree of p is less than x, then the x-th derivative of p is zero.

Русский

Если natDegree p < x, то x-я производная p равна нулю.

LaTeX

$$$\text{natDegree}(p) < x \Rightarrow \operatorname{derivative}^{x}(p) = 0$$$

Lean4

theorem iterate_derivative_eq_zero {p : R[X]} {x : ℕ} (hx : p.natDegree < x) : Polynomial.derivative^[x] p = 0 :=
  by
  induction h : p.natDegree using Nat.strong_induction_on generalizing p x with
  | _ _ ih
  subst h
  obtain ⟨t, rfl⟩ := Nat.exists_eq_succ_of_ne_zero (pos_of_gt hx).ne'
  rw [Function.iterate_succ_apply]
  by_cases hp : p.natDegree = 0
  · rw [derivative_of_natDegree_zero hp, iterate_derivative_zero]
  have := natDegree_derivative_lt hp
  exact ih _ this (this.trans_le <| Nat.le_of_lt_succ hx) rfl

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