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