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.

Estimated changes