[Merged by Bors] - refactor(algebra/gcd_monoid): don't require normalization

[Ruben-VandeVelde]

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.

---

• depends on: [Merged by Bors] - refactor(ring_theory/unique_factorization_domain): rename unique_factorization_monoid.factors #9503

This still needs some documentation and lint fixes, and I didn't pay much attention to names yet, but I'd like to hear if people think this is the right direction first.

[eric-wieser]

Doesn't a bounded lattice require lcm and gcd be commutative and associative, which is no longer true of the weaker typeclass?

[Ruben-VandeVelde]

That seems plausible - I can't find an actual Lean instance, though, so I'm not sure what this comment is referring to.

[eric-wieser]

Do the generalisations you care about not have associativity or commutativity either?

[Ruben-VandeVelde]

No commutativity, in any case:

import algebra.euclidean_domain

#eval euclidean_domain.gcd (1 : int) (-1 : int)
-- 1
#eval euclidean_domain.gcd (-1 : int) (1 : int)
-- -1

[kim-em]

Please don't write /-- TODO -/. :-) The whole point of the linter is to warn you that these are still TODO.

I'll mark as WIP for now, for you to add the doc-strings, but otherwise this is looking good!

[awainverse]

I left some small recommendations. This seems like a good idea overall.
In particular, this doesn't get rid of the existing functionality of the existing gcd_monoid, just renames it, so I'm happy.

I think it would also be nice to tie a gcd_monoid structure on M to a normalized_gcd_monoid structure on associates M, but that should probably wait for a later PR because this one is a lot of lines!

[Ruben-VandeVelde]

I think it would also be nice to tie a gcd_monoid structure on M to a normalized_gcd_monoid structure on associates M, but that should probably wait for a later PR because this one is a lot of lines!

Yeah, I'm happy to do that after this.

[kim-em]

bors d+

[bors]

✌️ Ruben-VandeVelde can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[Ruben-VandeVelde]

bors merge

Thanks!

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests