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