Just FTR, the same practical decision was taken in the Coq standard library. The functions have to be total so the options were using an option type (equivalent of Maybe) or a default value. Note that it could have been any value but zero is just the most natural. This doesn’t break any standard mathematical theorems because all these theorems already have to include a precondition that the denominator is nonzero (whether there is a default value or the division by zero is undefined).
2 Likes