Commit 2022-11-30 13:42 83871f6c

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 ℝ)).