Commit 2022-08-11 21:15 de4a9ed1

feat(ring_theory/roots_of_unity): generalisation linter (#16014) This was really a huge generalisation of many results, and in fact now no results in this file depend on things being fields (just char-zero integral domains, such as ℤ!) Also a thanks to @YaelDillies for the division_monoid refactor, which united many similar-looking results here. This will be very helpful on flt_regular!