Commit 2023-02-20 12:02 be32c274

View on Github →

feat: port SetTheory.Ordinal.Exponential (#2330)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean

deleted theorem Ordinal.add_log_le_log_mul

deleted theorem Ordinal.div_opow_log_lt

deleted theorem Ordinal.left_le_opow

deleted def Ordinal.log

deleted theorem Ordinal.log_def

deleted theorem Ordinal.log_eq_zero

deleted theorem Ordinal.log_le_self

deleted theorem Ordinal.log_mod_opow_log_lt_log_self

deleted theorem Ordinal.log_mono_right

deleted theorem Ordinal.log_nonempty

deleted theorem Ordinal.log_of_left_le_one

deleted theorem Ordinal.log_of_not_one_lt_left

deleted theorem Ordinal.log_one_left

deleted theorem Ordinal.log_one_right

deleted theorem Ordinal.log_opow

deleted theorem Ordinal.log_opow_mul_add

deleted theorem Ordinal.log_pos

deleted theorem Ordinal.log_zero_left

deleted theorem Ordinal.log_zero_right

deleted theorem Ordinal.lt_opow_iff_log_lt

deleted theorem Ordinal.lt_opow_of_limit

deleted theorem Ordinal.lt_opow_succ_log_self

deleted theorem Ordinal.mod_opow_log_lt_self

deleted theorem Ordinal.nat_cast_opow

deleted theorem Ordinal.one_opow

deleted theorem Ordinal.opow_add

deleted theorem Ordinal.opow_def

deleted theorem Ordinal.opow_dvd_opow

deleted theorem Ordinal.opow_dvd_opow_iff

deleted theorem Ordinal.opow_isLimit

deleted theorem Ordinal.opow_isLimit_left

deleted theorem Ordinal.opow_isNormal

deleted theorem Ordinal.opow_le_iff_le_log

deleted theorem Ordinal.opow_le_of_limit

deleted theorem Ordinal.opow_le_opow_iff_right

deleted theorem Ordinal.opow_le_opow_left

deleted theorem Ordinal.opow_le_opow_right

deleted theorem Ordinal.opow_limit

deleted theorem Ordinal.opow_log_le_self

deleted theorem Ordinal.opow_lt_opow_iff_right

deleted theorem Ordinal.opow_lt_opow_left_of_succ

deleted theorem Ordinal.opow_mul

deleted theorem Ordinal.opow_mul_add_lt_opow_mul_succ

deleted theorem Ordinal.opow_mul_add_lt_opow_succ

deleted theorem Ordinal.opow_mul_add_pos

deleted theorem Ordinal.opow_ne_zero

deleted theorem Ordinal.opow_one

deleted theorem Ordinal.opow_one_add

deleted theorem Ordinal.opow_pos

deleted theorem Ordinal.opow_right_inj

deleted theorem Ordinal.opow_succ

deleted theorem Ordinal.opow_zero

deleted theorem Ordinal.right_le_opow

deleted theorem Ordinal.succ_log_def

deleted theorem Ordinal.sup_opow_nat

deleted theorem Ordinal.zero_opow'

deleted theorem Ordinal.zero_opow

Created Mathlib/SetTheory/Ordinal/Exponential.lean

added theorem Ordinal.add_log_le_log_mul

added theorem Ordinal.div_opow_log_lt

added theorem Ordinal.left_le_opow

added def Ordinal.log

added theorem Ordinal.log_def

added theorem Ordinal.log_eq_zero

added theorem Ordinal.log_le_self

added theorem Ordinal.log_mod_opow_log_lt_log_self

added theorem Ordinal.log_mono_right

added theorem Ordinal.log_nonempty

added theorem Ordinal.log_of_left_le_one

added theorem Ordinal.log_of_not_one_lt_left

added theorem Ordinal.log_one_left

added theorem Ordinal.log_one_right

added theorem Ordinal.log_opow

added theorem Ordinal.log_opow_mul_add

added theorem Ordinal.log_pos

added theorem Ordinal.log_zero_left

added theorem Ordinal.log_zero_right

added theorem Ordinal.lt_opow_iff_log_lt

added theorem Ordinal.lt_opow_of_limit

added theorem Ordinal.lt_opow_succ_log_self

added theorem Ordinal.mod_opow_log_lt_self

added theorem Ordinal.nat_cast_opow

added theorem Ordinal.one_opow

added theorem Ordinal.opow_add

added theorem Ordinal.opow_def

added theorem Ordinal.opow_dvd_opow

added theorem Ordinal.opow_dvd_opow_iff

added theorem Ordinal.opow_isLimit

added theorem Ordinal.opow_isLimit_left

added theorem Ordinal.opow_isNormal

added theorem Ordinal.opow_le_iff_le_log

added theorem Ordinal.opow_le_of_limit

added theorem Ordinal.opow_le_opow_iff_right

added theorem Ordinal.opow_le_opow_left

added theorem Ordinal.opow_le_opow_right

added theorem Ordinal.opow_limit

added theorem Ordinal.opow_log_le_self

added theorem Ordinal.opow_lt_opow_iff_right

added theorem Ordinal.opow_lt_opow_left_of_succ

added theorem Ordinal.opow_mul

added theorem Ordinal.opow_mul_add_lt_opow_mul_succ

added theorem Ordinal.opow_mul_add_lt_opow_succ

added theorem Ordinal.opow_mul_add_pos

added theorem Ordinal.opow_ne_zero

added theorem Ordinal.opow_one

added theorem Ordinal.opow_one_add

added theorem Ordinal.opow_pos

added theorem Ordinal.opow_right_inj

added theorem Ordinal.opow_succ

added theorem Ordinal.opow_zero

added theorem Ordinal.right_le_opow

added theorem Ordinal.succ_log_def

added theorem Ordinal.sup_opow_nat

added theorem Ordinal.zero_opow'

added theorem Ordinal.zero_opow