English
For a function f: N × N → M into a semiring M, the sum over the antidiagonal of size n+1 of f(i,j) to the power (n+1 choose i) equals the product of two sums over antidiagonal of size n with shifted indices.
Русский
Для функции f: ℕ × ℕ → M, сумма по антидиагонали размера n+1 от f(i,j)^{(n+1 choose i)} равна произведению двух сумм по антидиагонали размера n с сдвинутыми индексами.
LaTeX
$$$$\sum_{(i,j) \in \operatorname{antidiagonal}(n+1)} f(i,j)^{\binom{n+1}{i}} = \left(\sum_{(i,j) \in \operatorname{antidiagonal}(n)} f(i, j+1)^{\binom{n}{i}}\right) \cdot \left(\sum_{(i,j) \in \operatorname{antidiagonal}(n)} f(i+1, j)^{\binom{n}{j}}\right).$$$$
Lean4
/-- The sum along the antidiagonal of `(n+1).choose i * f i j` can be split into two sums along the
antidiagonal at rank `n`, respectively of `n.choose i * f i (j+1)` and `n.choose j * f (i+1) j`. -/
theorem sum_antidiagonal_choose_succ_mul (f : ℕ → ℕ → R) (n : ℕ) :
(∑ ij ∈ antidiagonal (n + 1), ((n + 1).choose ij.1 : R) * f ij.1 ij.2) =
(∑ ij ∈ antidiagonal n, (n.choose ij.1 : R) * f ij.1 (ij.2 + 1)) +
∑ ij ∈ antidiagonal n, (n.choose ij.2 : R) * f (ij.1 + 1) ij.2 :=
by simpa only [nsmul_eq_mul] using sum_antidiagonal_choose_succ_nsmul f n
