mathlib3

4c4d47c2 - feat(algebra/gcd_monoid): noncomputably defines `gcd_monoid` structures from partial information (#4664)

feat(algebra/gcd_monoid): noncomputably defines `gcd_monoid` structures from partial information (#4664) Adds the following 4 noncomputable functions which define `gcd_monoid` instances. `gcd_monoid_of_gcd` takes as input a `gcd` function and a few of its properties `gcd_monoid_of_lcm` takes as input a `lcm` function and a few of its properties `gcd_monoid_of_exists_gcd` takes as input the prop that every two elements have a `gcd` `gcd_monoid_of_exists_lcm` takes as input the prop that every two elements have an `lcm` Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>