English
If m and n are finite and lie in the same universe as R, the rank of Matrix m n R is #m * #n lifted.
Русский
Если m и n конечны и лежат в той же вселенной, что и R, ранг Matrix m n R равен #m · #n, затем поднимается (lift).
LaTeX
$$$\operatorname{rank}_R(\mathrm{Matrix}_{m,n} R) = \#m \cdot \#n\,\uparrow$$$
Lean4
/-- If `m` and `n` are finite, the rank of `m × n` matrices is `(#m).lift * (#n).lift`. -/
theorem rank_matrix (m : Type v) (n : Type w) [Finite m] [Finite n] :
Module.rank R (Matrix m n R) = Cardinal.lift.{max v w u, v} #m * Cardinal.lift.{max v w u, w} #n := by
rw [rank_matrix_module, rank_self, lift_one, mul_one, ← lift_lift.{v, max u w}, lift_id, ← lift_lift.{w, max u v},
lift_id]
