So what should i mod 0 really be equal to? There has been a very interesting discussion over in the Mizar mailing list, starting with John Harrison's original post, followed by his superb summary of different choices, and Robert Boyer's response.  The discussion has continued since, but since the archive is only updated daily, you'll have to check back tomorrow to see the rest!

However, I thought that people here too might be interested in this discussion.  I am not sure which definition I prefer, but the ring-theoretical argument that Z/<0> is isomorphic to Z, makes it compelling to define it so that i mod 0 = i (rather than an error).


Please Wait...