Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-28 23:50 c058607c

View on Github →

chore(order): generalize min_top_left (#10486) As well as its relative min_top_right. Also provide max_bot_(left|right).

Estimated changes

Modified src/algebra/order/monoid.lean

deleted theorem min_top_left

deleted theorem min_top_right

Modified src/order/bounded_order.lean

added theorem max_bot_left

added theorem max_bot_right

added theorem min_top_left

added theorem min_top_right