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