α : Type u
inst✝ : DivisionRing α
x y : α
h : Commute x y
hxy : x ≠ y
m n : ℕ
hmn : m ≤ n
this : x - y ≠ 0
⊢ ∑ i in Ico m n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ (n - m) * x ^ m) / (x - y)
α : Type u
inst✝ : DivisionRing α
x y : α
h : Commute x y
hxy : x ≠ y
m n : ℕ
hmn : m ≤ n
⊢ ∑ i in Ico m n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ (n - m) * x ^ m) / (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
hxy : x ≠ y
m n : ℕ
hmn : m ≤ n
this : x - y ≠ 0
⊢ ∑ i in Ico m n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ (n - m) * x ^ m) / (x - y)
rw [← h.geom_sum₂_Ico_mul hmn, mul_div_cancel _ this]
no goals
α : Type u
inst✝ : DivisionRing α
x y : α
h : Commute x y
hxy : x ≠ y
m n : ℕ
hmn : m ≤ n
⊢ x - y ≠ 0
simp_all [sub_eq_iff_eq_add]