Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-22 08:40 cf7b16a6

View on Github →

chore(algebra/order/monoid): move lemmas (#16176)

  • move with_top.coe_nat to algebra.order.monoid, prove by rfl;
  • move with_top.nat_ne_top and with_top.top_ne_nat to algebra.order.monoid;
  • add with_bot versions.

Estimated changes

added theorem with_bot.bot_ne_nat
added theorem with_bot.coe_nat
added theorem with_bot.nat_ne_bot
added theorem with_top.coe_nat
added theorem with_top.nat_ne_top
added theorem with_top.top_ne_nat
deleted theorem with_top.coe_nat
deleted theorem with_top.nat_ne_top
deleted theorem with_top.top_ne_nat