English
Let M be a commutative monoid and f: N × N → M. Then for any n, the product over i = 0,…,n+1 of f(i, n+1−i)^{C(n+1,i)} equals the product over i = 0,…,n of f(i, n+1−i)^{C(n,i)} times the product over i = 0,…,n of f(i+1, n−i)^{C(n,i)}.
Русский
Пусть M — коммутативная моноида, f: ℕ × ℕ → M. Тогда для любого n произведение по i от 0 до n+1 of f(i, n+1−i)^{C(n+1,i)} равно произведению по i от 0 до n of f(i, n+1−i)^{C(n,i)} умноженному на произведение по i от 0 до n of f(i+1, n−i)^{C(n,i)}.
LaTeX
$$$$\prod_{i=0}^{n+1} f(i, n+1-i)^{\binom{n+1}{i}} = \left(\prod_{i=0}^{n} f(i, n+1-i)^{\binom{n}{i}}\right) \cdot \left(\prod_{i=0}^{n} f(i+1, n-i)^{\binom{n}{i}}\right).$$$$
Lean4
@[to_additive sum_choose_succ_nsmul]
theorem prod_pow_choose_succ {M : Type*} [CommMonoid M] (f : ℕ → ℕ → M) (n : ℕ) :
(∏ i ∈ range (n + 2), f i (n + 1 - i) ^ (n + 1).choose i) =
(∏ i ∈ range (n + 1), f i (n + 1 - i) ^ n.choose i) * ∏ i ∈ range (n + 1), f (i + 1) (n - i) ^ n.choose i :=
by
have A :
(∏ i ∈ range (n + 1), f (i + 1) (n - i) ^ (n.choose (i + 1))) * f 0 (n + 1) =
∏ i ∈ range (n + 1), f i (n + 1 - i) ^ (n.choose i) :=
by rw [prod_range_succ, prod_range_succ']; simp
rw [prod_range_succ']
simpa [choose_succ_succ, pow_add, prod_mul_distrib, A, mul_assoc] using mul_comm _ _
