Theorem Real.posLog_one

Modification history

2025-10-29 09:13
Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean
feat: elementary lemmas aiding computations with `log⁺`, Mark II (#30729) …
Added Real.posLog_oneView on Github →