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.

@[instance_reducible]

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

Equations

• One or more equations did not get rendered due to their size.