Re:Division by zero in type theory: a FAQ
by leanuser57 on Tuesday July 07, 2020 @12:29AM
(#23755702)
Here is a "nonsense" theorem that is provable in Lean:
“There exists a real number r such that 1/r = 0.”
If you try to translate this theorem into maths, you will run into trouble at some point. At which point exactly depends on how you want to make things precise... which is exactly what mathematicians avoid when talking about division in fields.
“There exists a real number r such that 1/r = 0.”
If you try to translate this theorem into maths, you will run into trouble at some point. At which point exactly depends on how you want to make things precise... which is exactly what mathematicians avoid when talking about division in fields.