toMatrixOrthonormal — Mathlib

English

The star-algebra equivalence preserves multiplication: the matrix of the product of two linear maps equals the product of their matrices.

Русский

Звёздное алгебраическое эквивалентство сохраняет умножение: матрица произведения линейных отображений равна произведению их матриц.

LaTeX

$$$[f g]_{v} = [f]_{v} [g]_{v}$$$

Lean4

/-- The star algebra equivalence between the linear endomorphisms of finite-dimensional inner
product space and square matrices induced by the choice of an orthonormal basis. -/
@[simps]
def toMatrixOrthonormal : (E →ₗ[𝕜] E) ≃⋆ₐ[𝕜] Matrix n n 𝕜 :=
  {
    LinearMap.toMatrix v₁.toBasis
      v₁.toBasis with
    map_mul' := LinearMap.toMatrix_mul v₁.toBasis
    map_star' := LinearMap.toMatrix_adjoint v₁ v₁ }

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