[mizar] gcd(0,0)

[trybulec <trybulec@math.uwb.edu.pl>]

I do not understand problems with divisibility by 0. With the definition
   
     i divides j means ex k st k*i = j

is no problem with saying
   
               0 divides i

in the statement

                0 divides i implies i = 0

Quite often we suppose that gcd(0,0) is undefined. It is true  with the 
high school definition of gcd

         gcd(i,j) divides i &
         gcd(i,j) divides j &
         for k st k divides i & k divides j holds k <= gcd(i,j)

because there is no greatest (wrt <=) natural number.

In lattice theoretic setting the definition is

        gcd(i,j) divides i &
         gcd(i,j) divides j &
         for k st k divides i & k divides j holds k divides gcd(i,j)

and because 0 is the greatest natural number (wrt divides), so gcd(0,0) = 0.

Probably it is nothing new, I would appreciate references.

Best regards,
Andrzej Trybulec