Commit 2024-02-06 19:27 0174e788

View on Github →

feat: Make the coercion ℝ≥0 → ℝ≥0∞ commute defeqly with nsmul and pow (#10225) by tweaking the definition of the AddMonoid and MonoidWithZero instances for WithTop. Also unprotect ENNReal.coe_injective and rename ENNReal.coe_eq_coe → ENNReal.coe_inj. From LeanAPAP

Estimated changes

modified theorem WithTop.coe_nsmul
added theorem WithBot.bot_mul'
modified theorem WithBot.bot_mul
modified theorem WithBot.bot_mul_bot
modified theorem WithBot.coe_mul
added theorem WithBot.coe_pow
added theorem WithBot.mul_bot'
modified theorem WithBot.mul_bot
deleted theorem WithBot.mul_coe
modified theorem WithBot.mul_def
modified theorem WithBot.mul_eq_bot_iff
modified theorem WithTop.coe_mul
added theorem WithTop.coe_pow
deleted theorem WithTop.mul_coe
modified theorem WithTop.mul_def
modified theorem WithTop.mul_eq_top_iff
modified theorem WithTop.mul_top'
modified theorem WithTop.mul_top
modified theorem WithTop.top_mul'
modified theorem WithTop.top_mul
modified theorem WithTop.top_mul_top
modified theorem WithTop.untop'_zero_mul
added theorem ENNReal.rpow_int_cast
added theorem ENNReal.rpow_inv_rpow
modified theorem ENNReal.rpow_left_injective
added theorem ENNReal.rpow_rpow_inv
modified theorem ENNReal.coe_add
deleted theorem ENNReal.coe_eq_coe
modified theorem ENNReal.coe_eq_one
modified theorem ENNReal.coe_eq_zero
added theorem ENNReal.coe_inj
added theorem ENNReal.coe_injective
modified theorem ENNReal.coe_mul
added theorem ENNReal.coe_ne_coe
added theorem ENNReal.coe_ne_one
modified theorem ENNReal.coe_ne_zero
added theorem ENNReal.coe_nsmul
added theorem ENNReal.coe_pow
modified theorem ENNReal.one_eq_coe
modified theorem ENNReal.zero_eq_coe
deleted theorem ENNReal.coe_pow
modified theorem ENat.coe_mul
modified theorem WithBot.coe_unbot
added def WithBot.map₂
added theorem WithBot.map₂_coe_coe
modified def WithBot.unbot
modified theorem WithTop.coe_untop
added def WithTop.map₂
added theorem WithTop.map₂_coe_coe
modified def WithTop.untop