Theorem NonUnitalStarAlgHom.instContinuousLinearMapClassComplex

Modification history

2024-08-08 16:24
Mathlib/Analysis/CStarAlgebra/Spectrum.lean
feat: star algebra homomorphisms between non-unital C⋆-algebras are contractive (#14544) …
Added NonUnitalStarAlgHom.instContinuousLinearMapClassComplexView on Github →