cstar_norm_def — Mathlib

English

For square matrices, the L2-norm coincides with the bundled Euclidean CLM norm: ||A|| = ||toEuclideanCLM(A)||.

Русский

Для квадратных матриц норма L2 совпадает с приводимой к евклидовой CLM нормой: ||A|| = ||toEuclideanCLM(A)||.

LaTeX

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

Lean4

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

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