Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-02-02 01:41 6925e4dc

View on Github →

feat(algebra/euclidean_domain): lcm (#665)

Estimated changes

Modified src/algebra/euclidean_domain.lean

added theorem euclidean_domain.dvd_lcm_left

added theorem euclidean_domain.dvd_lcm_right

added theorem euclidean_domain.gcd_mul_lcm

added def euclidean_domain.lcm

added theorem euclidean_domain.lcm_dvd

added theorem euclidean_domain.lcm_dvd_iff

added theorem euclidean_domain.lcm_eq_zero_iff

added theorem euclidean_domain.lcm_zero_left

added theorem euclidean_domain.lcm_zero_right