expMonoidHom — Mathlib

English

For any finite list l of complex numbers, the exponential of the sum equals the product of the exponentials of the elements: exp(sum l) = product (map exp l).

Русский

Для любого конечного списка комплексных чисел l выполнено exp(sum l) = prod (map exp l).

LaTeX

$$$\\forall \\ell: \\text{List}(\\mathbb{C}),\\; \\exp(\\sum \\ell) = \\prod (\\ell.map(\\exp))$$$

Lean4

/-- the exponential function as a monoid hom from `Multiplicative ℂ` to `ℂ` -/
@[simps]
noncomputable def expMonoidHom : MonoidHom (Multiplicative ℂ) ℂ :=
  { toFun := fun z => exp z.toAdd, map_one' := by simp, map_mul' := by simp [exp_add] }

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