Comment on Some Junk Theorems in LeanparentComments−istjohn8moDoesn'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.−Smaug1238moWhat theorem did you use that allowed you to multiply both sides by $0$? (That theorem had conditions on it which you didn't satisfy.)−rnhmjoj8moNo, 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.−orbifold8moI 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.
Comments
Doesn'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.
What theorem did you use that allowed you to multiply both sides by $0$? (That theorem had conditions on it which you didn't satisfy.)
No, 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.
I 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.