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