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.

Estimated changes