[Agda] Re: Data.Nat.Primality.Prime and irreducibility

[Sergei Meshveliani]

On Sun, 2015-03-08 at 01:23 +0530, N. Raghavendra wrote:
> At 2015-03-07T18:55:53+04:00, Sergei Meshveliani wrote:
> 
> >> A lot of the basic stuff about divisibility, irreducibility, primality,
> >> coprimality, gcd, lcm, etc., can be done for cancellative commutative
> >> monoids, as in, e.g., Jacobson's Basic Algebra, vol. 1, section 2.14
> >> (Factorial monoids and rings).  I think it'd be nice to have that
> >> generality in stdlib.
> >> 
> >> []
> >
> > 1) Consider the ring  R = Integer/(6)   (Integer modulo 6).
> > It has CommutativeMonoid for _*_,  and CommutativeSemiring  too.
> > According to the above suggestions, we have 
> >
> >   [2] ≈ [2] * [4]   in R.   
> >
> > So [2] occurs reducible in R, is has "reduced" to the two non-unit
> > factors:  [2] and [4].
> >
> > This definition looks counter-intuitive.
> 
> Dunno if that's counter-intuitive.  Anyway, I only said that the basic
> theory of divisibility, gcd, etc., goes through for any cancellative
> commutative monoid.  The multiplicative monoid of the ring Z/6Z isn't
> cancellative.

Sorry, I have missed the word `cancellative'.
All right, I am ready to believe that primality has sense in any
cancellative commutative monoid 
(though I am not, personally, ready to develop the corresponding generic
algorithms for the factorization structures in such monoids).

> > 2) to add the condition   ¬0 : ¬ n ≈ #0  to the definition if
> > irreducibility.
> 
> You don't need to add that condition in an integral domain.  It follows
> from the other one because 0=0*0, and neither of the factors 0 and 0 on
> the right hand side is a unit, because an integral domain is non-zero by
> definition.

Indeed! Thank you. I need to remove this part from my definition.

Thanks,

------
Sergei