Commit 2024-11-04 20:32 dbc6f5d7
View on Github →chore(Algebra/Ring/Int): split Algebra/Ring/Int.lean into Defs, Parity and Units (#18526)
The definition of the ring structure on the integers in this file was accompanied by a set of miscellaneous lemmas. If we split off the lemmas to their own files, they are not needed nearly as often.
(Hopefully this also allows some cleaning up around Data.Int.Cast in the future, although that seems still to be in a bit too much of a mess right now.)