Defining x/0 as 0 doesn’t break anything mathematically; all the relevant field axioms have an x != 0 hypothesis so this really is undefined behavior.

Moreover, it’s actually pretty common for proof assistants to adopt the x/0 = 0 convention, as it turns a partial function into a total one! Having something like NaN or Inf is definitely a better solution in practice, but x/0 = 0 does have its merits!