Theorem CFC.nnrpow_eq_cfcₙ_real

Modification history

2026-03-26 18:37

Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean

feat: add `IsSemitopologicalRing` (#36617) …

Modified CFC.nnrpow_eq_cfcₙ_real View on Github →

2025-08-21 02:05

Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean

feat(CStarAlgebra): `a => a ^ p` is operator monotone for `p ∈ Icc 0 1` (#27715) …

Added CFC.nnrpow_eq_cfcₙ_real View on Github →