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

Dr. ERDI Gergo gergo at erdi.hu
Fri Mar 6 12:17:10 CET 2015


On Fri, 6 Mar 2015, N. Raghavendra wrote:

> Irreducible : ℕ → Set
> Irreducible n = n ≢ 1 × ((x y : ℕ) → n ≡ x * y → x ≡ 1 ⊎ y ≡ 1)
>
> 2. How does one prove the converse of the above implication?

How about something simple & straightforward like this:
https://gist.github.com/gergoerdi/a70e414484a5d0ab97e0


More information about the Agda mailing list