Theorem Real.hasSum_log_one_add

Modification history

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