Commit 2024-01-18 17:23 91ac6909

View on Github →

chore: Move order lemmas about zpow (#9805) These lemmas can be proved earlier. Part of #9411

Estimated changes

deleted theorem abs_add_eq_add_abs_iff
deleted theorem abs_add_eq_add_abs_le
deleted theorem abs_nsmul
deleted theorem abs_pow
deleted theorem abs_zsmul
deleted theorem one_lt_zpow'
deleted theorem pow_bit1_neg_iff
deleted theorem pow_bit1_nonneg_iff
deleted theorem pow_bit1_nonpos_iff
deleted theorem pow_bit1_pos_iff
deleted theorem strictMono_pow_bit1
deleted theorem zpow_eq_zpow_iff'
deleted theorem zpow_le_zpow'
deleted theorem zpow_le_zpow
deleted theorem zpow_le_zpow_iff'
deleted theorem zpow_le_zpow_iff
deleted theorem zpow_left_inj
deleted theorem zpow_left_injective
deleted theorem zpow_lt_zpow'
deleted theorem zpow_lt_zpow
deleted theorem zpow_lt_zpow_iff'
deleted theorem zpow_lt_zpow_iff
deleted theorem zpow_mono_left
deleted theorem zpow_mono_right
deleted theorem zpow_right_strictMono
deleted theorem zpow_strictMono_left
deleted theorem abs_le_of_sq_le_sq'
deleted theorem abs_le_of_sq_le_sq
deleted theorem abs_lt_of_sq_lt_sq'
deleted theorem abs_lt_of_sq_lt_sq
deleted theorem abs_neg_one_pow
deleted theorem abs_pow_eq_one
deleted theorem abs_sq
deleted theorem one_le_sq_iff_one_le_abs
deleted theorem one_lt_sq_iff_one_lt_abs
added theorem one_lt_zpow'
deleted theorem pow_abs
added theorem pow_bit1_neg_iff
added theorem pow_bit1_nonneg_iff
added theorem pow_bit1_nonpos_iff
added theorem pow_bit1_pos_iff
modified theorem pow_left_strictMonoOn
deleted theorem sq_abs
deleted theorem sq_eq_sq_iff_abs_eq_abs
deleted theorem sq_le_one_iff_abs_le_one
deleted theorem sq_le_sq'
deleted theorem sq_le_sq
deleted theorem sq_lt_one_iff_abs_lt_one
deleted theorem sq_lt_sq'
deleted theorem sq_lt_sq
modified theorem sq_pos_iff
added theorem strictMono_pow_bit1
added theorem zpow_eq_zpow_iff'
added theorem zpow_le_zpow'
added theorem zpow_le_zpow
added theorem zpow_le_zpow_iff'
added theorem zpow_le_zpow_iff
added theorem zpow_left_inj
added theorem zpow_left_injective
added theorem zpow_lt_zpow'
added theorem zpow_lt_zpow
added theorem zpow_lt_zpow_iff'
added theorem zpow_lt_zpow_iff
added theorem zpow_mono_left
added theorem zpow_mono_right
added theorem zpow_right_strictMono
added theorem zpow_strictMono_left
added theorem mabs_pow
modified def absHom
modified theorem abs_eq_iff_mul_self_eq
modified theorem abs_le_iff_mul_self_le
added theorem abs_le_of_sq_le_sq'
added theorem abs_le_of_sq_le_sq
modified theorem abs_lt_iff_mul_self_lt
added theorem abs_lt_of_sq_lt_sq'
added theorem abs_lt_of_sq_lt_sq
modified theorem abs_mul
modified theorem abs_mul_abs_self
modified theorem abs_mul_self
added theorem abs_neg_one_pow
modified theorem abs_one
added theorem abs_pow
added theorem abs_pow_eq_one
added theorem abs_sq
modified theorem abs_two
added theorem mabs_zpow
added theorem pow_abs
added theorem sq_abs
added theorem sq_le_sq'
added theorem sq_le_sq
added theorem sq_lt_sq'
added theorem sq_lt_sq