rank_matrix' — Mathlib

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}]

Похожие утверждения