Commit 2024-05-22 12:39 e7603ff3

View on Github →

chore: Delete Algebra.Parity (#11863) #12829 made Algebra.Parity almost empty. This PR deletes it.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Group/Even.lean

Modified Mathlib/Algebra/Order/Ring/Abs.lean

added theorem odd_abs

Deleted Mathlib/Algebra/Parity.lean

deleted theorem even_iff_exists_bit0

deleted theorem odd_abs

deleted theorem one_add_self_self

Modified Mathlib/Algebra/Ring/Parity.lean