English
There is a natural star-algebra equivalence between square matrices and continuous linear endomorphisms of Euclidean space via an orthonormal basis.
Русский
Существует естественное эквивалентное отображение звёздных алгебр между квадратными матрицами и непрерывными линейными концевыми отображениями евклидова пространства через ортонормированный базис.
LaTeX
$$$toEuclideanCLM: Matrix(n,n,\\\\mathbb{C}) \\\\simeq_{*\\\\mathbb{C}} (\\\\mathbb{C}^n \\\\to) $ (End_{\mathbb{C}}(EuclideanSpace))$$
Lean4
/-- 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`. -/
def toEuclideanCLM : Matrix n n 𝕜 ≃⋆ₐ[𝕜] (EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n) :=
toMatrixOrthonormal (EuclideanSpace.basisFun n 𝕜) |>.symm.trans <|
{ toContinuousLinearMap with
map_mul' := fun _ _ ↦ rfl
map_star' := adjoint_toContinuousLinearMap }
