exp_sum — Mathlib

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

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