Theorem CFC.rpow_eq_cfc_real

Modification history

2026-03-26 18:37
Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean
feat: add `IsSemitopologicalRing` (#36617) …
Modified CFC.rpow_eq_cfc_realView on Github →
2025-11-26 02:38
Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean
feat(CStarAlgebra): the log is operator monotone (#30894) …
Added CFC.rpow_eq_cfc_realView on Github →