finrank_matrix — Mathlib

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]

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