English
If m and n are finite, rank(Matrix m n R) equals #m * #n lifted.
Русский
Если m и n конечны, ранг Matrix m n R равен lift (#m * #n).
LaTeX
$$$\operatorname{rank}_R(\mathrm{Matrix}_{m,n} R) = \operatorname{lift}(\#m \cdot \#n)$$$
Lean4
/-- If `m` and `n` are finite and lie in the same universe, the rank of `m × n` matrices is
`(#n * #m).lift`. -/
theorem rank_matrix' (m n : Type v) [Finite m] [Finite n] :
Module.rank R (Matrix m n R) = Cardinal.lift.{u} (#m * #n) := by rw [rank_matrix, lift_mul, lift_umax.{v, u}]