Theorem Unitization.starMap_id

Modification history

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