YAP (was Re: Proposal: Remove Show and Eq superclasses of Num)

[Paterson, Ross]

Tyson Whitehead writes:
> I see an integral domain is just a commutative ring with no zero divisors (and
> every euclidean domain is also an integral domain)

> http://en.wikipedia.org/wiki/Integral_domain

> If I'm understanding you then this is sufficient structure to tell us that an
> associate and unit decomposition exists, even if we can't compute it.

> I spent sometime last night trying to figure out what about this structure
> guarantees such a decomposition.  I didn't have much luck though.  Any hints?

Units are invertible elements, and two elements are associates if they're
factors of each other.  So association is an equivalence relation; in
particular the associates of 1 are the units, and the only associate of
0 is itself.

Now choose a member from each association equivalence class to be the
canonical associate for all the members of that class, choosing 1 as
the canonical associate for the unit class.  Because there are no zero
divisors, that uniquely determines the canonical unit for each element.