Theorem Unitization.sqrt_inr

Modification history

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