Theorem NonUnitalStarAlgHom.norm_map

Modification history

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