Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-28 08:03 8ee05e9a

View on Github →

feat(data/nat/log): Ceil log (#8764) Defines the upper natural log, which is the least k such that n ≤ b^k. Also expand greatly the docs of data.nat.multiplicity, in particular to underline that it proves Legendre's theorem.

Estimated changes

added def nat.clog
added theorem nat.clog_eq_one
added theorem nat.clog_le_clog_of_le
added theorem nat.clog_mono
added theorem nat.clog_of_two_le
added theorem nat.clog_one_left
added theorem nat.clog_one_right
added theorem nat.clog_pos
added theorem nat.clog_pow
added theorem nat.clog_zero_left
added theorem nat.clog_zero_right
added theorem nat.le_pow_clog
added theorem nat.le_pow_iff_clog_le
deleted theorem nat.log_b_one_eq_zero
deleted theorem nat.log_b_zero_eq_zero
deleted theorem nat.log_eq_zero_of_le
deleted theorem nat.log_eq_zero_of_lt
added theorem nat.log_le_clog
deleted theorem nat.log_le_log_succ
added theorem nat.log_of_left_le_one
added theorem nat.log_of_lt
deleted theorem nat.log_one_eq_zero
added theorem nat.log_one_left
added theorem nat.log_one_right
added theorem nat.log_pos
modified theorem nat.log_pow
deleted theorem nat.log_zero_eq_zero
added theorem nat.log_zero_left
added theorem nat.log_zero_right
modified theorem nat.pow_le_iff_le_log
modified theorem nat.pow_log_le_self
deleted theorem nat.pow_succ_log_gt_self