Commit 2025-02-19 08:59 535400d2
View on Github →chore(Algebra/CharP): move modeq lemmas from Defs to Basic (#21994)
These lemmas are useful but they bring in a lot of dependencies such as GCDs and order structures, so I think we should rather have them in the Basic files to keep the definition minimal.