Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-09-02 06:00 d35dc135

View on Github →

feat(data/nat/gcd): add simple lemmas (#1382)

feat(data/nat/gcd): more simple lemmas
Prove iff instead of one side implication

Estimated changes

Modified src/data/nat/gcd.lean

added theorem nat.coprime.gcd_both

added theorem nat.coprime.gcd_left

added theorem nat.coprime.gcd_mul

added theorem nat.coprime.gcd_right

deleted theorem nat.exists_eq_prod_and_dvd_and_dvd

added theorem nat.gcd_eq_left_iff_dvd

added theorem nat.gcd_eq_right_iff_dvd

added theorem nat.gcd_le_left

added theorem nat.gcd_le_right

added theorem nat.gcd_mul_dvd_mul_gcd

added def nat.prod_dvd_and_dvd_of_dvd_prod