im_sum — Mathlib

English

The imaginary part of a finite sum equals the sum of the imaginary parts: Im(∑ f(i)) = ∑ Im(f(i)).

Русский

Мнимая часть суммы равна сумме мнимых частей: Im(∑ f(i)) = ∑ Im(f(i)).

LaTeX

$$$$ \operatorname{Im}\left( \sum_{i \in s} f(i) \right) = \sum_{i \in s} \operatorname{Im}\big( f(i) \big) $$$$

Lean4

@[simp]
theorem im_sum (f : α → ℂ) : (∑ i ∈ s, f i).im = ∑ i ∈ s, (f i).im :=
  map_sum imAddGroupHom f s

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