instL2OpNormedRing — Mathlib

English

The operator norm induces a normed ring structure on matrices by the rule ∥xy∥ ≤ ∥x∥ ∥y∥.

Русский

Операторная норма задаёт нормированное кольцо на матрицах: ∥xy∥ ≤ ∥x∥ ∥y∥.

LaTeX

$$$\\forall X,Y: M_{m\\times m}(\\mathbb{C}), \\\\ \\|XY\\|_{2} \\leq \\|X\\|_{2} \\cdot \\|Y\\|_{2}$$$

Lean4

/-- The normed ring structure on `Matrix n n 𝕜` arising from the operator norm given by the
identification with (continuous) linear endmorphisms of `EuclideanSpace 𝕜 n`. -/
def instL2OpNormedRing : NormedRing (Matrix n n 𝕜)
    where
  dist_eq := l2OpNormedRingAux.dist_eq
  norm_mul_le := l2OpNormedRingAux.norm_mul_le

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