derivWithin_fun_pow — Mathlib

English

For any n, derive (x^n) within a field: d/dx (x^n) = n x^{n-1}.

Русский

Для функции x↦x^n на поле: производная dx (x^n) = n x^{n-1}.

LaTeX

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

Lean4

@[simp]
theorem derivWithin_fun_pow (h : DifferentiableWithinAt 𝕜 f s x) (n : ℕ) :
    derivWithin (fun x => f x ^ n) s x = n * f x ^ (n - 1) * derivWithin f s x :=
  by
  by_cases hsx : UniqueDiffWithinAt 𝕜 s x
  · exact (h.hasDerivWithinAt.pow n).derivWithin hsx
  · simp [derivWithin_zero_of_not_uniqueDiffWithinAt hsx]

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