mathlib3

101555b1 - refactor(data/real/ennreal): redefine `ennreal.to_nnreal` in terms of `with_top.untop'` (#15247)

refactor(data/real/ennreal): redefine `ennreal.to_nnreal` in terms of `with_top.untop'` (#15247) * redefine `ennreal.to_nnreal` as `with_top.untop' 0`; * use lambda function instead of `id` for identity coercions of `nat` and `int`; * move `with_top.add_monoid_with_one` and `with_bot.add_monoid_with_one` to `algebra.order.monoid`, add commutative version; * generalize `ennreal.to_nnreal_mul` to `with_top`.