Commit 2025-02-21 15:07 3faeb592

View on Github →

chore(Algebra/Order/Monoid/Unbundled/WithTop): golf, clean up (#22109)

  • Shorten proofs
  • Make the WithBot and WithTop sections analogous
  • Avoid relying on the defeq (WithTop α)ᵒᵈ = WithBot αᵒᵈ
  • Pull more implicit variables to variable statements
  • Stick to the convention that a b : α and x y : WithBot α This is a follow-up to #21274.

Estimated changes

modified theorem WithBot.add_bot
modified theorem WithBot.add_coe_eq_bot_iff
modified theorem WithBot.add_eq_bot
modified theorem WithBot.add_eq_coe
modified theorem WithBot.add_left_cancel
added theorem WithBot.add_left_inj
modified theorem WithBot.add_ne_bot
modified theorem WithBot.add_right_cancel
added theorem WithBot.add_right_inj
modified theorem WithBot.bot_add
modified theorem WithBot.bot_lt_add
modified theorem WithBot.coe_add
modified theorem WithBot.coe_add_eq_bot_iff
modified theorem WithTop.add_coe_eq_top_iff
modified theorem WithTop.add_eq_top
modified theorem WithTop.add_left_cancel
added theorem WithTop.add_left_inj
modified theorem WithTop.add_lt_top
modified theorem WithTop.add_ne_top
modified theorem WithTop.add_right_cancel
added theorem WithTop.add_right_inj
modified theorem WithTop.add_top
modified theorem WithTop.coe_add_eq_top_iff
modified theorem WithTop.top_add