Theorems · Definition · functional analysis

CStarMatrix.toCLM

{m : Type u_1} →
  {n : Type u_2} →
    {A : Type u_5} →
      [Fintype m] →
        [inst : NonUnitalCStarAlgebra A] →
          CStarMatrix m n A →ₗ[ℂ] WithCStarModule A (m → A) →L[ℂ] WithCStarModule A (n → A)

Interpret a CStarMatrix m n A as a continuous linear map acting on C⋆ᵐᵒᵈ (n → A).

Defined in

Mathlib.Analysis.CStarAlgebra.CStarMatrix

Cited by

13 results in Mathlib

Foundations

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

Assumes

FintypeNonUnitalCStarAlgebra