One could posit, instead of the property that for all and , there exist such that and either or ; that the commutative ring has the structure of a function called the division function, and a function called the remainder function, such that for all and , and either or . There might be multiple such division and remainder functions for the commutative ring .
One could also add the requirement that for all nonzero . There is no loss of generality in assuming it; every Euclidean ring admits such a degree function , defining .
In constructive mathematics
The definition of the Euclidean ring further bifurcates in constructive mathematics due to the disjunctive condition above. These statements, which are equivalent in the presence of excluded middle, include:
or equivalently,
Properties
Every Euclidean ring is a Bézout ring, and every prefield is an Euclidean ring.
A classical Euclidean domain is a Euclidean ring where is the multiplicative monoid of elements not equal to zero (where inequality is denial inequality)
A Heyting Euclidean domain is a Euclidean ring where is the multiplicative monoid of elements apart from zero
An ordered Euclidean domain is a Euclidean ring where is the multiplicative monoid of elements with a positive absolute value