Obviously a system can define a symbol like "/" as whatever it wants to. But then it isn't what many mathematicians would expect. The Metamath Proof Explorer d

Obviously a system can define a symbol like "/" as whatever it wants to. But then it isn't what many mathematicians would expect. The Metamath Proof Explorer defines "/" so it only has a value if the denominator is a nonzero complex number: http://us.metamath.org/mpeuni/df-div.html http://us.metamath.org/mpeuni/df-div.html You can argue if that is better, but that is a possible choice.