Theorem Real.norm_inv_mul_rpow_sub_one_sub_log_le

Modification history

2025-11-26 02:38
Mathlib/Analysis/SpecialFunctions/Log/RpowTendsto.lean
feat(CStarAlgebra): the log is operator monotone (#30894) …
Added Real.norm_inv_mul_rpow_sub_one_sub_log_leView on Github →