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

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
deleted theorem ordinal.log_power
deleted theorem ordinal.log_power_mul_add
deleted theorem ordinal.lt_power_of_limit
deleted theorem ordinal.lt_power_succ_log
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_is_limit
added theorem ordinal.opow_is_normal
added theorem ordinal.opow_limit
added theorem ordinal.opow_log_le
added theorem ordinal.opow_lt_omega
added theorem ordinal.opow_mul
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_is_limit
deleted theorem ordinal.power_is_normal
deleted theorem ordinal.power_le_of_limit
deleted theorem ordinal.power_limit
deleted theorem ordinal.power_log_le
deleted theorem ordinal.power_lt_omega
deleted theorem ordinal.power_mul
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
added def nonote.opow
deleted def nonote.power
added theorem nonote.repr_opow
deleted theorem nonote.repr_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