instNormedSpace

Mathlib.Analysis.CStarAlgebra.CStarMatrix

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

English

CStarMatrix(m,n,A) carries a NormedSpace structure over the complex numbers ℂ.

Русский

CStarMatrix(m,n,A) образует нормированное пространство над полем комплексных чисел.

LaTeX

$$$$\\text{NormedSpace}_{\\mathbb{C}}(\\mathrm{CStarMatrix}(m,n,A)).$$$$

Lean4

noncomputable instance instNormedSpace : NormedSpace ℂ (CStarMatrix m n A) :=
  .ofCore CStarMatrix.normedSpaceCore

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

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

Разделы

Аффилиация

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