iteratedFDeriv_succ_const — Mathlib

English

If n ≠ 0, then the nth iterated derivative of a constant function is zero: iteratedFDeriv 𝕜 n (x ↦ c) = 0.

Русский

Если n ≠ 0, то n-я итерационная производная константы равна нулю: iteratedFDeriv 𝕜 n (x ↦ c) = 0.

LaTeX

$$$ n \neq 0 \Rightarrow \operatorname{iteratedFDeriv}_{\mathbb{K}}^{n}(x \mapsto c) = 0 $$$

Lean4

theorem iteratedFDeriv_succ_const (n : ℕ) (c : F) : (iteratedFDeriv 𝕜 (n + 1) fun _ : E ↦ c) = 0 :=
  iteratedFDeriv_const_of_ne (by simp) _

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