instCStarAlgebra — Mathlib

English

Matrices with entries in a unital C*-algebra A form a unital CStarAlgebra (unital matrix algebra).

Русский

Матрицы над унитной C*-алгеброй образуют унитарную C*-алгебру.

LaTeX

$$$$\\text{CStarAlgebra}(\\mathrm{CStarMatrix}(n,n,A)).$$$$

Lean4

/-- Matrices with entries in a unital C⋆-algebra form a unital C⋆-algebra. -/
noncomputable instance instCStarAlgebra [DecidableEq n] : CStarAlgebra (CStarMatrix n n A) where

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