Theorem Real.natLog_le_logb

Modification history

2024-09-08 09:20
Mathlib/Analysis/SpecialFunctions/Log/Base.lean
feat: Nat.log is less than or equal to Real.logb (#16450) …
Added Real.natLog_le_logbView on Github →