Commit 2024-04-05 11:13 0996e120

View on Github →

chore: move some basic multiplicity results out of Mathlib.RingTheory.Int.Basic (#11919) This means Mathlib.NumberTheory.Padics.PadicVal no longer needs to depend on Mathlib.RingTheory.Int.Basic, which is surprisingly heavy (in particular through Mathlib.RingTheory.Noetherian).

Estimated changes