Theorems · Definition · functional analysis

Matrix.toEuclideanCLM

{𝕜 : Type u_1} →
  {n : Type u_3} →
    [inst : RCLike 𝕜] →
      [inst_1 : Fintype n] → [DecidableEq n] → Matrix n n 𝕜 ≃⋆ₐ[𝕜] EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n

The natural star algebra equivalence between matrices and continuous linear endomorphisms of Euclidean space induced by the orthonormal basis EuclideanSpace.basisFun. This is a more-bundled version of Matrix.toEuclideanLin, for the special case of square matrices, followed by a more-bundled version of LinearMap.toContinuousLinearMap.

Defined in

Mathlib.Analysis.CStarAlgebra.Matrix

Cited by

12 results in Mathlib

Foundations

Depth 233 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RCLikeFintypeDecidableEq