4 ms·
I'm surprised to learn that lean defines the natural number 1/0 as 0.
by bjt12345 10mo ago
I'm surprised to learn that lean defines the natural number 1/0 as 0.
- istjohn 10mo agoDoesn't this allow one to prove x=y for any x, y? x/0 = x(1/0) = x*0 = 0, so x/0 = 0 for all x. So x/0 = y/0. Multiply both sides by 0: x = y.
- deleted 10mo ago[deleted]
- deleted 10mo ago[deleted]
- rnhmjoj 10mo agoNo, because x/y is just an arbitrary operation between x and y. Here you're assuming that 1/x is the inverse of x under *, but it's not.
- orbifold 10mo agoI mean in a normal math curriculum you would define only the multiplicative inverse and then there is a separate way to define fraction, if you start out with certain rings. It is kind of surprising to me that they did a lazy definition of division.
- Smaug123 10mo agoWhat theorem did you use that allowed you to multiply both sides by $0$? (That theorem had conditions on it which you didn't satisfy.)
- zodiac 10mo agoHere’s a good document defending the merits of this design. https://xenaproject.wordpress.com/2020/07/05/division-by-zero-in-type-theory-a-faq/ https://xenaproject.wordpress.com/2020/07/05/division-by-zer...