α : Type u
inst✝ : Ring α
x : α
n : ℕ
this : (∑ i in range n, x ^ i * 1 ^ (n - 1 - i)) * (x - 1) = x ^ n - 1 ^ n
⊢ (∑ i in range n, x ^ i) * (x - 1) = x ^ n - 1
α : Type u
inst✝ : Ring α
x : α
n : ℕ
⊢ (∑ i in range n, x ^ i) * (x - 1) = x ^ n - 1
have := (Commute.one_right x).geom_sum₂_mul n
α : Type u
inst✝ : Ring α
x : α
n : ℕ
this : (∑ i in range n, x ^ i) * (x - 1) = x ^ n - 1
⊢ (∑ i in range n, x ^ i) * (x - 1) = x ^ n - 1
α : Type u
inst✝ : Ring α
x : α
n : ℕ
this : (∑ i in range n, x ^ i * 1 ^ (n - 1 - i)) * (x - 1) = x ^ n - 1 ^ n
⊢ (∑ i in range n, x ^ i) * (x - 1) = x ^ n - 1
rw [one_pow, geom_sum₂_with_one] at this
no goals
α : Type u
inst✝ : Ring α
x : α
n : ℕ
this : (∑ i in range n, x ^ i) * (x - 1) = x ^ n - 1
⊢ (∑ i in range n, x ^ i) * (x - 1) = x ^ n - 1
exact this