ofReal_sum — Mathlib

English

For a finite index set s and f: α → ℝ, the complex embedding of the sum equals the sum of the complex embeddings: (∑ i ∈ s, f i) viewed in ℂ equals ∑ i ∈ s, (f i) viewed in ℂ.

Русский

Для конечного множества индексов s и функции f: α → ℝ справедливо: сумма f(i) по i∈s, взятая как комплекс, равна сумме комплексизации каждого слагаемого.

LaTeX

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

Lean4

@[simp, norm_cast]
theorem ofReal_sum (f : α → ℝ) : ((∑ i ∈ s, f i : ℝ) : ℂ) = ∑ i ∈ s, (f i : ℂ) :=
  map_sum ofRealHom _ _

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