Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-08 04:07 7fbadc69

View on Github →

chore(order/basic): move Prop.partial_order to order/basic (#15884) This ensures, among other things, that r ≤ s is almost always available as notation for subrelations. We don't move Prop.linear_order since doing so means we need to manually prove or = max_default and and = min_default.

Estimated changes