Showing changes from revision #2 to #3:
Added | Removed | Changed
Let be a discrete integral domain, and let us define the type family as
The type family is by definition a predicate, and can be proven to be a (0,1)-precategory. is a discrete GCD domain if is a finitely complete (0,1)-precategory.
Last revised on June 13, 2022 at 01:01:17. See the history of this page for a list of all contributions to it.