English
Let s be a finite set and f: α → ℂ. Then exp (sum_{x in s} f(x)) = product_{x in s} exp(f(x)).
Русский
Пусть s — конечное множество и f: α → ℂ. Тогда exp(сумма по x ∈ s f(x)) равна произведению exp(f(x)) по всем x ∈ s.
LaTeX
$$$\\exp\\left(\\sum_{x \\in s} f(x)\\right) = \\prod_{x \\in s} \\exp\\left(f(x)\\right)$$$
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