no goals
l : Type ?u.4278
m : Type ?u.4281
n : Type u_2
o : Type ?u.4287
R : Type u_1
m_fin : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Fintype o
inst✝² : CommRing R
inst✝¹ : StrongRankCondition R
inst✝ : DecidableEq n
⊢ rank 1 = Fintype.card n
rw [rank, mulVecLin_one, LinearMap.range_id, finrank_top, finrank_pi]