Commit 2023-02-25 06:35 357d16b1

View on Github →

feat: add/generalize lemmas about WithTop/WithBot (#2406) Some of these lemmas are generalized from ENNReal while porting Data.Real.ENNReal. Backported to Mathlib 3 in leanprover-community/mathlib#18487, now forward-porting back to Mathlib 4. Also forward-porting leanprover-community/mathlib#18391

Estimated changes

modified theorem WithTop.prod_lt_top
modified theorem WithTop.sum_eq_top_iff
modified theorem WithTop.sum_lt_top
modified theorem WithTop.sum_lt_top_iff
modified theorem WithBot.bot_lt_add
modified theorem WithTop.add_lt_top
added theorem WithBot.bot_lt_mul'
modified theorem WithBot.bot_lt_mul
added theorem WithTop.mul_lt_top'
modified theorem WithTop.mul_lt_top
added theorem WithTop.mul_top'
modified theorem WithTop.mul_top
added theorem WithTop.top_mul'
modified theorem WithTop.top_mul
added theorem WithTop.sub_eq_top_iff
added theorem List.prod_int_mod
added theorem List.prod_nat_mod
added theorem List.sum_int_mod
added theorem List.sum_nat_mod
added theorem WithBot.unbot'_eq_iff
added theorem WithTop.untop'_eq_iff