Theorem CFC.inverse_eq_rpow_neg_one

Modification history

2026-03-19 01:06
Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean
feat(CStarAlgebra): lemmas related to `CFC.rpow` and `IsStrictlyPositive` (#36784) …
Added CFC.inverse_eq_rpow_neg_oneView on Github →