mathlib

85117294 - refactor(data/int/gcd,ring_theory/int/basic): collect integer divisibility results from various files (#4572)

refactor(data/int/gcd,ring_theory/int/basic): collect integer divisibility results from various files (#4572) Applying comments from PR #4384. In particular: 1) Move the gcd and lcm results from gcd_monoid to `data/int/gcd.lean` with new proofs (for a few lcm results) that do not need ring theory. 2) Try to collect applications of ring theory to ℕ and ℤ into a new file `ring_theory/int/basic.lean`. Co-authored-by: paulvanwamelen <30371019+paulvanwamelen@users.noreply.github.com>