logDeriv_mul_const — Mathlib

English

logDeriv of f^n equals n times logDeriv f for integer exponent n, provided f(x) ≠ 0 and differentiability.

Русский

logDeriv от f^n равен n умножить на logDeriv f при целочисленном показателе n, если f(x) ≠ 0 и функция дифференцируема.

LaTeX

$$$\forall n\in\mathbb{Z},\; f(x)\neq 0,\; \text{DifferentiableAt } f x\Rightarrow \logDeriv\,(f^n) x = n \cdot \logDeriv f x$$$

Lean4

theorem logDeriv_mul_const {f : 𝕜 → 𝕜'} (x : 𝕜) (a : 𝕜') (ha : a ≠ 0) : logDeriv (fun z => f z * a) x = logDeriv f x :=
  by simp only [logDeriv_apply, deriv_mul_const_field, mul_div_mul_right _ _ ha]

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