instStarRing

Mathlib.Analysis.CStarAlgebra.CStarMatrix

URI: https://scilib.ai/kg/mathlib#CStarMatrix.instStarRing

English

If A is a star ring, then CStarMatrix n n A is a star ring as well.

Русский

Если A — звёздочная кольцо, то CStarMatrix n n A тоже является звездочным кольцом.

LaTeX

$$StarRing(CStarMatrix_{n,n} A)$$

Lean4

instance instStarRing [Fintype n] [NonUnitalSemiring A] [StarRing A] : StarRing (CStarMatrix n n A) :=
  inferInstanceAs <| StarRing (Matrix n n A)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru