English
Let f be a finitely supported function α → M and g a function α → M → ℚ. The product over α of g(a,b) with respect to f, when cast to a field R of characteristic zero, equals the product over α of g(a,b) cast to R, i.e., the cast commutes with finsupp.prod.
Русский
Пусть f — конечноподдерживаемая функция α → M, а g — функция α → M → ℚ. Произведение по α от g(a,b) относительно f, приводимое к полю R нулевой характеристики, равно произведению приводимых значений g(a,b).
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 [Field R] [CharZero R] (g : α → M → ℚ) : (↑(f.prod g) : R) = f.prod fun a b => ↑(g a b) :=
cast_prod _ _
