α : Type u
inst✝ : DivisionRing α
x : α
h : x ≠ 1
n : ℕ
this : x - 1 ≠ 0
⊢ ∑ i in range n, x ^ i = (x ^ n - 1) / (x - 1)
α : Type u
inst✝ : DivisionRing α
x : α
h : x ≠ 1
n : ℕ
⊢ ∑ i in range n, x ^ i = (x ^ n - 1) / (x - 1)
have : x - 1 ≠ 0 := by simp_all [sub_eq_iff_eq_add]
no goals
α : Type u
inst✝ : DivisionRing α
x : α
h : x ≠ 1
n : ℕ
this : x - 1 ≠ 0
⊢ ∑ i in range n, x ^ i = (x ^ n - 1) / (x - 1)
rw [← geom_sum_mul, mul_div_cancel _ this]
no goals
α : Type u
inst✝ : DivisionRing α
x : α
h : x ≠ 1
n : ℕ
⊢ x - 1 ≠ 0
simp_all [sub_eq_iff_eq_add]