Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-02-24 15:00 afdb4fa3

View on Github →

feat(*/with_top): add lemmas about with_top/with_bot (#18487) Backport leanprover-community/mathlib4#2406

Estimated changes

modified theorem with_top.prod_lt_top
modified theorem with_top.sum_eq_top_iff
modified theorem with_top.sum_lt_top
modified theorem with_top.sum_lt_top_iff
modified theorem with_bot.bot_lt_add
modified theorem with_top.add_lt_top
added theorem with_bot.bot_lt_mul'
modified theorem with_bot.bot_lt_mul
modified theorem with_bot.mul_eq_bot_iff
modified theorem with_top.coe_mul
modified theorem with_top.mul_eq_top_iff
added theorem with_top.mul_lt_top'
modified theorem with_top.mul_lt_top
added theorem with_top.mul_top'
modified theorem with_top.mul_top
added theorem with_top.top_mul'
modified theorem with_top.top_mul
modified theorem ennreal.mul_eq_mul_left
modified theorem ennreal.mul_le_mul_left
modified theorem ennreal.mul_lt_mul_left
added theorem with_bot.unbot'_eq_iff
added theorem with_top.untop'_eq_iff