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 division ring R with CharZero commutes with the sum of 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 [DivisionRing R] [CharZero R] (g : α → M → ℚ) : (↑(f.sum g) : R) = f.sum fun a b => ↑(g a b) :=
  cast_sum _ _

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