iteratedFDeriv_one_apply — Mathlib

English

The order-1 iterated derivative evaluated on a 1-point index equals the first derivative at that point.

Русский

Производная порядка один, применяемая к единичному индексу, равна производной первого порядка в данной точке.

LaTeX

$$@[simp] theorem iteratedFDeriv_one_apply (m : Fin 1 → E) :\n iteratedFDeriv 𝕜 1 f x m = fderiv 𝕜 f x (m 0)$$

Lean4

@[simp]
theorem iteratedFDeriv_one_apply (m : Fin 1 → E) : iteratedFDeriv 𝕜 1 f x m = fderiv 𝕜 f x (m 0) := by
  rw [iteratedFDeriv_succ_apply_right, iteratedFDeriv_zero_apply, last_zero]

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