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