Commit 2020-10-14 08:24 85117294
View on Github →refactor(data/int/gcd,ring_theory/int/basic): collect integer divisibility results from various files (#4572) Applying comments from PR #4384. In particular:
- 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. - Try to collect applications of ring theory to ℕ and ℤ into a new file
ring_theory/int/basic.lean
.