Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-16 05:24 1f1289fc

View on Github →

feat(algebra/parity + data/{int, nat}/parity): parity lemmas for general semirings (#12718) This PR proves some general facts about adding even/odd elements in a semiring, thus removing the need to proving the same results for nat and int.

Estimated changes

added theorem even.add_even
added theorem even.add_odd
added theorem odd.add_even
added theorem odd.add_odd
deleted theorem int.even.add_even
deleted theorem int.even.add_odd
deleted theorem int.odd.add_even
deleted theorem int.odd.add_odd
deleted theorem nat.even.add_even
deleted theorem nat.even.add_odd
deleted theorem nat.odd.add_even
deleted theorem nat.odd.add_odd