Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-18 20:45 429aaa30

View on Github →

feat(order/bounded_lattice): coe_unbot simp lemma (#9258)

Estimated changes

added theorem with_bot.coe_unbot
added theorem with_top.coe_untop