ofReal_sum — Mathlib

English

For a finite set s and a real-valued function f, the embedding commutes with finite sums: ((∑ i ∈ s, f i : ℝ) : K) = ∑ i ∈ s, (f i : K).

Русский

Для конечного множества s и функции f: отображение сохраняет сумму: ((∑ i ∈ s, f i) : K) = ∑ i ∈ s, (f i : K).

LaTeX

$$$\left(\sum_{i \in s} f_i : \mathbb{R}\right) : K = \sum_{i \in s} (f_i : K)$$$

Lean4

@[rclike_simps, norm_cast]
theorem ofReal_sum {α : Type*} (s : Finset α) (f : α → ℝ) : ((∑ i ∈ s, f i : ℝ) : K) = ∑ i ∈ s, (f i : K) :=
  map_sum (algebraMap ℝ K) _ _

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