case intro
l : Type ?u.158331
m : Type ?u.158334
n : Type u_2
o : Type ?u.158340
R : Type u_1
m_fin : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Fintype o
inst✝² : CommRing R
inst✝¹ : StrongRankCondition R
inst✝ : DecidableEq n
A : (Matrix n n R)ˣ
⊢ rank ↑A = Fintype.card n
l : Type ?u.158331
m : Type ?u.158334
n : Type u_2
o : Type ?u.158340
R : Type u_1
m_fin : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Fintype o
inst✝² : CommRing R
inst✝¹ : StrongRankCondition R
inst✝ : DecidableEq n
A : Matrix n n R
h : IsUnit A
⊢ rank A = Fintype.card n
obtain ⟨A, rfl⟩ := h
no goals
case intro
l : Type ?u.158331
m : Type ?u.158334
n : Type u_2
o : Type ?u.158340
R : Type u_1
m_fin : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Fintype o
inst✝² : CommRing R
inst✝¹ : StrongRankCondition R
inst✝ : DecidableEq n
A : (Matrix n n R)ˣ
⊢ rank ↑A = Fintype.card n
exact rank_unit A