Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-06 01:49 108fa6f3

View on Github →

feat(order/bounded_lattice): min/max commute with coe (#6900) to with_bot and with_top

Estimated changes

added theorem with_bot.coe_max
added theorem with_bot.coe_min
added theorem with_top.coe_max
added theorem with_top.coe_min