int.gcd

Stream: general

[Paul van Wamelen]

The algebra/gcd_monoid.lean file contains a whole bunch of gcd lemmas for the integers that are neither needed nor used in the gcd_monoid file.
Should these be moved to the data/int/gcd.lean file? I've tried doing it but it has some other consequences. We probably then should also move the lcm results to the data/int/gcd.lean file. But those are proved using the gcd_monoid results. So we need to import gcd_monoid into data/int/gcd.lean. Is that OK?
One consequence of that was that we get a circular import from this result:

lemma pow_gcd_eq_one {M : Type*} [monoid M] (x : M) {m n : ℕ} (hm : x ^ m = 1) (hn : x ^ n = 1) :
  x ^ m.gcd n = 1

General monoid theory needs this result about (extended) gcds, but gcds need ring theory that needs monoids. This can be fixed by splitting out the extended gcd results into its own file. Is all this worth the effort? If so, I can PR this. Or just PR it and see what the reviewers think.

[Paul van Wamelen]

This is now PR #4384.