mathlib
b602702a - chore(number_theory/cyclotomic): tidying (#19067)

Commit
2 years ago
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.
Author
Parents
Loading