Theorem EuclideanDomain.gcd_isUnit_iff

Modification history

2024-02-04 23:05
Mathlib/RingTheory/EuclideanDomain.lean
feat(EuclideanDomain): drop `DecidableEq` assumptions (#10255)
Modified EuclideanDomain.gcd_isUnit_iffView on Github →
2023-07-29 10:38
Mathlib/RingTheory/EuclideanDomain.lean
fix: make EuclideanDomain.gcdMonoid computable (#6076) …
Modified EuclideanDomain.gcd_isUnit_iffView on Github →
2023-03-21 13:27
Mathlib/RingTheory/EuclideanDomain.lean
feat: port RingTheory.EuclideanDomain (#3017)
Added EuclideanDomain.gcd_isUnit_iffView on Github →