English
For any f: Fin(a+b) → M (M commutative monoid), the product over Fin(a+b) equals the product over Fin a of f(castAdd b i) multiplied by the product over Fin b of f(natAdd a i).
Русский
Для любого f: Fin(a+b) → M произведение по Fin(a+b) равно произведению по Fin a от f(castAdd b i) умноженному на произведение по Fin b от f(natAdd a i).
LaTeX
$$$\displaystyle \prod_{i \in \mathrm{Fin}(a+b)} f(i) = \left(\prod_{i \in \mathrm{Fin}(a)} f(\mathrm{castAdd}(b,i))\right) \cdot \left(\prod_{i \in \mathrm{Fin}(b)} f(\mathrm{natAdd}(a,i))\right).$$$
Lean4
@[to_additive]
theorem prod_univ_add {a b : ℕ} (f : Fin (a + b) → M) :
(∏ i : Fin (a + b), f i) = (∏ i : Fin a, f (castAdd b i)) * ∏ i : Fin b, f (natAdd a i) :=
by
rw [Fintype.prod_equiv finSumFinEquiv.symm f fun i => f (finSumFinEquiv.toFun i)]
· apply Fintype.prod_sum_type
· intro x
simp only [Equiv.toFun_as_coe, Equiv.apply_symm_apply]
