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