Commit 2023-03-21 13:27 d98a95a2

View on Github →

feat: port RingTheory.EuclideanDomain (#3017)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/EuclideanDomain.lean

added theorem EuclideanDomain.dvd_or_coprime

added def EuclideanDomain.gcdMonoid

added theorem EuclideanDomain.gcd_isUnit_iff

added theorem EuclideanDomain.isCoprime_of_dvd

added theorem EuclideanDomain.span_gcd

added theorem gcd_ne_zero_of_left

added theorem gcd_ne_zero_of_right

added theorem left_div_gcd_ne_zero

added theorem right_div_gcd_ne_zero