Theorem Real.posLog_nat_mul

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_nat_mulView on Github →
2025-10-29 09:13
Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean
feat: elementary lemmas aiding computations with `log⁺`, Mark II (#30729) …
Modified Real.posLog_nat_mulView 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_nat_mulView on Github →