Commit 2024-04-23 04:59 61ef41dd

View on Github →

chore: move NormalizedGCDMonoid ℕ to reduce imports (#12341) Previously Mathlib.GroupTheory.Perm.Fin knew about LinearMap for no good reason, because it relied on Mathlib.RingTheory.Int.Basic for some basic things, but that file also has heavy imports.

Estimated changes