Commit 2024-05-17 09:40 ad63ab75

View on Github →

chore: Delete Data.Nat.Parity (#12882) Scatter the lemmas in Data.Nat.Parity to earlier files:

  • Data.Nat.Defs
  • Algebra.Group.Nat
  • Algebra.Ring.Nat
  • Algebra.Order.Ring.Abs

Estimated changes

added theorem Nat.even_add
added theorem Nat.even_add_one
added theorem Nat.even_iff
added theorem Nat.even_mul
added theorem Nat.even_mul_pred_self
added theorem Nat.even_mul_succ_self
added theorem Nat.even_pow'
added theorem Nat.even_pow
added theorem Nat.even_sub
added theorem Nat.not_even_iff
added theorem Nat.not_even_one
added theorem Nat.two_dvd_ne_zero
added theorem Even.mod_even
added theorem Even.mod_even_iff
added theorem Odd.mod_even
added theorem Odd.mod_even_iff
added theorem Odd.ne_two_of_dvd_nat
added theorem Odd.of_dvd_nat
added theorem pow_eq_neg_one_iff
added theorem pow_eq_neg_pow_iff
added theorem pow_eq_one_iff_cases
added theorem pow_eq_pow_iff_cases
added theorem Nat.Even.sub_odd
added theorem Nat.Odd.of_mul_left
added theorem Nat.Odd.of_mul_right
added theorem Nat.Odd.sub_even
added theorem Nat.Odd.sub_odd
added theorem Nat.bit0_div_bit0
added theorem Nat.bit0_div_two
added theorem Nat.bit0_mod_bit0
added theorem Nat.bit1_div_bit0
added theorem Nat.bit1_div_two
added theorem Nat.bit1_mod_bit0
added theorem Nat.even_add'
added theorem Nat.even_div
added theorem Nat.even_iff_not_odd
added theorem Nat.even_or_odd'
added theorem Nat.even_or_odd
added theorem Nat.even_sub'
added theorem Nat.even_xor_odd'
added theorem Nat.even_xor_odd
added theorem Nat.isCompl_even_odd
added theorem Nat.ne_of_odd_add
added theorem Nat.not_even_bit1
added theorem Nat.not_odd_iff
added theorem Nat.odd_add'
added theorem Nat.odd_add
added theorem Nat.odd_iff
added theorem Nat.odd_iff_not_even
added theorem Nat.odd_mul
added theorem Nat.odd_sub'
added theorem Nat.odd_sub
added theorem Odd.not_two_dvd_nat
added theorem Nat.mod_two_ne_one
added theorem Nat.mod_two_ne_zero
deleted theorem Even.mod_even
deleted theorem Even.mod_even_iff
deleted theorem Nat.Even.sub_odd
deleted theorem Nat.Odd.of_mul_left
deleted theorem Nat.Odd.of_mul_right
deleted theorem Nat.Odd.sub_even
deleted theorem Nat.Odd.sub_odd
deleted theorem Nat.bit0_div_bit0
deleted theorem Nat.bit0_div_two
deleted theorem Nat.bit0_mod_bit0
deleted theorem Nat.bit1_div_bit0
deleted theorem Nat.bit1_div_two
deleted theorem Nat.bit1_mod_bit0
deleted theorem Nat.even_add'
deleted theorem Nat.even_add
deleted theorem Nat.even_add_one
deleted theorem Nat.even_div
deleted theorem Nat.even_iff
deleted theorem Nat.even_iff_not_odd
deleted theorem Nat.even_mul
deleted theorem Nat.even_mul_pred_self
deleted theorem Nat.even_mul_succ_self
deleted theorem Nat.even_or_odd'
deleted theorem Nat.even_or_odd
deleted theorem Nat.even_pow'
deleted theorem Nat.even_pow
deleted theorem Nat.even_sub'
deleted theorem Nat.even_sub
deleted theorem Nat.even_xor_odd'
deleted theorem Nat.even_xor_odd
deleted theorem Nat.isCompl_even_odd
deleted theorem Nat.mod_two_ne_one
deleted theorem Nat.mod_two_ne_zero
deleted theorem Nat.ne_of_odd_add
deleted theorem Nat.not_even_bit1
deleted theorem Nat.not_even_iff
deleted theorem Nat.not_even_one
deleted theorem Nat.not_odd_iff
deleted theorem Nat.odd_add'
deleted theorem Nat.odd_add
deleted theorem Nat.odd_iff
deleted theorem Nat.odd_iff_not_even
deleted theorem Nat.odd_mul
deleted theorem Nat.odd_sub'
deleted theorem Nat.odd_sub
deleted theorem Nat.two_dvd_ne_zero
deleted theorem Odd.mod_even
deleted theorem Odd.mod_even_iff
deleted theorem Odd.ne_two_of_dvd_nat
deleted theorem Odd.not_two_dvd_nat
deleted theorem Odd.of_dvd_nat
deleted theorem pow_eq_neg_one_iff
deleted theorem pow_eq_neg_pow_iff
deleted theorem pow_eq_one_iff_cases
deleted theorem pow_eq_one_iff_of_ne_zero
deleted theorem pow_eq_pow_iff_cases
deleted theorem pow_eq_pow_iff_of_ne_zero