3 ms·

The standard arithmetic classes of Isabelle/HOL show that you can extend division with the equation `x / 0 = 0` and things (seemingly) work out. https://lawren

The standard arithmetic classes of Isabelle/HOL show that you can extend division with the equation `x / 0 = 0` and things (seemingly) work out. https://lawrencecpaulson.github.io/2021/12/01/Undefined.html https://lawrencecpaulson.github.io/2021/12/01/Undefined.html https://www.hillelwayne.com/post/divide-by-zero/ https://www.hillelwayne.com/post/divide-by-zero/ 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... You'll need to do some thinking/proof to find out if it works for you.

JonChesterfield 3y ago
Huh. That's surprising but quite persuasive, thank you for the references. I like the general view that a non-axiomatic divide can't introduce unsoundness so define it however is useful. It has somewhat kicked the can down the road to defining the multiplicative inverse, but that's still a good step forward. Thank you