Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-11 19:01 e61a4645

View on Github →

feat(ring_theory/euclidean_domain): add more specific Euclidean domain stuff (#527)

Estimated changes

Modified algebra/euclidean_domain.lean

added theorem euclidean_domain.eq_div_of_mul_eq_left

added theorem euclidean_domain.eq_div_of_mul_eq_right

Created ring_theory/euclidean_domain.lean

added theorem dvd_or_coprime

added theorem gcd_is_unit_iff

added theorem is_coprime_of_dvd

added theorem span_gcd