coe_sum — Mathlib

English

The image under the inclusion map of a finite sum equals the sum of images.

Русский

Изображение конечной суммы через включение равно сумме изображений.

LaTeX

$$$\uparrow(\sum_{i\in s} x_i) = \sum_{i\in s} \uparrow x_i$$$

Lean4

/-- Note the `AddSubmonoid` version of this lemma is called `AddSubmonoid.coe_finset_sum`. -/
theorem coe_sum (x : ι → p) (s : Finset ι) : ↑(∑ i ∈ s, x i) = ∑ i ∈ s, (x i : M) :=
  map_sum p.subtype _ _

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