Theorem cfc_ringInverse_id

Modification history

2026-04-25 22:48
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
feat(CStarAlgebra): `x ↦ x ^ p` is operator concave for `p ∈ [0, 1]` (#37643) …
Modified cfc_ringInverse_idView on Github →
2026-03-24 16:45
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
feat: notation for `Ring.inverse` (#34396) …
Added cfc_ringInverse_idView on Github →