Commit 2024-10-24 13:22 3693a5a5
View on Github →chore: split NumberTheory/NumberField/Discriminant (#18168) Splits NumberTheory/NumberField/Discriminant in Defs and Basic. Defs suffices for Cyclotomic/Discriminant, and doesn't require much analysis. Basic contains Hermite's theorem.