Theorem Unitization.starMap_injective

Modification history

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