deriv_zpow' — Mathlib

English

The derivative operator commutes with the power map: the derivative of x^m is the function x ↦ m x^{m-1}.

Русский

Оператор производной действует на степенную функцию: производная x^m равна функция x ↦ m x^{m-1}.

LaTeX

$$$\\text{deriv }(x \\mapsto x^m) = (x \\mapsto m x^{m-1})$$$

Lean4

@[simp]
theorem deriv_zpow' (m : ℤ) : (deriv fun x : 𝕜 => x ^ m) = fun x => (m : 𝕜) * x ^ (m - 1) :=
  funext <| deriv_zpow m

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