Theorem Unitization.starMap_comp

Modification history

2024-09-11 00:28
Mathlib/Algebra/Algebra/Unitization.lean
feat: star monomorphisms between Cā‹†-algebras are isometric (#16599)
Added Unitization.starMap_compView on Github ā†’