Commit 2024-04-05 07:05 22afa0a4
View on Github →chore: split NumberTheory.NumberField.CanonicalEmbedding
(#11873)
#8361 indicates that this is the most compute-intensive file on the longest pole for compiling Mathlib. It's bottlenecked dependency is Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
, and this import isn't used until the second half of the file, in the sections regarding convex bodies. I am therefore splitting the file at that point, from the context of the file it seems to me that this is a sensible split anyway.