Commit 2025-01-25 05:58 3a62ce83

View on Github →

feat(Data.Real.EReal): add lemmas about division (#20293) A few more lemmas about division and order/distributivity in EReal.

Estimated changes

added theorem EReal.bot_lt_inv
added theorem EReal.div_eq_iff
added theorem EReal.div_lt_iff
added theorem EReal.inv_lt_top
added theorem EReal.lt_div_iff