3 ms·

Yes, but to make this "self-consistent" 0 * 0 = 1 would need to hold. And I'm totally sure that they don't have that...

• librexpr 3y ago
  ((x / y) * y) = x is not a true statement about real numbers, regardless of if division by zero is defined as an error or as being equal to 0. The true statement is ( y != 0 -> ((x / y) * y) = x ), and this holds no matter how you define division by zero. More generally, in normal math, every theorem that involves division by some value Y which could be zero must have as hypothesis that Y is not equal to zero. All these theorems still work in systems like Lean where division by zero is defined to be zero, so nothing is lost.