Theorem Int.clog_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.clog_one_leftView on Github →