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
Comments
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://www.hillelwayne.com/post/divide-by-zero/
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.
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