[Agda] factorization monoid, ring

[N. Raghavendra]

At 2016-06-20T14:36:57+04:00, Sergei Meshveliani wrote:

> But I do not find:  where there are implemented the general notions of
> Factorization Monoid or Factorization Ring,
> a notion of factorization uniqueness for such domains, and some generic
> lemmata about them?
> (papers, documentation -- ?)
>
> Can somebody point at such?

In case you are looking for some references on the general theory of
factorial monoids and rings, here are some possible references.  (They
don't say anything about implementation.)

1. N. Jacobson, Basic Algebra, vol. 1, 2nd ed., section 2.14 (Factorial
   monoids and rings).

2. R. Mines, F. Richman, and W. Ruitenberg, A course in constructive
   algebra, Chapter IV, section 1 (Divisibility in cancellation
   monoids).

3. N. Bourbaki, Algebra II, Chapter VI, Section 1 (Ordered groups and
   divisibility).

4. Pete L. Clark, Commutative algebra, notes, Section 15
   (Factorization), http://math.uga.edu/~pete/integral.pdf

Cheers,
Raghu.

--
N. Raghavendra <raghu at hri.res.in>, http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/