logDeriv_fun_pow — Mathlib

English

For natural exponent n, logDeriv of f^n equals n times logDeriv f.

Русский

Для натурального показателя n logDeriv f^n = n·logDeriv f.

LaTeX

$$$\forall f:\; \mathbb{K}\to\mathbb{K}',\; \forall n\in\mathbb{N},\; \logDeriv\,(f\cdot^n) = n\cdot \logDeriv f$$$

Lean4

theorem logDeriv_fun_pow {f : 𝕜 → 𝕜'} {x : 𝕜} (hdf : DifferentiableAt 𝕜 f x) (n : ℕ) :
    logDeriv (f · ^ n) x = n * logDeriv f x :=
  mod_cast logDeriv_fun_zpow hdf n

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