Theorem CFC.log_le_log

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_le_logView on Github →