Mathlib does indeed define the extended real numbers, but they also need to define division on the reals. This is similar to the definition of subtraction having to be done for integers and for naturals (mentioned in the article)

I presume though that Mathlib does not define the extended naturals? If they did then 1:N / 0:N would be valued at this infinity.

What I found interesting about the Scott encoding was that natural infinity was trivial to define, and arises directly from a straightforward construction of the div function (for naturals).

The encoding is as follows (\x indicates lambda abstraction for identifier x. Recursion is assumed, of course it could be made explicit with the Y combinator):

  zero := \f \x n
  succ := \n \f \x f n

  infinite := \n succ (infinite n)
  infinity := infinite zero

  subn := \n \m m (\p n (\q subn q p) n) n

  divn := \n \m (subn m n) (\p zero) (succ (divn (subn n m) m))

  divn (succ zero) zero => infinity

EDIT: Note that infinity does not have a normal form (does not terminate), but:

  subn n infinity => zero

The extended reals can also arise directly from the definition of reals either as Cauchy sequences of rationals (as unbounded increasing sequences, etc) or Dedekind cuts (let the lower cut contain all rationals) :) for reals IIRC the main reason to exclude the extended reals is to make it a field.

However I don't think any of this matters for the point the article made. The problem is not that 1:N/0:N has "nothing sensible" to return, the problem is that if you define it in the way most mathematicians do, a lot of your proofs will be littered with (inline) lemmas showing that the result of such-and-such a division is a finite natural / finite real. This is analogous the problem brought up in the article of having proofs littered with lemmas showing that the result of such-and-such a square root was real.

In fact, there is also a type `enat` in mathlib. However, have `x/y` be a term of a type that is not the type of `x` and `y` comes with it's own sets of problems. It doesn't compose as smoothly as homogeneous division.

> n * inf == inf

I would expert this to be 0 actually.

Why would you want the product of two non-zero values to equal zero?

Among other things, this would have the unpleasant effect of making expressions like "0÷1" undefined, because the result could equal either zero or infinity.

Apologies, I meant for 0 * inf = 0. Since in n * inf n can be 0 the result should be able to be 0.

You are correct - it should indeed be zero (and * can be constructed accordingly)