Commit 2022-12-19 15:36 331a5bb1

View on Github →

feat: port Data.Nat.Log (#1089) 11bb0c9152e5d14278fb0ac5e0be6d50e2c8fa05 Warning: attributes mono and pp_nodot are unknown and were commented out (with porting notes).

Estimated changes

added theorem Nat.add_pred_div_lt
added def Nat.clog
added theorem Nat.clog_anti_left
added theorem Nat.clog_antitone_left
added theorem Nat.clog_eq_one
added theorem Nat.clog_mono_right
added theorem Nat.clog_monotone
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_log_of_pow_le
added theorem Nat.le_pow_clog
added theorem Nat.le_pow_iff_clog_le
added def Nat.log
added theorem Nat.log_anti_left
added theorem Nat.log_antitone_left
added theorem Nat.log_div_base
added theorem Nat.log_div_mul_self
added theorem Nat.log_eq_iff
added theorem Nat.log_eq_one_iff'
added theorem Nat.log_eq_one_iff
added theorem Nat.log_eq_zero_iff
added theorem Nat.log_le_clog
added theorem Nat.log_lt_of_lt_pow
added theorem Nat.log_mono_right
added theorem Nat.log_monotone
added theorem Nat.log_mul_base
added theorem Nat.log_of_left_le_one
added theorem Nat.log_of_lt
added theorem Nat.log_one_left
added theorem Nat.log_one_right
added theorem Nat.log_pos
added theorem Nat.log_pos_iff
added theorem Nat.log_pow
added theorem Nat.log_zero_left
added theorem Nat.log_zero_right
added theorem Nat.lt_pow_iff_log_lt
added theorem Nat.lt_pow_of_log_lt
added theorem Nat.pow_le_iff_le_log
added theorem Nat.pow_le_of_le_log
added theorem Nat.pow_log_le_add_one
added theorem Nat.pow_log_le_self
added theorem Nat.pow_lt_iff_lt_clog