instPartialOrder

Mathlib.Analysis.CStarAlgebra.CStarMatrix

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

English

Partial order for CStarMatrix(n,n,A) via spectral order (duplicate).

Русский

Частичный порядок для CStarMatrix через спектральный порядок (повтор).

LaTeX

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

Lean4

noncomputable instance instPartialOrder : PartialOrder (CStarMatrix n n A) :=
  CStarAlgebra.spectralOrder _

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

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

Разделы

Аффилиация

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