l : Type ?u.51935
m : Type ?u.51938
n : Type u_2
o : Type ?u.51944
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)ˣ
⊢ Fintype.card n ≤ rank ↑A
l : Type ?u.51935
m : Type ?u.51938
n : Type u_2
o : Type ?u.51944
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
refine' le_antisymm (rank_le_card_width A) _
l : Type ?u.51935
m : Type ?u.51938
n : Type u_2
o : Type ?u.51944
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)ˣ
this : rank (↑A ⬝ ↑A⁻¹) ≤ rank ↑A
⊢ Fintype.card n ≤ rank ↑A
l : Type ?u.51935
m : Type ?u.51938
n : Type u_2
o : Type ?u.51944
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)ˣ
⊢ Fintype.card n ≤ rank ↑A
have := rank_mul_le_left (A : Matrix n n R) (↑A⁻¹ : Matrix n n R)
no goals
l : Type ?u.51935
m : Type ?u.51938
n : Type u_2
o : Type ?u.51944
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)ˣ
this : rank (↑A ⬝ ↑A⁻¹) ≤ rank ↑A
⊢ Fintype.card n ≤ rank ↑A
rwa [← mul_eq_mul, ← Units.val_mul, mul_inv_self, Units.val_one, rank_one] at this