Theorem Real.log_of_nat_eq_posLog

Modification history

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.log_of_nat_eq_posLogView on Github →