Power_Rule_for_Derivatives
Provedderivativespower-rule-for-derivativesproofwiki
Let n be a natural number. Let f: R -> R be the real function defined as f(x) = x^n. Then f'(x) = n * x^(n-1).
Preamble
import Mathlib.Analysis.SpecialFunctions.Pow.Deriv import Mathlib.Analysis.Calculus.Deriv.Pow
Formal statement
theorem Power_Rule_for_Derivatives (n : ℕ) (x : ℝ) (hx : x ≠ 0) : deriv (fun x => x ^ (n : ℕ)) x = ↑n * x ^ (n - 1) := by sorry
Source