Theorem CFC.rpow_neg_one_eq_cfc_inv

Modification history

2024-10-30 16:54
Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow.lean
feat: positive contractions in a Cā‹†-algebra form a directed set (#18016)
Added CFC.rpow_neg_one_eq_cfc_invView on Github ā†’