instSubsingleton

Mathlib.Analysis.CStarAlgebra.CStarMatrix

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

English

If A is a Subsingleton, then CStarMatrix m n A is a Subsingleton.

Русский

Если A — подсинглтон, то CStarMatrix m n A тоже подсинглтон.

LaTeX

$$$[Subsingleton A] \Rightarrow Subsingleton (CStarMatrix m n A)$$$

Lean4

instance instSubsingleton [Subsingleton A] : Subsingleton (CStarMatrix m n A) :=
  inferInstanceAs <| Subsingleton <| m → n → A

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

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

Разделы

Аффилиация

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