Theorem CFC.tendsto_cfc_rpow_sub_one_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.tendsto_cfc_rpow_sub_one_logView on Github →