English
In a semiring where two elements commute, the nth power of their sum expands as a finite sum with binomial coefficients and monomials x^m y^{n-m}.
Русский
В полусложенном кольце при условии взаимной коммутативности элементов x,y распадается (x+y)^n в конечную сумму с коэффициентами бинома и степенями x^m y^{n-m}.
LaTeX
$$$ (x+y)^n = \sum_{m=0}^n \binom{n}{m} x^m y^{n-m} $$$
Lean4
/-- A version of the **binomial theorem** for commuting elements in noncommutative semirings. -/
theorem add_pow (h : Commute x y) (n : ℕ) : (x + y) ^ n = ∑ m ∈ range (n + 1), x ^ m * y ^ (n - m) * n.choose m :=
by
let t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * n.choose m
change (x + y) ^ n = ∑ m ∈ range (n + 1), t n m
have h_first : ∀ n, t n 0 = y ^ n := fun n ↦ by
simp only [t, choose_zero_right, pow_zero, cast_one, mul_one, one_mul, tsub_zero]
have h_last : ∀ n, t n n.succ = 0 := fun n ↦ by simp only [t, choose_succ_self, cast_zero, mul_zero]
have h_middle : ∀ n i : ℕ, i ∈ range n.succ → (t n.succ i.succ) = x * t n i + y * t n i.succ :=
by
intro n i h_mem
have h_le : i ≤ n := le_of_lt_succ (mem_range.mp h_mem)
dsimp only [t]
rw [choose_succ_succ, cast_add, mul_add]
congr 1
· rw [pow_succ' x, succ_sub_succ, mul_assoc, mul_assoc, mul_assoc]
· rw [← mul_assoc y, ← mul_assoc y, (h.symm.pow_right i.succ).eq]
by_cases h_eq : i = n
· rw [h_eq, choose_succ_self, cast_zero, mul_zero, mul_zero]
· rw [succ_sub (lt_of_le_of_ne h_le h_eq)]
rw [pow_succ' y, mul_assoc, mul_assoc, mul_assoc, mul_assoc]
induction n with
| zero =>
rw [pow_zero, sum_range_succ, range_zero, sum_empty, zero_add]
dsimp only [t]
rw [pow_zero, pow_zero, choose_self, cast_one, mul_one, mul_one]
| succ n
ih =>
rw [sum_range_succ', h_first, sum_congr rfl (h_middle n), sum_add_distrib, add_assoc, pow_succ' (x + y), ih,
add_mul, mul_sum, mul_sum]
congr 1
rw [sum_range_succ', sum_range_succ, h_first, h_last, mul_zero, add_zero, _root_.pow_succ']
