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