coe_sum — Mathlib

English

Sum of elements of an indexed family in an intermediate field, when viewed inside L, equals the sum of the embedded elements in L.

Русский

Сумма элементов семейства, взятого по индексу, внутри промежуточного поля равна сумме изображений этих элементов в L.

LaTeX

$$$\\left( \\uparrow\\left( \\sum_{i} f(i) \\right) : L \\right) = \\sum_{i} (f(i) : L)$$$

Lean4

@[norm_cast]
theorem coe_sum {ι : Type*} [Fintype ι] (f : ι → S) : (↑(∑ i, f i) : L) = ∑ i, (f i : L) :=
  AddSubmonoidClass.coe_finset_sum f Finset.univ

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