English
In a commutative ring, (x−y)^n expands as a sum with alternating signs and binomial coefficients: (x−y)^n = ∑_{m=0}^n (−1)^{m+n} x^m y^{n−m} binom(n,m).
Русский
В коммутативном кольце разложение (x−y)^n в сумму с знаками по модулю биномиалов: (x−y)^n = ∑_{m=0}^n (−1)^{m+n} x^m y^{n−m} binom(n,m).
LaTeX
$$$ (x-y)^n = \sum_{m=0}^n (-1)^{m+n} x^m y^{n-m} \binom{n}{m} $$$
Lean4
/-- A special case of the **binomial theorem** -/
theorem sub_pow [CommRing R] (x y : R) (n : ℕ) :
(x - y) ^ n = ∑ m ∈ range (n + 1), (-1) ^ (m + n) * x ^ m * y ^ (n - m) * n.choose m :=
by
rw [sub_eq_add_neg, add_pow]
congr! 1 with m hm
have : (-1 : R) ^ (n - m) = (-1) ^ (n + m) := by
rw [mem_range] at hm
simp [show n + m = n - m + 2 * m by cutsat, pow_add]
rw [neg_pow, this]
ring
