deriv_ofReal_cpow_const — Mathlib

English

For real x ≠ 0 and c ≠ 0, the derivative with respect to the real variable of x ↦ (x^{c}) (viewed in ℂ) equals c x^{c-1}.

Русский

Для действительного x ≠ 0 и c ≠ 0 производная по действительной переменной функции x ↦ (x^{c}) (как комплексная) равна c x^{c-1}.

LaTeX

$$$\\text{Let }x\\in\\mathbb{R},\\ x\\neq 0:\\ \\dfrac{d}{dx} (x^{c}) = c x^{c-1}.$$$

Lean4

/-- A version of `Complex.deriv_cpow_const` for a real variable. -/
theorem deriv_ofReal_cpow_const {x : ℝ} (hx : x ≠ 0) (hc : c ≠ 0) :
    deriv (fun x : ℝ ↦ (x : ℂ) ^ c) x = c * x ^ (c - 1) :=
  (hasDerivAt_ofReal_cpow_const hx hc).deriv

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