no goals
l : Type ?u.231349
m : Type u_1
n : Type u_2
o : Type ?u.231358
R : Type u_3
m_fin : Fintype m
inst✝² : Fintype n
inst✝¹ : Fintype o
inst✝ : CommRing R
A : Matrix m n R
⊢ rank A = finrank R { x // x ∈ Submodule.span R (Set.range Aᵀ) }
rw [rank, Matrix.range_mulVecLin]