mathlib3

de4a9ed1 - feat(ring_theory/roots_of_unity): generalisation linter (#16014)

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`!