Commit 2025-12-03 03:21 66ba1e1a
View on Github →chore: split operator monotonicity results to privately import integration results (#32329)
This PR splits the file Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation to split off operator monotonicity results into their own file (called Order). This allows us to privately
import the results about CFC integration since they are rather heavy and only used as a proof technique.