instNorm — Mathlib

English

The operator norm on the matrix algebra is induced by the operator norm on the associated continuous linear maps: ‖M‖ = ‖toCLM M‖.

Русский

Операторная норма на алгебре матриц задаётся через норму соответствующих непрерывно линейных отображений: ‖M‖ = ‖toCLM M‖.

LaTeX

$$Norm (CStarMatrix m n A) defined by ‖M‖ := ‖toCLM M‖.$$

Lean4

/-- The operator norm on `CStarMatrix m n A`. -/
noncomputable instance instNorm : Norm (CStarMatrix m n A) where norm M := ‖toCLM M‖

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