Def EuclideanDomain.gcdMonoid

Modification history

2023-07-29 10:38

Mathlib/RingTheory/EuclideanDomain.lean

fix: make EuclideanDomain.gcdMonoid computable (#6076) …

Modified EuclideanDomain.gcdMonoid View on Github →

2023-03-21 13:27

Mathlib/RingTheory/EuclideanDomain.lean

feat: port RingTheory.EuclideanDomain (#3017)

Added EuclideanDomain.gcdMonoid View on Github →