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