Theorem Unitization.inr_inj

Modification history

2026-03-10 23:22
Mathlib/Algebra/Algebra/Unitization.lean
feat(Analysis/CStarAlgebra/CFC/Order): conjugating with a star projection in a C*-algebra (#35997) …
Added Unitization.inr_injView on Github →