Commit 2024-06-30 14:09 db17c10b

View on Github →

feat(Data/Real/EReal): add inverse and division of ENNReals (#14224) This PR adds API for inverse and division of extended reals.

Estimated changes

added theorem EReal.coe_div
added theorem EReal.coe_inv
added theorem EReal.div_bot
added theorem EReal.div_div
added theorem EReal.div_eq_inv_mul
added theorem EReal.div_mul_cancel
added theorem EReal.div_nonneg
added theorem EReal.div_self
added theorem EReal.div_top
added theorem EReal.div_zero
added theorem EReal.inv_bot
added theorem EReal.inv_inv
added theorem EReal.inv_neg
added theorem EReal.inv_top
added theorem EReal.inv_zero
added theorem EReal.mul_div
added theorem EReal.mul_div_cancel
added theorem EReal.mul_div_right
added theorem EReal.mul_inv
added theorem EReal.sign_mul_inv_abs
added theorem EReal.zero_div