coe_sum — Mathlib

English

Sum commutes with the coercion to WithBot: the sum in M over s equals the sum in WithBot M of the coerced values.

Русский

Сумма по множеству Finset сохраняется при внедрении в WithBot: сумма над s равна сумме после отображения в WithBot M.

LaTeX

$$$\sum_{i\in s} f(i) = \sum_{i\in s} (f(i) : WithBot\ M)$$$

Lean4

@[simp, norm_cast]
theorem coe_sum (s : Finset ι) (f : ι → M) : ∑ i ∈ s, f i = ∑ i ∈ s, (f i : WithBot M) :=
  map_sum addHom f s

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