exp_multiset_sum — Mathlib

English

Let s be a multiset of complex numbers. Then exp(sum s) equals the product of exp of each element.

Русский

Пусть s — мультисет комплексных чисел. Тогда exp суммы элементов равна произведению exp каждого элемента.

LaTeX

$$$\\exp\\left(\\sum_{a \\in s} a\\right) = \\prod_{a \\in s} \\exp(a)$$$

Lean4

theorem exp_multiset_sum (s : Multiset ℂ) : exp s.sum = (s.map exp).prod :=
  @MonoidHom.map_multiset_prod (Multiplicative ℂ) ℂ _ _ expMonoidHom s

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