E →L[ℂ] E as a C⋆-algebra

We place this here because, for reasons related to the import hierarchy, it should not be placed in earlier files.

noncomputable instance instCStarAlgebraContinuousLinearMapComplexIdOfCompleteSpace {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] : CStarAlgebra (E →L[ℂ] E)

Equations

• instCStarAlgebraContinuousLinearMapComplexIdOfCompleteSpace = CStarAlgebra.mk