Commit 2022-12-12 18:31 e340c6a5

View on Github →

feat: port of Data.Nat.Gcd.Basic (#965) tracking cf9386b56953fb40904843af98b7a80757bbe7f9 Most of the code was already ported to Std. A couple of lemmas gave a linting error with simp normal form. I have commented out the simp attribute for this.

Estimated changes

added theorem Nat.coprime.lcm_eq_mul
added theorem Nat.coprime.symmetric
added theorem Nat.dvd_mul
added theorem Nat.gcd_add_self_left
added theorem Nat.gcd_add_self_right
added theorem Nat.gcd_greatest
added theorem Nat.gcd_self_add_left
added theorem Nat.gcd_self_add_right
added theorem Nat.lcm_dvd_iff
added theorem Nat.lcm_dvd_mul
added theorem Nat.pow_dvd_pow_iff