[Agda] factorization monoid, ring

[Andreas Abel]

Maybe you could ask this question on the Coq mailing list, if you 
haven't done so already. --Andreas

On 20.06.2016 12:36, Sergei Meshveliani wrote:
> People,
>
> I have fully implemented in Agda
>
> 1) the notion of Factorization Monoid (for a commutative cancellative
> monoid)
> (as Raghu mentioned last year),
>
> 2) the notion of Factorization Ring,
> 3) the notion factorization uniqueness for such domains,
> 4) proofs for many lemmata which relate these notions to each other, and
> to factorization in a multiplicative monoid of Nat and Integer,
>
> 5) factorization by the sieve method for Nat (with a proof).
>
> It remains to revise a manual (many types and modules have changed) and
> to put on the Web the library DoCon-A 0.04 which includes this.
>
>
> And I need to compare my approach to what it is done in  Coq
>                                                           ----
>
> with respect to this particular subject -- papers, documentation for
> various libraries, not necessarily standard library.
>
> I observe on the Web a couple of libraries in Coq related to
> 1) a general algebraic hierarchy (Monoid, Ring, etc),
> 2) advanced algorithms for factoring integer numbers, and such.
>
> 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?
>
> Thanks,
>
> ------
> Sergei
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/