Theorem NonUnitalStarAlgHom.nnnorm_map

Modification history

2024-09-11 00:28
Mathlib/Analysis/CStarAlgebra/Hom.lean
feat: star monomorphisms between Cā‹†-algebras are isometric (#16599)
Added NonUnitalStarAlgHom.nnnorm_mapView on Github ā†’