Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-08 19:06 449ba97d

View on Github →

refactor(data/nat/log): Golf + improved theorem names (#14019) Other than golfing and moving a few things around, our main changes are:

  • rename log_le_log_of_le to log_mono_right, analogous renames elsewhere.
  • add lt_pow_iff_log_lt and a clog analog.

Estimated changes

added theorem nat.clog_anti_left
deleted theorem nat.clog_le_clog_of_le
added theorem nat.clog_mono_right
modified theorem nat.le_pow_iff_clog_le
added theorem nat.log_anti_left
deleted theorem nat.log_eq_zero
deleted theorem nat.log_le_log_of_le
deleted theorem nat.log_le_log_of_left_ge
added theorem nat.log_mono_right
modified theorem nat.log_monotone
modified theorem nat.log_of_left_le_one
modified theorem nat.log_of_lt
modified theorem nat.log_one_left
modified theorem nat.log_zero_left
added theorem nat.lt_pow_iff_log_lt
modified theorem nat.pow_le_iff_le_log
added theorem nat.pow_lt_iff_lt_clog