Commit 2024-10-22 08:37 5eb330bc
View on Github →chore(Algebra/PUnitInstances): split off GCDMonoid PUnit
instance (#18014)
This instance does not seem to be used anywhere in Mathlib and splitting it off should allow us to shave quite a few imports from low down in the hierarchy.