English
If either x ≠ 0 or p ≥ 1, then the derivative of x^p with respect to x is p x^{p-1}.
Русский
Пусть либо x ≠ 0, либо p ≥ 1. Тогда производная x^p по x равна p x^{p-1}.
LaTeX
$$$\\text{If } x\\neq 0\\ \\text{or } p\\ge 1,\\ \\dfrac{d}{dx} x^p = p x^{p-1}.$$$
Lean4
theorem hasDerivAt_rpow_const {x p : ℝ} (h : x ≠ 0 ∨ 1 ≤ p) : HasDerivAt (fun x => x ^ p) (p * x ^ (p - 1)) x :=
by
rcases ne_or_eq x 0 with (hx | rfl)
· exact (hasStrictDerivAt_rpow_const_of_ne hx _).hasDerivAt
replace h : 1 ≤ p := h.neg_resolve_left rfl
apply hasDerivAt_of_hasDerivAt_of_ne fun x hx => (hasStrictDerivAt_rpow_const_of_ne hx p).hasDerivAt
exacts [continuousAt_id.rpow_const (Or.inr (zero_le_one.trans h)),
continuousAt_const.mul (continuousAt_id.rpow_const (Or.inr (sub_nonneg.2 h)))]
