Commit 2023-01-25 09:35 234131a3

View on Github →

feat: port Data.Nat.Parity (#1661) Backported in leanprover-community/mathlib#18221.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Parity.lean

added theorem Dvd.dvd.even

added theorem Even.trans_dvd

modified theorem even_bit0

modified theorem odd_bit1

modified theorem range_two_mul

Created Mathlib/Data/Nat/Parity.lean

added theorem Even.mod_even

added theorem Even.mod_even_iff

added theorem Function.Involutive.iterate_bit0

added theorem Function.Involutive.iterate_bit1

added theorem Function.Involutive.iterate_eq_id

added theorem Function.Involutive.iterate_eq_self

added theorem Function.Involutive.iterate_even

added theorem Function.Involutive.iterate_odd

added theorem Function.Involutive.iterate_two_mul

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.div_two_mul_two_add_one_of_odd

added theorem Nat.div_two_mul_two_of_even

added theorem Nat.even_add'

added theorem Nat.even_add

added theorem Nat.even_add_one

added theorem Nat.even_div

added theorem Nat.even_iff

added theorem Nat.even_iff_not_odd

added theorem Nat.even_mul

added theorem Nat.even_mul_self_pred

added theorem Nat.even_mul_succ_self

added theorem Nat.even_or_odd'

added theorem Nat.even_or_odd

added theorem Nat.even_pow'

added theorem Nat.even_pow

added theorem Nat.even_sub'

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.mod_two_add_add_odd_mod_two

added theorem Nat.mod_two_add_succ_mod_two

added theorem Nat.mod_two_ne_one

added theorem Nat.mod_two_ne_zero

added theorem Nat.ne_of_odd_add

added theorem Nat.not_even_bit1

added theorem Nat.not_even_iff

added theorem Nat.not_even_one

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 Nat.one_add_div_two_mul_two_of_odd

added theorem Nat.succ_mod_two_add_mod_two

added theorem Nat.two_dvd_ne_zero

added theorem Nat.two_mul_div_two_add_one_of_odd

added theorem Nat.two_mul_div_two_of_even

added theorem Nat.two_not_dvd_two_mul_add_one

added theorem Nat.two_not_dvd_two_mul_sub_one

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 neg_one_pow_eq_one_iff_even

Modified Mathlib/Data/Nat/Prime.lean

added theorem Nat.Prime.even_sub_one