exp_sum — Mathlib

English

For s a finite set and f: α → ℝ, exp(sum_{x∈s} f(x)) = prod_{x∈s} exp(f(x)).

Русский

Для конечного множества s и функции f: α → ℝ: exp(сумма_{x∈s} f(x)) = произведение_{x∈s} exp(f(x)).

LaTeX

$$$\\exp\\left(\\sum x \\in s \\; f(x)\\right) = \\prod_{x \\in s} \\exp(f(x))$$$

Lean4

theorem exp_sum {α : Type*} (s : Finset α) (f : α → ℝ) : exp (∑ x ∈ s, f x) = ∏ x ∈ s, exp (f x) :=
  map_prod (M := Multiplicative ℝ) expMonoidHom f s

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