l : Type u_2
m : Type u_3
n : Type u_4
o : Type ?u.37975
R : Type u_1
m_fin : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : CommRing R
inst✝ : StrongRankCondition R
A : Matrix l m R
B : Matrix m n R
⊢ finrank R { x // x ∈ LinearMap.range (LinearMap.comp (mulVecLin A) (mulVecLin B)) } ≤
    finrank R { x // x ∈ LinearMap.range (mulVecLin B) }
l : Type u_2
m : Type u_3
n : Type u_4
o : Type ?u.37975
R : Type u_1
m_fin : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : CommRing R
inst✝ : StrongRankCondition R
A : Matrix l m R
B : Matrix m n R
⊢ rank (A ⬝ B) ≤ rank B
rw [rank, rank, mulVecLin_mul]
no goals
l : Type u_2
m : Type u_3
n : Type u_4
o : Type ?u.37975
R : Type u_1
m_fin : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : CommRing R
inst✝ : StrongRankCondition R
A : Matrix l m R
B : Matrix m n R
⊢ finrank R { x // x ∈ LinearMap.range (LinearMap.comp (mulVecLin A) (mulVecLin B)) } ≤
    finrank R { x // x ∈ LinearMap.range (mulVecLin B) }
exact
  finrank_le_finrank_of_rank_le_rank (LinearMap.lift_rank_comp_le_right _ _) (rank_lt_aleph0 _ _)