Theorem Real.abs_log_eq_posLog_add_posLog_inv

Modification history

2026-08-13 17:23
Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean
feat: trivial estimates for the positive part of the logarithm (#42000) …
Added Real.abs_log_eq_posLog_add_posLog_invView on Github →