Theorem Real.posLog_sub_posLog_inv

Modification history

2025-10-31 17:31
Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean
chore(Analysis/SpecialFunctions/Log/PosLog): uniformize variable names (#31084) …
Modified Real.posLog_sub_posLog_invView on Github →
2025-01-31 20:04
Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean
feat: add function log⁺ (=positive part of the logarithm) and prove standard estimates (#21289) …
Added Real.posLog_sub_posLog_invView on Github →