no goals
l : Type ?u.9554
m : Type u_2
n : Type u_3
o : Type ?u.9563
R : Type u_1
m_fin : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : CommRing R
inst✝ : Nontrivial R
⊢ rank 0 = 0
rw [rank, mulVecLin_zero, LinearMap.range_zero, finrank_bot]