ofMatrixStarAlgEquiv — Mathlib

English

There exists a canonical star-algebra equivalence between Matrix n by n over A and CStarMatrix n by n with entries in A, provided by the ofMatrix construction.

Русский

Существует каноническое эквивалентное отношение звёздной алгебры между матрицами размерности n×n над A и CStarMatrix n×n над A, задаваемое конструкцией ofMatrix.

LaTeX

$$$\text{Matrix}_{n\times n}(A) \;\cong_{\ast}^{\mathbb{C}}\; C^*\text{-Matrix}_{n\times n}(A).$$$

Lean4

/-- `ofMatrix` bundled as a star algebra equivalence. -/
def ofMatrixStarAlgEquiv [Fintype n] [SMul ℂ A] [Semiring A] [StarRing A] : Matrix n n A ≃⋆ₐ[ℂ] CStarMatrix n n A :=
  { ofMatrixRingEquiv with
    map_star' := fun _ => rfl
    map_smul' := fun _ _ => rfl }

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