Normalization domain: multiplying with norm_unit gives a normal form for associated elements.

GCD domain: an integral domain with normalization and gcd (greatest common divisor) and lcm (least common multiple) operations. In this setting gcd and lcm form a bounded lattice on the associated elements where gcd is the infimum, lcm is the supremum, 1 is bottom, and 0 is top. The type class focuses on gcd and we derive the correpsonding lcm facts from gcd.

ℤ specific version of least common multiple.