coe_finset_sum — Mathlib

English

The coercion of the sum ∑ i∈S f_i equals the sum of the coerced f_i.

Русский

Коэрцирование суммы ∑ i∈S f_i равно сумме коэрцированных f_i.

LaTeX

$$$$ \\Big( \\sum_{i\\in S} f_i \\Big)^{\\uparrow} = \\sum_{i\\in S} f_i^{\\uparrow} $$$$

Lean4

@[simp, norm_cast]
theorem coe_finset_sum [AddCommMonoid N] (S : Finset ι) (f : ι → α →₀ N) : ⇑(∑ i ∈ S, f i) = ∑ i ∈ S, ⇑(f i) :=
  map_sum (coeFnAddHom : (α →₀ N) →+ _) _ _

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