re_sum — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem re_sum (f : α → ℂ) : (∑ i ∈ s, f i).re = ∑ i ∈ s, (f i).re :=
  map_sum reAddGroupHom f s

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