Theorem Real.posLog_le_posLog

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_le_posLogView on Github →
2025-10-20 08:46
Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean
chore(Analysis/SpecialFunctions/Log/PosLog): golf a proof using `grw` (#30704)
Added Real.posLog_le_posLogView on Github →