Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-27 07:02 d36a67c7

View on Github →

feat(ring_theory/euclidean_domain): generalize lemmas to PIDs (#10324) This moves the existing lemmas to the euclidean_domain namespace.

Estimated changes

Modified src/data/polynomial/field_division.lean

Modified src/field_theory/separable.lean

Modified src/ring_theory/euclidean_domain.lean

deleted theorem dvd_or_coprime

added theorem euclidean_domain.dvd_or_coprime

added theorem euclidean_domain.gcd_is_unit_iff

added def euclidean_domain.gcd_monoid

added theorem euclidean_domain.is_coprime_of_dvd

added theorem euclidean_domain.span_gcd

deleted theorem gcd_is_unit_iff

deleted theorem is_coprime_of_dvd

deleted theorem span_gcd

Modified src/ring_theory/principal_ideal_domain.lean

added theorem dvd_or_coprime

added theorem gcd_is_unit_iff

added theorem is_coprime_of_dvd

added theorem span_gcd