Commit 2023-05-23 14:49 b602702a

chore(number_theory/cyclotomic): tidying (#19067) Now that the splitting field diamond is gone, we can tidy the code around these areas a bit more. This also incidentally removed another diamond (the ℤ-algebra on cyclotomic_ring) and so we can remove ugliness related to this.