logDeriv_const_mul — Mathlib

English

logDeriv of a constant multiple equals logDeriv of the function (multiplier not affecting derivative).

Русский

logDeriv от константного множителя функции равен logDeriv самой функции; множитель не влияет на производную.

LaTeX

$$$\forall f:\; \logDeriv(\lambda z. a\cdot f(z)) x = \logDeriv f x$ при $a\neq 0$$$

Lean4

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

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