instCStarRing — Mathlib

English

The L2-operator norm yields a submultiplicative norm on square matrices: ∥AB∥ ≤ ∥A∥ ∥B∥.

Русский

Норма оператора L2 на квадратных матрицах субумножаема: ∥AB∥ ≤ ∥A∥ ∥B∥.

LaTeX

$$$\\forall A,B: M_{n\\times n}(\\mathbb{C}), \\\\ \\|AB\\|_{2} \\leq \\|A\\|_{2} \\cdot \\|B\\|_{2}$$$

Lean4

/-- The operator norm on `Matrix n n 𝕜` given by the identification with (continuous) linear
endmorphisms of `EuclideanSpace 𝕜 n` makes it into a `L2OpRing`. -/
theorem instCStarRing : CStarRing (Matrix n n 𝕜) where
  norm_mul_self_le M := le_of_eq <| Eq.symm <| l2_opNorm_conjTranspose_mul_self M

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