logDeriv_zpow — Mathlib

English

For a nontrivial normed field, the log-derivative of the map x ↦ x^n is n/x for every x ≠ 0 and integer n.

Русский

Пусть 𝕜 — ненулевое нормированное поле. Тогда логарифм производной отображения x ↦ x^n равен n/x для всех x ≠ 0 и целого n.

LaTeX

$$$\displaystyle \logDeriv\bigl(x \mapsto x^n\bigr)(x) = \frac{n}{x}$$$

Lean4

@[simp]
theorem logDeriv_zpow (x : 𝕜) (n : ℤ) : logDeriv (· ^ n) x = n / x := by
  rw [logDeriv_fun_zpow (by fun_prop), logDeriv_id', mul_one_div]

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