mathlib3

78764375 - refactor(data/real/ennreal): `div_inv_one_monoid` instance (#16689)

refactor(data/real/ennreal): `div_inv_one_monoid` instance (#16689) Add a `div_inv_one_monoid` instance for `ennreal`, so eliminating its `inv_one` and `div_one` lemmas. (Once we have typeclasses for antitone `inv`, more separate `ennreal` lemmas can be eliminated.)