Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2022-01-17 19:54
e096b99a
View on Github →
refactor(set_theory/ordinal_arithmetic): Rename
power
to
opow
(
#11279
)
Estimated changes
Modified
src/set_theory/ordinal_arithmetic.lean
added
theorem
ordinal.add_lt_omega_opow
deleted
theorem
ordinal.add_lt_omega_power
added
theorem
ordinal.add_omega_opow
deleted
theorem
ordinal.add_omega_power
added
theorem
ordinal.le_opow_self
deleted
theorem
ordinal.le_power_self
added
theorem
ordinal.log_opow
added
theorem
ordinal.log_opow_mul_add
deleted
theorem
ordinal.log_power
deleted
theorem
ordinal.log_power_mul_add
added
theorem
ordinal.lt_opow_of_limit
added
theorem
ordinal.lt_opow_succ_log
deleted
theorem
ordinal.lt_power_of_limit
deleted
theorem
ordinal.lt_power_succ_log
added
theorem
ordinal.mul_lt_omega_opow
deleted
theorem
ordinal.mul_lt_omega_power
added
theorem
ordinal.mul_omega_opow_opow
deleted
theorem
ordinal.mul_omega_power_power
added
theorem
ordinal.nat_cast_opow
deleted
theorem
ordinal.nat_cast_power
added
theorem
ordinal.one_opow
deleted
theorem
ordinal.one_power
added
def
ordinal.opow
added
theorem
ordinal.opow_add
added
theorem
ordinal.opow_dvd_opow
added
theorem
ordinal.opow_dvd_opow_iff
added
theorem
ordinal.opow_is_limit
added
theorem
ordinal.opow_is_limit_left
added
theorem
ordinal.opow_is_normal
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
added
theorem
ordinal.opow_lt_omega
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_omega
added
theorem
ordinal.opow_one
added
theorem
ordinal.opow_pos
added
theorem
ordinal.opow_right_inj
added
theorem
ordinal.opow_succ
added
theorem
ordinal.opow_zero
deleted
def
ordinal.power
deleted
theorem
ordinal.power_add
deleted
theorem
ordinal.power_dvd_power
deleted
theorem
ordinal.power_dvd_power_iff
deleted
theorem
ordinal.power_is_limit
deleted
theorem
ordinal.power_is_limit_left
deleted
theorem
ordinal.power_is_normal
deleted
theorem
ordinal.power_le_of_limit
deleted
theorem
ordinal.power_le_power_iff_right
deleted
theorem
ordinal.power_le_power_left
deleted
theorem
ordinal.power_le_power_right
deleted
theorem
ordinal.power_limit
deleted
theorem
ordinal.power_log_le
deleted
theorem
ordinal.power_lt_omega
deleted
theorem
ordinal.power_lt_power_iff_right
deleted
theorem
ordinal.power_lt_power_left_of_succ
deleted
theorem
ordinal.power_mul
deleted
theorem
ordinal.power_mul_add_lt_power_mul_succ
deleted
theorem
ordinal.power_mul_add_lt_power_succ
deleted
theorem
ordinal.power_mul_add_pos
deleted
theorem
ordinal.power_ne_zero
deleted
theorem
ordinal.power_omega
deleted
theorem
ordinal.power_one
deleted
theorem
ordinal.power_pos
deleted
theorem
ordinal.power_right_inj
deleted
theorem
ordinal.power_succ
deleted
theorem
ordinal.power_zero
added
theorem
ordinal.zero_opow'
added
theorem
ordinal.zero_opow
deleted
theorem
ordinal.zero_power'
deleted
theorem
ordinal.zero_power
Modified
src/set_theory/ordinal_notation.lean
added
def
nonote.opow
deleted
def
nonote.power
added
theorem
nonote.repr_opow
deleted
theorem
nonote.repr_power
added
theorem
onote.NF.of_dvd_omega_opow
deleted
theorem
onote.NF.of_dvd_omega_power
added
def
onote.opow
added
def
onote.opow_aux
added
theorem
onote.opow_def
deleted
def
onote.power
deleted
def
onote.power_aux
deleted
theorem
onote.power_def
added
theorem
onote.repr_opow
added
theorem
onote.repr_opow_aux₁
added
theorem
onote.repr_opow_aux₂
deleted
theorem
onote.repr_power
deleted
theorem
onote.repr_power_aux₁
deleted
theorem
onote.repr_power_aux₂
added
theorem
onote.scale_opow_aux
deleted
theorem
onote.scale_power_aux