Let RR be a discrete integral domain, and let us define the type family (−)|(−)(-)\vert(-) as
The type family is by definition a predicate, and RR can be proven to be a (0,1)-precategory. RR is a discrete GCD domain if (R,|)(R, \vert) is a finitely complete (0,1)-precategory.
Revision on May 2, 2022 at 18:14:58 by Anonymous?. See the history of this page for a list of all contributions to it.