mathlib3

26660331 - refactor(algebra/gcd_monoid): don't require normalization (#9443)

refactor(algebra/gcd_monoid): don't require normalization (#9443) This will allow us to set up a gcd_monoid instance for all euclidean_domains and generalize the results in ring_theory/euclidean_domain.lean to PIDs.