English
There is a star-algebra equivalence between End(E) and the square matrices M_n(𝕜) induced by an orthonormal basis v₁, i.e., End(E) ≃⋆ₐ M_n(𝕜). The map is given by f ↦ [f]_{v₁}, and it preserves multiplication and the star operation.
Русский
Существует звёздо-алгебраическое эквивалентство между End(E) и квадратными матрицами M_n(𝕜), индуцируемое ортонормированным базисом v₁: End(E) ≃⋆ₐ M_n(𝕜). Отображение f ↦ [f]_{v₁} сохраняет умножение и операцию звезды.
LaTeX
$$$End_{𝕂}(E) \cong_{⋆} M_n(𝕂)$, задаваемое $f \mapsto [f]_{v_1}$$$
Lean4
/-- The matrix associated to the adjoint of a linear map corresponding to two orthonormal bases
is the conjugate transpose of the matrix associated to the linear map. -/
theorem toMatrix_adjoint (f : E →ₗ[𝕜] F) :
toMatrix v₂.toBasis v₁.toBasis (adjoint f) = (toMatrix v₁.toBasis v₂.toBasis f)ᴴ :=
toLin v₂.toBasis v₁.toBasis |>.injective <| by simp [toLin_conjTranspose]
