Commit 2025-02-17 21:24 5cf7d900

chore(Algebra/EuclideanDomain): clean up imports for Defs.lean (#22000) We can reduce the imports of this file if we move some lemmas downstream. It's a -137 / 50% reduction for definition of euclidean domains and a few downstream files, and a +1 / +0.1% increase for PrincipalIdealDomain and a lot of downstream files: I think that's definitely worth it. (Especially if we can split PrincipalIdealDomain later on.)