case intro
l : Type ?u.285266
m : Type u_2
n : Type u_3
o : Type ?u.285275
R : Type u_1
m_fin : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : LinearOrderedField R
inst✝ : Finite m
A : Matrix m n R
val✝ : Fintype m
⊢ rank A = finrank R { x // x ∈ Submodule.span R (Set.range A) }
l : Type ?u.285266
m : Type u_2
n : Type u_3
o : Type ?u.285275
R : Type u_1
m_fin : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : LinearOrderedField R
inst✝ : Finite m
A : Matrix m n R
⊢ rank A = finrank R { x // x ∈ Submodule.span R (Set.range A) }
cases nonempty_fintype m
no goals
case intro
l : Type ?u.285266
m : Type u_2
n : Type u_3
o : Type ?u.285275
R : Type u_1
m_fin : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : LinearOrderedField R
inst✝ : Finite m
A : Matrix m n R
val✝ : Fintype m
⊢ rank A = finrank R { x // x ∈ Submodule.span R (Set.range A) }
rw [← rank_transpose, rank_eq_finrank_span_cols, transpose_transpose]