Theorem Real.le_log_one_add_of_nonneg

Modification history

2026-06-13 17:40
Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
feat(Analysis/Complex/Exponential): add new bounds on exponential (#39690) …
Modified Real.le_log_one_add_of_nonnegView on Github →
2025-02-17 23:56
Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean
feat(Analysis): lower bound for `log (1 + x)` (#21671)
Added Real.le_log_one_add_of_nonnegView on Github →