Commit 2022-12-09 06:47 a88ea9ca

View on Github →

feat: port Algebra.Order.Monoid.WithTop (#902) mathlib3: 655994e298904d7e5bbd1e18c95defd7b543eb94

  • depends on #910 Not too bad. Mostly renaming instances and a few broken proofs. Things to double-check (all marked with Porting note):
  • lift is not implemented yet, I replaced it with induction.
  • In addSemigroup I didn't get repeat or repeat' to work. That could be golfed.
  • In WithTop.addHom the anonymous constructor didn't work, but writing it out, it did. Is that expected?
  • I'm a bit unsure about coersions. I left in most things and removed (commented out) the lemma coe_coe_add_hom. Could be worth gleaming over anything that has coe in it's name.

Estimated changes

added theorem WithBot.add_bot
added theorem WithBot.add_eq_bot
added theorem WithBot.add_eq_coe
added theorem WithBot.add_ne_bot
added theorem WithBot.bot_add
added theorem WithBot.bot_lt_add
added theorem WithBot.bot_ne_nat
added theorem WithBot.coe_add
added theorem WithBot.coe_eq_one
added theorem WithBot.coe_lt_one
added theorem WithBot.coe_nat
added theorem WithBot.coe_one
added theorem WithBot.nat_ne_bot
added theorem WithBot.one_lt_coe
added def WithTop.addHom
added theorem WithTop.add_eq_coe
added theorem WithTop.add_eq_top
added theorem WithTop.add_lt_top
added theorem WithTop.add_ne_top
added theorem WithTop.add_top
added theorem WithTop.coe_add
added theorem WithTop.coe_eq_one
added theorem WithTop.coe_lt_one
added theorem WithTop.coe_nat
added theorem WithTop.coe_one
added theorem WithTop.nat_ne_top
added theorem WithTop.one_eq_coe
added theorem WithTop.one_lt_coe
added theorem WithTop.one_ne_top
added theorem WithTop.top_add
added theorem WithTop.top_ne_nat
added theorem WithTop.top_ne_one
added theorem WithTop.zero_lt_coe
added theorem WithTop.zero_lt_top