Theorem Unitization.inr_inj

Modification history

2026-03-25 16:54

Mathlib/Algebra/Algebra/Unitization.lean

refactor: make `Unitization` into a one-field structure (#37014) …

Modified Unitization.inr_inj View on Github →

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_inj View on Github →