English
If m and n are finite, the finrank of Matrix m n M is card m × card n × finrank M.
Русский
Если m и n конечны, то finrank Matrix m n M равно card m × card n × finrank M.
LaTeX
$$$\operatorname{finrank}_R(\mathrm{Matrix}_{m,n}(M)) = \operatorname{card}(m) \cdot \operatorname{card}(n) \cdot \operatorname{finrank}_R M$$$
Lean4
/-- If `m` and `n` are `Fintype`, the `finrank` of `m × n` matrices over a module `M` is
`(Fintype.card m) * (Fintype.card n) * finrank R M`. -/
theorem finrank_matrix (m n : Type*) [Fintype m] [Fintype n] :
finrank R (Matrix m n M) = card m * card n * finrank R M := by simp [finrank]