Commit 2024-02-12 06:18 fa3313a1

View on Github →

chore: Split off WithTop lemmas (#10239) from Algebra.BigOperators.Order . Add the corresponding WithBot lemmas.

Estimated changes

deleted theorem WithTop.prod_lt_top
deleted theorem WithTop.sum_eq_top_iff
deleted theorem WithTop.sum_lt_top
deleted theorem WithTop.sum_lt_top_iff
added theorem WithBot.bot_lt_sum_iff
added theorem WithBot.coe_sum
added theorem WithBot.prod_lt_bot
added theorem WithBot.sum_eq_bot_iff
added theorem WithBot.sum_lt_bot
added theorem WithTop.coe_sum
added theorem WithTop.prod_lt_top
added theorem WithTop.sum_eq_top_iff
added theorem WithTop.sum_lt_top
added theorem WithTop.sum_lt_top_iff