[Merged by Bors] - feat(Data/Real/EReal): add inverse and division of ENNReals

[pitmonticone]

This PR adds API for inverse and division of extended reals.

Co-authored-by: @D-Thomine

---

[github-actions]

PR summary cbbfb55dff

Import changes

No significant changes to the import graph

---

Declarations diff

+ antitone_div_right_of_nonpos
+ bot_div_of_neg_ne_bot
+ bot_div_of_pos_ne_top
+ coe_div
+ coe_inv
+ div_bot
+ div_div
+ div_eq_inv_mul
+ div_le_div_right_of_nonneg
+ div_le_div_right_of_nonpos
+ div_le_iff_le_mul
+ div_lt_div_right_of_neg
+ div_lt_div_right_of_pos
+ div_mul_cancel
+ div_nonneg
+ div_nonneg_of_nonpos_of_nonpos
+ div_nonpos_of_nonneg_of_nonpos
+ div_nonpos_of_nonpos_of_nonneg
+ div_right_distrib_of_nonneg
+ div_self
+ div_top
+ div_zero
+ instance : DivInvMonoid EReal where inv := EReal.inv
+ instance : DivInvOneMonoid EReal
+ instance : Inv (EReal) := ⟨EReal.inv⟩
+ inv
+ inv_bot
+ inv_inv
+ inv_neg
+ inv_neg_of_neg_ne_bot
+ inv_nonneg_of_nonneg
+ inv_nonpos_of_nonpos
+ inv_pos_of_pos_ne_top
+ inv_top
+ inv_zero
+ le_div_iff_mul_le
+ monotone_div_right_of_nonneg
+ mul_div
+ mul_div_cancel
+ mul_div_mul_cancel
+ mul_div_right
+ mul_inv
+ sign_mul_inv_abs
+ sign_mul_inv_abs'
+ strictAnti_div_right_of_neg
+ strictMono_div_right_of_pos
+ top_div_of_neg_ne_bot
+ top_div_of_pos_ne_top
+ zero_div

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

[sgouezel]

It's a bad idea to define a non-homogeneous division on EReal → ENNReal → EReal. Instead, as I discussed with Damien, one should define an homogeneous division on EReal, first be defining an inverse function and then using (a, b) -> a * b⁻¹.

[pitmonticone]

Yes, I believe that is the new API in BET/TopologicalEntropy.

@D-Thomine can you confirm?

[sgouezel]

This looks very good. Minor tweaks are required about the naming of lemmas, though.

[pitmonticone]

I should have addressed all review comments.

Thank you very much @sgouezel for your review!

[sgouezel]

bors r+
Thanks!

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style