deriv_zpow — Mathlib

English

The derivative of x^m at x is m x^{m−1} (under the usual differentiability conditions).

Русский

Производная от x^m в точке x равна m x^{m−1} при обычных условиях дифференцируемости.

LaTeX

$$$\\frac{d}{dx} x^m = m \\cdot x^{m-1}$ (при допустимых x)$$

Lean4

theorem deriv_zpow (m : ℤ) (x : 𝕜) : deriv (fun x => x ^ m) x = m * x ^ (m - 1) :=
  by
  by_cases H : x ≠ 0 ∨ 0 ≤ m
  · exact (hasDerivAt_zpow m x H).deriv
  · rw [deriv_zero_of_not_differentiableAt (mt differentiableAt_zpow.1 H)]
    push_neg at H
    rcases H with ⟨rfl, hm⟩
    rw [zero_zpow _ ((sub_one_lt _).trans hm).ne, mul_zero]

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