l2_opNorm_def — Mathlib

English

The natural isomorphism between matrices and continuous linear maps preserves the linear structure and inner products.

Русский

Естественный изоморфизм между матрицами и непрерывными линейными отображениями сохраняет линейную структуру и скалярное произведение.

LaTeX

$$$toEuclideanLin: Matrix(n,n,\\\\mathbb{C}) \\\\cong ILinearMap(\\\\mathbb{C}^n, \\\\mathbb{C}^n)$$$

Lean4

theorem l2_opNorm_def (A : Matrix m n 𝕜) :
    ‖A‖ = ‖(toEuclideanLin (𝕜 := 𝕜) (m := m) (n := n)).trans toContinuousLinearMap A‖ :=
  rfl

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