Theorem CFC.rpow_le_rpow

Modification history

2025-12-03 03:21
Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/IntegralRepresentation.lean
chore: split operator monotonicity results to privately import integration results (#32329) …
Modified CFC.rpow_le_rpowView on Github →
2025-08-21 02:05
Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/IntegralRepresentation.lean
feat(CStarAlgebra): `a => a ^ p` is operator monotone for `p ∈ Icc 0 1` (#27715) …
Added CFC.rpow_le_rpowView on Github →