Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-25 10:28 ba1c3f36

View on Github →

feat(data/int/log): integer logarithms of linearly ordered fields (#13913) Notably, this provides a way to find the position of the most significant digit of a decimal expansion

Estimated changes

added theorem int.ceil_one
added theorem nat.ceil_one
added theorem nat.floor_lt_one
added def int.clog
added theorem int.clog_inv
added theorem int.clog_mono_right
added theorem int.clog_nat_cast
added theorem int.clog_one_right
added theorem int.clog_zero_right
added theorem int.clog_zpow
added def int.clog_zpow_gi
added def int.log
added theorem int.log_inv
added theorem int.log_mono_right
added theorem int.log_nat_cast
added theorem int.log_of_left_le_one
added theorem int.log_one_right
added theorem int.log_zero_right
added theorem int.log_zpow
added theorem int.lt_zpow_iff_log_lt
added theorem int.self_le_zpow_clog
added theorem int.zpow_le_iff_le_log
added def int.zpow_log_gi
added theorem int.zpow_log_le_self