[Agda] ¬ 0# ? 1#

[Sergei Meshveliani]

People,
this is a question about Standard library.
I write

module _ {α α=} (R : CommutativeRing α α=)
(open CommutativeRing R using (0#; 1#; ...))
(0≉1 : ¬ 0# ≈ 1#)
...


But probably 0≉1 needs to be an axiom in RingWithOne (and in
CommutativeRing). Is such in Standard library?

Thanks,

------
Sergei

[Sergei Meshveliani]

On Mon, Feb 26, 2018 at 11:06 AM, Sergei Meshveliani <***@botik.ru>
wrote:
[..]

Post by Sergei Meshveliani
I write
module _ {α α=} (R : CommutativeRing α α=)
(open CommutativeRing R using (0#; 1#; ...))
(0≉1 : ¬ 0# ≈ 1#)
...
But probably 0≉1 needs to be an axiom in RingWithOne (and in
CommutativeRing). Is such in Standard library?

But I have looked now into (I) "Algebra" by S.Lang 1968,
and into (II) "Algebra" by Wan Der Waerden.

(I) requires 0 ≉ 1 only starting from Principle Ideal Ring.
(II) requires 0 ≉ 1 only starting from Division Ring.

So that Standard library agrees with these two books,
and RingWithOne does not need to include 0≉1,
and I withdraw my question.

Sorry for noise,

------
Sergei