[Agda] ¬ 0# ? 1#

[Sergei Meshveliani]

On Mon, Feb 26, 2018 at 11:06 AM, Sergei Meshveliani <mechvel at botik.ru>
wrote:
[..]
>        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