mathlib3

bf3b618e - feat(algebra/gcd_monoid/div): add finset.int.gcd_is_unit_of_div_gcd and similar results (#16838)

feat(algebra/gcd_monoid/div): add finset.int.gcd_is_unit_of_div_gcd and similar results (#16838) We add `finset.nat.gcd_is_unit_of_div_gcd`, `finset.int.gcd_is_unit_of_div_gcd` and `finset.polynomial.gcd_is_unit_of_div_gcd`. These are the analogue of [finset.coprime_of_div_gcd](https://leanprover-community.github.io/mathlib_docs/algebra/gcd_monoid/nat.html#finset.coprime_of_div_gcd) for `ℤ` and `K[X]`. We also move [finset.coprime_of_div_gcd](https://leanprover-community.github.io/mathlib_docs/algebra/gcd_monoid/nat.html#finset.coprime_of_div_gcd) (changing its name). From flt-regular