Theorem Unitization.starMap_inl

Modification history

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