Commit 2024-02-04 23:05 cbe30b9e

View on Github →

feat(EuclideanDomain): drop DecidableEq assumptions (#10255)

Estimated changes

Modified Mathlib/RingTheory/EuclideanDomain.lean

modified theorem EuclideanDomain.gcd_isUnit_iff

modified theorem EuclideanDomain.span_gcd