Commit 2025-07-31 03:42 4e6a2162

View on Github →

feat: use grind in Nat/Int parity results (#27661)

Estimated changes

Modified Mathlib/Algebra/Group/Int/Even.lean

modified theorem Int.ediv_two_mul_two_of_even

modified theorem Int.emod_two_ne_one

modified theorem Int.emod_two_ne_zero

modified theorem Int.even_add

modified theorem Int.even_add_one

modified theorem Int.even_coe_nat

modified theorem Int.even_mul

modified theorem Int.even_pow'

modified theorem Int.even_pow

modified theorem Int.even_sub

modified theorem Int.even_sub_one

modified theorem Int.not_even_iff

modified theorem Int.two_dvd_ne_zero

modified theorem Int.two_mul_ediv_two_of_even

modified theorem Int.two_not_dvd_two_mul_add_one

Modified Mathlib/Algebra/Group/Nat/Even.lean

modified theorem Nat.even_add

modified theorem Nat.even_add_one

modified theorem Nat.even_mul

modified theorem Nat.even_mul_pred_self

modified theorem Nat.even_mul_succ_self

modified theorem Nat.even_pow'

modified theorem Nat.even_pow

modified theorem Nat.even_sub

modified theorem Nat.not_even_iff

modified theorem Nat.not_even_one

modified theorem Nat.one_lt_of_ne_zero_of_even

modified theorem Nat.succ_mod_two_eq_one_iff

modified theorem Nat.succ_mod_two_eq_zero_iff

modified theorem Nat.two_dvd_ne_zero

modified theorem Nat.two_not_dvd_two_mul_add_one

modified theorem Nat.two_not_dvd_two_mul_sub_one

Modified Mathlib/Algebra/Ring/Int/Parity.lean

modified theorem Int.add_one_ediv_two_mul_two_of_odd

modified theorem Int.ediv_two_mul_two_add_one_of_odd

modified theorem Int.even_add'

modified theorem Int.even_mul_pred_self

modified theorem Int.even_mul_succ_self

modified theorem Int.even_or_odd

modified theorem Int.even_sub'

modified theorem Int.natAbs_even

modified theorem Int.natAbs_odd

modified theorem Int.ne_of_odd_add

modified theorem Int.not_even_iff_odd

modified theorem Int.not_even_two_mul_add_one

modified theorem Int.not_odd_iff

modified theorem Int.not_odd_iff_even

modified theorem Int.not_odd_zero

modified theorem Int.odd_add'

modified theorem Int.odd_add

modified theorem Int.odd_coe_nat

modified theorem Int.odd_pow'

modified theorem Int.odd_pow

modified theorem Int.odd_sign_iff

modified theorem Int.odd_sub'

modified theorem Int.odd_sub

modified theorem Int.two_mul_ediv_two_add_one_of_odd

modified theorem Int.two_mul_ediv_two_of_odd

Modified Mathlib/Algebra/Ring/Parity.lean

modified theorem Nat.Even.sub_odd

modified theorem Nat.Odd.sub_even

modified theorem Nat.Odd.sub_odd

modified theorem Nat.div_two_mul_two_add_one_of_odd

modified theorem Nat.even_add'

modified theorem Nat.even_sub'

modified theorem Nat.even_xor_odd

modified theorem Nat.mod_two_add_add_odd_mod_two

modified theorem Nat.mod_two_add_succ_mod_two

modified theorem Nat.ne_of_odd_add

modified theorem Nat.not_even_iff_odd

modified theorem Nat.not_even_two_mul_add_one

modified theorem Nat.not_odd_iff

modified theorem Nat.not_odd_iff_even

modified theorem Nat.not_odd_zero

modified theorem Nat.odd_add'

modified theorem Nat.odd_add

modified theorem Nat.odd_add_one

modified theorem Nat.odd_mul

modified theorem Nat.odd_pow_iff

modified theorem Nat.odd_sub'

modified theorem Nat.odd_sub

modified theorem Nat.one_add_div_two_mul_two_of_odd

modified theorem Nat.succ_mod_two_add_mod_two

modified theorem Nat.two_mul_div_two_add_one_of_odd

modified theorem Odd.not_two_dvd_nat

Modified Mathlib/Logic/Basic.lean

modified theorem xor_comm

added theorem xor_def

modified theorem xor_false

modified theorem xor_not_left

modified theorem xor_not_not

modified theorem xor_not_right

modified theorem xor_self

modified theorem xor_true