ennreal multiplication

Stream: maths

[Sebastien Gouezel]

With the multiplication we have currently on ennreal (a.k.a. the extended reals), the following lemma is proved in the library:

lemma mul_top (x : ereal) (h : x ≠ 0) : x * ⊤ = ⊤ := with_top.mul_top h

Does everyone agree our definition is nonsense for, say, x = -1?

[Kevin Buzzard]

ha ha we were laughing at this very lemma at Xena last Thursday! I'm an algebraist, I don't multiply by infinity, I consider infinity a junk value. If you analysts actually find situations where you want to multiply infinity by -1 then surely go ahead and change it to whatever junk value you want the answer to be :-) Currently the graph of the function is spectacularly discontinuous at x=0, it's like infinity minus the Dirac delta "function".

[Sebastien Gouezel]

When you have +∞ and -∞, even algebraists should agree that the only meaningful answer for (-1) * (+∞) is -∞. Otherwise, negation does not even coincide with multiplication with -1!

[Reid Barton]

You are talking about just ereal and not ennreal, right?

[Sebastien Gouezel]

Yes, it's just for ereal that what we have is nonsense.