Theorem Real.logb_one_left

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