Theorems · Definition · functional analysis

CStarMatrix.toCLMNonUnitalAlgHom

{n : Type u_2} →
  {A : Type u_5} →
    [inst : NonUnitalCStarAlgebra A] →
      [inst_1 : Fintype n] → CStarMatrix n n A →ₙₐ[ℂ] (WithCStarModule A (n → A) →L[ℂ] WithCStarModule A (n → A))ᵐᵒᵖ

Interpret a CStarMatrix m n A as a continuous linear map acting on C⋆ᵐᵒᵈ (n → A). This version is specialized to the case m = n and is bundled as a non-unital algebra homomorphism.

Defined in

Mathlib.Analysis.CStarAlgebra.CStarMatrix

Cited by

2 results in Mathlib

Foundations

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

Assumes

NonUnitalCStarAlgebraFintype