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