Theorem: MatrixCookbook.eq_487 (MatrixCookbook/10FunctionsAndOperators.lean)

State before:
ι : Type ?u.263
R : Type u_2
l : Type ?u.269
m : Type u_1
n✝ : Type ?u.275
p : Type ?u.278
q : Type ?u.281
r : Type ?u.284
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n✝
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n✝
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
X : Matrix m m R
n : ℕ
hx : (X - 1).det ≠ 0
⊢ (X ^ n - 1) * (X - 1)⁻¹ = ∑ i ∈ Finset.range n, X ^ i
Tactic:
rw [← geom_sum_mul X n, mul_nonsing_inv_cancel_right _ _ hx.isUnit]
State after:
no goals