English
Let f be a finitely supported function α → M and g a function α → M → ℤ. Casting the sum f.sum g from ℤ to a commutative additive ring R commutes with the sum of casts: the cast of the sum equals the sum of the casts.
Русский
Пусть f — конечноподдерживаемая функция α → M, а g — функция α → M → ℤ. Приведение суммы f.sum g из ℤ в R сопряжено со сложением: приведённая сумма равна сумме приведений.
LaTeX
$$$\\bigl( f.sum\\, g \\bigr)^{\\uparrow} = f.sum\\, (a,b \\mapsto \\uparrow\\bigl(g\\,a\,b\\bigr)).$$$
Lean4
@[simp, norm_cast]
theorem cast_finsupp_sum [AddCommMonoidWithOne R] (g : α → M → ℕ) : (↑(f.sum g) : R) = f.sum fun a b => ↑(g a b) :=
Nat.cast_sum _ _
