Commit 2021-04-18 22:03 969c6a3e

View on Github →

feat(data/int/parity): update to match nat/parity (where applicable) (#7155) We had a number of lemmas for nat but not for int, so I add them. I also globalize variables in the file and add a module docstring.

Estimated changes

Modified src/data/int/parity.lean

added theorem int.even.add_even

added theorem int.even.add_odd

added theorem int.even.mul_left

added theorem int.even.mul_right

added theorem int.even.sub_even

added theorem int.even.sub_odd

added theorem int.even_add'

modified theorem int.even_add

added theorem int.even_add_one

modified theorem int.even_coe_nat

modified theorem int.even_iff

modified theorem int.even_iff_not_odd

modified theorem int.even_mul

modified theorem int.even_neg

modified theorem int.even_pow

added theorem int.even_sub'

modified theorem int.even_sub

added theorem int.is_compl_even_odd

modified theorem int.mod_two_ne_one

modified theorem int.mod_two_ne_zero

modified theorem int.ne_of_odd_sum

modified theorem int.not_even_iff

modified theorem int.not_odd_iff

added theorem int.odd.add_even

added theorem int.odd.add_odd

added theorem int.odd.mul

added theorem int.odd.of_mul_left

added theorem int.odd.of_mul_right

added theorem int.odd.sub_even

added theorem int.odd.sub_odd

added theorem int.odd_add'

added theorem int.odd_add

modified theorem int.odd_iff

modified theorem int.odd_iff_not_even

added theorem int.odd_mul

added theorem int.odd_sub'

added theorem int.odd_sub

modified theorem int.two_dvd_ne_zero

added theorem int.two_not_dvd_two_mul_add_one