symmetric monoidal (∞,1)-category of spectra
constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
In the same vein that commutative rings are to integral domains and GCD rings are to GCD domains, Euclidean rings are to Euclidean domains.
A Euclidean ring is a commutative ring for which there exists a function from the multiplicative submonoid of regular elements in to the natural numbers, often called a degree function, such that for all and , there exist such that and either or . There is no uniqueness requirement for .
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 .
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,
Every Euclidean ring is a Bézout ring, and every prefield is an Euclidean ring.
The integers are a 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)
Last revised on June 23, 2024 at 04:01:17. See the history of this page for a list of all contributions to it.