cast_sum — Mathlib

English

Let s be a finite set (Finset) and f a function from an index set to Nat. The cast of the sum over s of f equals the sum of the casts of the f-values: ↑(∑ x∈s, f x) = ∑ x∈s, (f x).

Русский

Пусть s — конечное множество индексов, f: индексы → Nat. Пробразование суммы f по s равно сумме образов: ↑(∑ x∈s, f x) = ∑ x∈s, (f x).

LaTeX

$$$\left(\sum_{x \in s} f(x)\right)^{\uparrow} = \sum_{x \in s} (f(x))^{\uparrow}$$$

Lean4

@[simp, norm_cast]
theorem cast_sum [AddCommMonoidWithOne R] (s : Finset ι) (f : ι → ℕ) : ↑(∑ x ∈ s, f x : ℕ) = ∑ x ∈ s, (f x : R) :=
  map_sum (castAddMonoidHom R) _ _

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