Theorem Real.posLog_eq_log_max_one

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_eq_log_max_oneView on Github →
2025-10-11 10:18
Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean
feat(Analysis/SpecialFunctions/Log): one trivial fact about posLog (#30369) …
Added Real.posLog_eq_log_max_oneView on Github →