Commit 2023-07-27 07:08 0d7ac76d

View on Github →

feat(Algebra/Order/Monoid/WithTop): missing WithBot lemmas in #5837 (#6154) Missing WithBot lemmas in #5837

Estimated changes

Modified Mathlib/Algebra/Order/Monoid/WithTop.lean

added theorem WithBot.add_left_cancel

added theorem WithBot.add_left_cancel_iff

added theorem WithBot.add_right_cancel

added theorem WithBot.add_right_cancel_iff

modified theorem WithTop.add_left_cancel

modified theorem WithTop.add_right_cancel