Commit 2024-09-30 02:32 07a48737

View on Github →

chore(Data/ZMod/Parity): Delete (#17236) The files can be moved earlier at no cost

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Combinatorics/SimpleGraph/DegreeSum.lean

Modified Mathlib/Data/ZMod/Basic.lean

added theorem ZMod.eq_one_iff_odd

added theorem ZMod.eq_zero_iff_even

added theorem ZMod.ne_zero_iff_odd

Deleted Mathlib/Data/ZMod/Parity.lean

deleted theorem ZMod.eq_one_iff_odd

deleted theorem ZMod.eq_zero_iff_even

deleted theorem ZMod.ne_zero_iff_odd

Modified Mathlib/GroupTheory/Coxeter/Inversion.lean