English
Let M be a commutative monoid. For h : n = m, a ∈ Fin n, and f : Fin m → M, the product over i < a.cast h equals the product over i < a of f(i.cast h).
Русский
Пусть M — коммутативный моноид. При h : n = m, a ∈ Fin n и f : Fin m → M произведение по i < a.cast(h) равно произведению по i < a от f(i.cast(h)).
LaTeX
$$$$ \\displaystyle \\prod_{i < a^{\\mathrm{cast}(h)}} f(i) = \\prod_{i < a} f(i^{\\mathrm{cast}(h)}) $$$$
Lean4
@[to_additive]
theorem prod_Iio_cast (h : n = m) (f : Fin m → M) (a : Fin n) : ∏ i < a.cast h, f i = ∏ i < a, f (i.cast h) := by
simp [← map_finCongr_Iio]