ofMatrixL — Mathlib

English

ofMatrixL is a continuous linear equivalence between Matrix m n A and CStarMatrix m n A.

Русский

ofMatrixL является непрерывной линейной эквивалентностью между Matrix m n A и CStarMatrix m n A.

LaTeX

$$$$\\mathrm{ofMatrixL} : \\mathrm{Matrix}(m,n,A) \\simeq_L[\\mathbb{C}] \\mathrm{CStarMatrix}(m,n,A).$$$$

Lean4

/-- `ofMatrix` bundled as a continuous linear equivalence. -/
def ofMatrixL : Matrix m n A ≃L[ℂ] CStarMatrix m n A :=
  { ofMatrixₗ with
    continuous_toFun := continuous_id
    continuous_invFun := continuous_id }

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