finiteDimensional — Mathlib

English

Let R be a field and m, n finite types. The space of m-by-n matrices with entries in R is a finite-dimensional vector space over R.

Русский

Пусть R — поле и m, n конечные множества. Пространство матриц размером m × n над R является конечномерным векторным пространством над R.

LaTeX

$$$\operatorname{Mat}_{m\times n}(R) \cong_R R^{m\cdot n}$, hence $\dim_R(\operatorname{Mat}_{m\times n}(R)) = |m|\cdot |n|$.$$

Lean4

instance finiteDimensional [Finite m] [Finite n] : FiniteDimensional R (Matrix m n R) :=
  Module.Finite.matrix

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