α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
n : ℕ
this : (∑ i in range n, (x - y + y) ^ i * y ^ (n - 1 - i)) * (x - y) + y ^ n = (x - y + y) ^ n
⊢ (∑ i in range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
n : ℕ
⊢ (∑ i in range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n
have := (h.sub_left (Commute.refl y)).geom_sum₂_mul_add n
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
n : ℕ
this : (∑ i in range n, x ^ i * y ^ (n - 1 - i)) * (x - y) + y ^ n = x ^ n
⊢ (∑ i in range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
n : ℕ
this : (∑ i in range n, (x - y + y) ^ i * y ^ (n - 1 - i)) * (x - y) + y ^ n = (x - y + y) ^ n
⊢ (∑ i in range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n
rw [sub_add_cancel] at this
no goals
α : Type u
inst✝ : Ring α
x y : α
h : Commute x y
n : ℕ
this : (∑ i in range n, x ^ i * y ^ (n - 1 - i)) * (x - y) + y ^ n = x ^ n
⊢ (∑ i in range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n
rw [← this, add_sub_cancel]