cast_finsupp_sum — Mathlib

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 coincides with 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 [AddCommGroupWithOne R] (g : α → M → ℤ) : (↑(f.sum g) : R) = f.sum fun a b => ↑(g a b) :=
  Int.cast_sum _ _

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