Theorem Int.log_one_left

Modification history

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