Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-01-06 13:36
724f91b0
View on Github →
feat: port Algebra.Order.Ring.WithTop (
#976
)
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/Algebra/Order/Ring/WithTop.lean
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
added
theorem
WithTop.untop'_zero_mul