instL2OpNormedAlgebra — Mathlib

English

The operator-norm on matrices gives a NormedAlgebra structure over the complex field.

Русский

Операторная норма на матрицах образует нормированную алгебру над комплексными числами.

LaTeX

$$$\\text{instL2OpNormedAlgebra}: \\text{NormedAlgebra}_{\\mathbb{C}}(M_{n\\times n}(\\mathbb{C}))$$$

Lean4

/-- The normed algebra structure on `Matrix n n 𝕜` arising from the operator norm given by the
identification with (continuous) linear endmorphisms of `EuclideanSpace 𝕜 n`. -/
def instL2OpNormedAlgebra : NormedAlgebra 𝕜 (Matrix n n 𝕜) where norm_smul_le := norm_smul_le

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