no goals
R : Type u
M : Type v
N : Type w
inst✝⁹ : Ring R
inst✝⁸ : StrongRankCondition R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module.Free R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : Module.Free R N
m n : Type v
inst✝¹ : Finite m
inst✝ : Finite n
⊢ Module.rank R (Matrix m n R) = Cardinal.lift ((#m) * (#n))
rw [rank_matrix, lift_mul, lift_umax.{v, u}]