Commit 2023-01-06 13:36 724f91b0

View on Github →

feat: port Algebra.Order.Ring.WithTop (#976)

Estimated changes

added theorem WithBot.bot_lt_mul
added theorem WithBot.bot_mul
added theorem WithBot.bot_mul_bot
added theorem WithBot.coe_mul
added theorem WithBot.mul_bot
added theorem WithBot.mul_coe
added theorem WithBot.mul_def
added theorem WithBot.mul_eq_bot_iff
added theorem WithTop.coe_mul
added theorem WithTop.mul_coe
added theorem WithTop.mul_def
added theorem WithTop.mul_eq_top_iff
added theorem WithTop.mul_lt_top
added theorem WithTop.mul_top
added theorem WithTop.top_mul
added theorem WithTop.top_mul_top