exp_sum — Mathlib

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 _ _

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