Commit 2023-07-29 10:38 e6e9a9e6

View on Github →

fix: make EuclideanDomain.gcdMonoid computable (#6076) This of course still works non-computably in the presence of Classical.decEq, but the caller now has the option.

Estimated changes

modified theorem EuclideanDomain.span_gcd