Commit 2024-05-07 08:14 43881b58

View on Github →

chore: Move sign of power lemmas (#11986)

  • Move the sign of power lemmas from Algebra.Parity to Algebra.GroupPower.Order.
  • For this to work, I must swap the order of import between Algebra.GroupPower.Order and Algebra.Parity. This means that I need to weaken one assert_not_exists to allow importing Data.Set.Defs. This is inconsequential.
  • Use them to golf and deprecate the bit0/bit1 lemmas
  • Delete the deprecated pow_bit0_abs, pow_bit0_pos_of_neg, pow_bit1_neg

Estimated changes

added theorem Even.pow_nonneg
added theorem Even.pow_pos
added theorem Even.pow_pos_iff
added theorem Odd.pow_neg_iff
added theorem Odd.pow_nonneg_iff
added theorem Odd.pow_nonpos_iff
added theorem Odd.pow_pos_iff
added theorem Odd.strictMono_pow
modified theorem pow_bit0_nonneg
modified theorem pow_bit0_pos
modified theorem pow_bit0_pos_iff
deleted theorem pow_bit0_pos_of_neg
deleted theorem pow_bit1_neg
modified theorem pow_bit1_neg_iff
modified theorem pow_bit1_nonneg_iff
modified theorem pow_bit1_nonpos_iff
modified theorem pow_bit1_pos_iff
modified theorem sq_pos_iff
modified theorem sq_pos_of_neg
modified theorem strictMono_pow_bit1
added theorem Even.pow_abs
deleted theorem Even.pow_abs
deleted theorem Even.pow_nonneg
deleted theorem Even.pow_pos
deleted theorem Even.pow_pos_iff
deleted theorem Odd.pow_neg_iff
deleted theorem Odd.pow_nonneg_iff
deleted theorem Odd.pow_nonpos_iff
deleted theorem Odd.pow_pos_iff
deleted theorem Odd.strictMono_pow
modified theorem even_iff_two_dvd
modified theorem odd_iff_exists_bit1
deleted theorem pow_bit0_abs