deriv_pow — Mathlib

English

For DifferentiableAt f x, the derivative of f^n is the sum with deriv f x in place of derivative.

Русский

Для DifferentiableAt f x производная f^n равна сумме с deriv f x на месте производной.

LaTeX

$$$$\frac{d}{dx}\bigl(f(x)^n\bigr)=\sum_{i=0}^{n-1} f(x)^{\,n-1-i}\, (\frac{d}{dx} f(x))\, f(x)^{\,i}. $$$$

Lean4

@[simp]
theorem deriv_pow (h : DifferentiableAt 𝕜 f x) (n : ℕ) : deriv (f ^ n) x = n * f x ^ (n - 1) * deriv f x :=
  deriv_fun_pow h n

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