Commit 2024-08-23 09:30 b44ac128

View on Github →

chore: Don't simplify Odd n to ¬ Even n, but the other way around (#16024) This is simply not simpler From LeanAPAP

Estimated changes

modified theorem Int.even_or_odd
modified theorem Int.ne_of_odd_add
added theorem Int.not_even_iff_odd
added theorem Int.not_odd_iff_even
modified theorem Int.odd_iff_not_even
modified theorem Int.odd_mul
modified theorem Nat.ne_of_odd_add
added theorem Nat.not_even_iff_odd
added theorem Nat.not_odd_iff_even
modified theorem Nat.odd_iff_not_even
modified theorem Nat.odd_mul
added theorem mersenne_odd