English
For a finite set, exp(∑ f_i) equals the product over i of exp(f_i).
Русский
Для конечного множества элементов exp(∑ f_i) равно произведению exp(f_i) по всем i.
LaTeX
$$$\\exp 𝕂\\left(\\sum_{i \\in s} f(i)\\right) = \\prod_{i \\in s} \\exp 𝕂(f(i))$$$
Lean4
/-- A version of `NormedSpace.exp_sum_of_commute` for a commutative Banach-algebra. -/
theorem exp_sum {ι} (s : Finset ι) (f : ι → 𝔸) : exp 𝕂 (∑ i ∈ s, f i) = ∏ i ∈ s, exp 𝕂 (f i) :=
by
rw [exp_sum_of_commute, Finset.noncommProd_eq_prod]
exact fun i _hi j _hj _ => Commute.all _ _