Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2021-12-03 10:55
e0c27fe4
View on Github →
feat(order/bounded_order): a few more
simp
lemmas (
#10533
) Inspired by
#10486
Estimated changes
Modified
src/order/bounded_order.lean
added
theorem
max_eq_bot
added
theorem
max_eq_top
added
theorem
max_top_left
added
theorem
max_top_right
added
theorem
min_bot_left
added
theorem
min_bot_right
added
theorem
min_eq_bot
added
theorem
min_eq_top