Commit 2025-01-17 12:14 bad84cb5
View on Github →feat: elementary estimate for Real.log (#20766)
Generalize the theorem log_pos_iff', weakening the hypothesis hx : 0 < x to the (perhaps more natural) hypothesis hx : 0 ≤ x. Do the same for log_nonpos_iff and depreciate log_nonpos_iff'. Fix one trivial typo in a docstring of Mathlib/NumberTheory/Bertrand.lean.