Commit 2025-10-06 22:42 cd0687a5

View on Github →

chore(Nat/Log): swap Nat.pow_le_iff_le_log lemmas (#30229) Swap the order of the following four lemmas:

  • Nat.pow_le_iff_le_log
  • Nat.lt_pow_iff_log_lt
  • Nat.le_pow_iff_clog_le
  • Nat.pow_lt_iff_lt_clog This is to match the pattern used everywhere else in mathlib, eg for Real.log, and the pattern used in core, eg for Nat.log2.

Estimated changes

added theorem Nat.clog_le_iff_le_pow
added theorem Nat.le_log_iff_pow_le
modified theorem Nat.le_pow_iff_clog_le
added theorem Nat.log_lt_iff_lt_pow
added theorem Nat.lt_clog_iff_pow_lt