mathlib

83871f6c - chore(data/real/ereal): fix addition and multiplication on ereal (#17770)

chore(data/real/ereal): fix addition and multiplication on ereal (#17770) The current version of multiplication on ereal is completely broken (it satisfies `(-1) * (+∞) = +∞`). The addition is not really broken, but it satisfies `(-∞) + (+∞) = +∞`, while the analogy with ennreal through the exponential and the logarithm suggest that a better convention would be `(-∞) + (+∞) = -∞`. We fix the multiplication (by defining one directly by hand) and tweak the addition to obey the better convention (by changing the definition from `with_top (with_bot ℝ)` to `with_bot (with_top ℝ)`).