Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] The greatest common divisor in the standard library

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] The greatest common divisor in the standard library


chronological Thread 
  • From: Johannes Waldmann <waldmann AT imn.htwk-leipzig.de>
  • To: Andrés Sicard-Ramírez <andres.sicard AT gmail.com>
  • Cc: Coq-Club <coq-club AT pauillac.inria.fr>, Ana Bove <bove AT chalmers.se>, Peter Dybjer <peterd AT cs.chalmers.se>
  • Subject: Re: [Coq-Club] The greatest common divisor in the standard library
  • Date: Thu, 10 Jul 2008 15:04:47 +0200
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1


| b)), however, Zgcd 0 0 = 0 and 0 is not the greatest common divisor of
| 0 and 0

yes it is.

the definition is correct w.r.t. the partial ordering
given by  "x divides y" (= exists z : x * z = y)

there, 0 is the maximal element, because any number divides 0.

this has nothing to do with the usual "<" on numbers.

j.w.


-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2.0.4-svn0 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org

iD8DBQFIdgjvDqiTJ5Q4dm8RAtBAAJ40DTKdfWHRpehLGcwn2DtF+hq4lgCdGiya
g0r+FYgO0GSYcT4+L/yZXpM=
=6UPO
-----END PGP SIGNATURE-----



Archive powered by MhonArc 2.6.16.

Top of Page