I'm surprised to learn that lean defines the natural number 1/0 as 0.
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.
alt Hacker News
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.