cstar_nnnorm_def — Mathlib

English

For square matrices, the NN-norm equals the bundled NNNorm on Euclidean CLM: ||A||₊ = ||toEuclideanCLM(A)||₊.

Русский

Для квадратных матриц NN-норма равна соответствующей NNNorm после привязки к EuclideanCLM.

LaTeX

$$$\\forall A: M_{n\\times n}(\\mathbb{C}), \\\\ \\|A\\|_{NN} = \\|toEuclideanCLM(A)\\|_{NN}$$$

Lean4

/-- This is the same as `Matrix.l2_opNNNorm_def`, but with a more bundled RHS for square
matrices. -/
theorem cstar_nnnorm_def (A : Matrix n n 𝕜) : ‖A‖₊ = ‖toEuclideanCLM (n := n) (𝕜 := 𝕜) A‖₊ :=
  rfl

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