English
For any x and n, the relation (sum i=0..n-1 (x+1)^i) · x + 1 = (x+1)^n holds in any semiring where x and 1 commute.
Русский
Для любого x и n выполняется (∑_{i=0}^{n-1} (x+1)^i)·x + 1 = (x+1)^n в любой полугруппе с единицей.
LaTeX
$$$\\left(\\sum_{i=0}^{n-1} (x+1)^{i}\\right) \\cdot x + 1 = (x+1)^{n}$$$
Lean4
/-- $x^n-y^n = (x-y) \sum x^ky^{n-1-k}$ reformulated without `-` signs. -/
protected theorem geom_sum₂_mul_add {x y : R} (h : Commute x y) (n : ℕ) :
(∑ i ∈ range n, (x + y) ^ i * y ^ (n - 1 - i)) * x + y ^ n = (x + y) ^ n :=
by
let f : ℕ → ℕ → R := fun m i : ℕ => (x + y) ^ i * y ^ (m - 1 - i)
change (∑ i ∈ range n, (f n) i) * x + y ^ n = (x + y) ^ n
induction n with
| zero => rw [range_zero, sum_empty, zero_mul, zero_add, pow_zero, pow_zero]
| succ n
ih =>
have f_last : f (n + 1) n = (x + y) ^ n := by
dsimp only [f]
rw [← tsub_add_eq_tsub_tsub, Nat.add_comm, tsub_self, pow_zero, mul_one]
have f_succ : ∀ i, i ∈ range n → f (n + 1) i = y * f n i := fun i hi =>
by
dsimp only [f]
have : Commute y ((x + y) ^ i) := (h.symm.add_right (Commute.refl y)).pow_right i
rw [← mul_assoc, this.eq, mul_assoc, ← pow_succ' y (n - 1 - i), add_tsub_cancel_right, ← tsub_add_eq_tsub_tsub,
add_comm 1 i]
have : i + 1 + (n - (i + 1)) = n := add_tsub_cancel_of_le (mem_range.mp hi)
rw [add_comm (i + 1)] at this
rw [← this, add_tsub_cancel_right, add_comm i 1, ← add_assoc, add_tsub_cancel_right]
rw [pow_succ' (x + y), add_mul, sum_range_succ_comm, add_mul, f_last, add_assoc,
(((Commute.refl x).add_right h).pow_right n).eq, sum_congr rfl f_succ, ← mul_sum, pow_succ' y, mul_assoc, ←
mul_add y, ih]
