hasDerivAt_pow

theorem hasDerivAt_pow : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (n : ℕ) (x : 𝕜), HasDerivAt (fun x => x ^ n) (↑n * x ^ (n - 1)) x

This theorem states that, for any non-trivially normed field `𝕜` and any natural number `n`, the derivative of the function `f(x) = x^n` at a point `x` in `𝕜` is `n * x^(n - 1)`. In other words, it asserts the power rule of calculus in the context of non-trivially normed fields. The power rule says that the derivative of `x^n` with respect to `x` is `n*x^(n-1)`.

More concisely: For any non-trivially normed field and natural number, the derivative of the function `x => x^n` is `n * x^(n-1)`.