ofMatrixₗ — Mathlib

English

There exists a canonical linear equivalence between the space of m-by-n matrices over A and the type CStarMatrix m n A; the equivalence is the identity on underlying matrices.

Русский

Существует каноническое линейное эквивалентное отображение между пространством матриц размерности m×n над A и множеством CStarMatrix m n A; эквивалентность задаётся как тождественное отображение на базовой матрице.

LaTeX

$$$(Matrix\_{m,n}(A)) \cong_R CStarMatrix_{m,n}(A)$$

Lean4

/-- The equivalence to matrices, bundled as a linear equivalence. -/
def ofMatrixₗ [AddCommMonoid A] [Semiring R] [Module R A] : (Matrix m n A) ≃ₗ[R] CStarMatrix m n A :=
  LinearEquiv.refl _ _

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