English
Let M be a commutative monoid and f: N × N → M. Then the product over all (i,j) in the antidiagonal of size n+1 of f(i,j)^{C(n+1,i)} equals the product over the antidiagonal of size n of f(i, j+1)^{C(n,i)} times the product over the antidiagonal of size n of f(i+1, j)^{C(n,j)}.
Русский
Пусть M — коммутативная моноида, f: ℕ × ℕ → M. Тогда произведение по всем парам (i,j) на антидиагонали размера n+1 from f(i,j)^{C(n+1,i)} равно произведению по антидиагонали размера n от f(i, j+1)^{C(n,i)} умноженному на произведение по антидиагонали размера n от f(i+1, j)^{C(n,j)}.
LaTeX
$$$$\prod_{(i,j) \in \operatorname{antidiagonal}(n+1)} f(i,j)^{\binom{n+1}{i}} = \Big(\prod_{(i,j) \in \operatorname{antidiagonal}(n)} f(i, j+1)^{\binom{n}{i}}\Big) \cdot \Big(\prod_{(i,j) \in \operatorname{antidiagonal}(n)} f(i+1, j)^{\binom{n}{j}}\Big).$$$$
Lean4
@[to_additive sum_antidiagonal_choose_succ_nsmul]
theorem prod_antidiagonal_pow_choose_succ {M : Type*} [CommMonoid M] (f : ℕ → ℕ → M) (n : ℕ) :
(∏ ij ∈ antidiagonal (n + 1), f ij.1 ij.2 ^ (n + 1).choose ij.1) =
(∏ ij ∈ antidiagonal n, f ij.1 (ij.2 + 1) ^ n.choose ij.1) *
∏ ij ∈ antidiagonal n, f (ij.1 + 1) ij.2 ^ n.choose ij.2 :=
by
simp only [Nat.prod_antidiagonal_eq_prod_range_succ_mk, prod_pow_choose_succ]
have : ∀ i ∈ range (n + 1), i ≤ n := fun i hi ↦ by simpa [Nat.lt_succ_iff] using hi
congr 1
· refine prod_congr rfl fun i hi ↦ ?_
rw [tsub_add_eq_add_tsub (this _ hi)]
· refine prod_congr rfl fun i hi ↦ ?_
rw [choose_symm (this _ hi)]
