Commit 2023-01-26 07:35 fcb13d16

View on Github →

feat: port Data.Int.Log (#1793)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Int/Log.lean

added def Int.clog

added def Int.clogZpowGi

added theorem Int.clog_inv

added theorem Int.clog_mono_right

added theorem Int.clog_natCast

added theorem Int.clog_of_left_le_one

added theorem Int.clog_of_one_le_right

added theorem Int.clog_of_right_le_one

added theorem Int.clog_of_right_le_zero

added theorem Int.clog_one_right

added theorem Int.clog_zero_right

added theorem Int.clog_zpow

added theorem Int.le_zpow_iff_clog_le

added def Int.log

added theorem Int.log_inv

added theorem Int.log_mono_right

added theorem Int.log_natCast

added theorem Int.log_of_left_le_one

added theorem Int.log_of_one_le_right

added theorem Int.log_of_right_le_one

added theorem Int.log_of_right_le_zero

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.lt_zpow_succ_log_self

added theorem Int.neg_clog_inv_eq_log

added theorem Int.neg_log_inv_eq_clog

added theorem Int.self_le_zpow_clog

added def Int.zpowLogGi

added theorem Int.zpow_le_iff_le_log

added theorem Int.zpow_log_le_self

added theorem Int.zpow_lt_iff_lt_clog

added theorem Int.zpow_pred_clog_lt_self