Commit 2022-09-29 01:02 78764375
View on Github →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.)