Theorem CFC.log_monotoneOn

Modification history

2025-11-26 02:38
Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog/Order.lean
feat(CStarAlgebra): the log is operator monotone (#30894) …
Added CFC.log_monotoneOnView on Github →