Commit 2024-11-25 20:58 69eeb745

View on Github →

chore(Data/Nat/Defs): rename two lemmas that were not about Ne (#19476) From LeanCamCombi

Estimated changes

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

modified theorem Nat.not_even_iff

Modified Mathlib/Algebra/Ring/Parity.lean

modified theorem Nat.not_odd_iff

Modified Mathlib/Data/Nat/Defs.lean

modified theorem Nat.mod_two_ne_one

modified theorem Nat.mod_two_ne_zero

added theorem Nat.mod_two_not_eq_one

added theorem Nat.mod_two_not_eq_zero