Commit 2023-01-26 12:54 2fcb378a

View on Github →

feat: port Data.Int.Parity (#1836)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Int/Parity.lean

added theorem Int.Odd.of_mul_left

added theorem Int.Odd.of_mul_right

added theorem Int.add_one_ediv_two_mul_two_of_odd

added theorem Int.ediv_two_mul_two_add_one_of_odd

added theorem Int.ediv_two_mul_two_of_even

added theorem Int.emod_two_ne_one

added theorem Int.emod_two_ne_zero

added theorem Int.even_add'

added theorem Int.even_add

added theorem Int.even_add_one

added theorem Int.even_coe_nat

added theorem Int.even_iff

added theorem Int.even_iff_not_odd

added theorem Int.even_mul

added theorem Int.even_mul_succ_self

added theorem Int.even_or_odd'

added theorem Int.even_or_odd

added theorem Int.even_pow'

added theorem Int.even_pow

added theorem Int.even_sub'

added theorem Int.even_sub

added theorem Int.even_xor'_odd'

added theorem Int.even_xor'_odd

added theorem Int.four_dvd_add_or_sub_of_odd

added theorem Int.isCompl_even_odd

added theorem Int.natAbs_even

added theorem Int.natAbs_odd

added theorem Int.ne_of_odd_add

added theorem Int.not_even_bit1

added theorem Int.not_even_iff

added theorem Int.not_even_one

added theorem Int.not_odd_iff

added theorem Int.odd_add'

added theorem Int.odd_add

added theorem Int.odd_coe_nat

added theorem Int.odd_iff

added theorem Int.odd_iff_not_even

added theorem Int.odd_mul

added theorem Int.odd_sub'

added theorem Int.odd_sub

added theorem Int.two_dvd_ne_zero

added theorem Int.two_mul_ediv_two_add_one_of_odd

added theorem Int.two_mul_ediv_two_of_even

added theorem Int.two_mul_ediv_two_of_odd

added theorem Int.two_not_dvd_two_mul_add_one