English
A strengthened form of the binomial theorem sum over all indices using an antidiagonal split and binomial weights.
Русский
Усиленная форма биномиальной теоремы с суммированием по всем индексам через разложение по антидиагонали и биномиальные веса.
LaTeX
$$$ (x+y)^n = \sum_{m\in[0,n]} x^m y^{n-m} \binom{n}{m} $$$
Lean4
/-- A version of `Commute.add_pow` that avoids ℕ-subtraction by summing over the antidiagonal and
also with the binomial coefficient applied via scalar action of ℕ. -/
theorem add_pow' (h : Commute x y) (n : ℕ) : (x + y) ^ n = ∑ m ∈ antidiagonal n, n.choose m.1 • (x ^ m.1 * y ^ m.2) :=
by
simp_rw [Nat.sum_antidiagonal_eq_sum_range_succ fun m p ↦ n.choose m • (x ^ m * y ^ p), nsmul_eq_mul, cast_comm,
h.add_pow]
