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

[N. Raghavendra]

At 2015-03-07T13:10:56+08:00, Dr. ERDI Gergo wrote:

> In more practical terms however, since 0 is not a unit of the
> multiplicative monoid of Nat, so wouldn't your definition allow for 0
> being irreducible?

As I said in my earlier message, this is not relevant because
ultimately, to apply the general theory we need to consider the
multiplicative monoid of non-zero nats.  However, I should've said that,
in any case, 0 is not irreducible by the general definition because
0=0*0, and neither of the two factors 0 and 0 on the right hand side is
a unit in Nat.

Cheers,
Raghu.

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