Theorem Unitization.starMap_surjective

Modification history

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