Theorem Real.lt_log_one_add_of_pos

Modification history

2025-02-17 23:56
Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean
feat(Analysis): lower bound for `log (1 + x)` (#21671)
Added Real.lt_log_one_add_of_posView on Github →