logDeriv_prod — Mathlib

English

If s is a finite set and f: s → R has nonzero values, then logDeriv of the finite product equals the sum of the logDeriv of the factors.

Русский

Если s — конечное множество и f: s → R принимает ненулевые значения, то logDeriv произведения по s равен сумме logDeriv каждого f(x).

LaTeX

$$$\\logDeriv\\left(\\prod_{x \\in s} f(x)\\right) = \\sum_{x \\in s} \\logDeriv(f(x))$$$

Lean4

theorem logDeriv_prod (ι : Type*) (s : Finset ι) (f : ι → R) (h : ∀ x ∈ s, f x ≠ 0) :
    logDeriv (∏ x ∈ s, f x) = ∑ x ∈ s, logDeriv (f x) :=
  logDeriv_multisetProd _ h

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