Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-25 05:29 d052c527

View on Github →

feat(order/extension): extend partial order to linear order (#7142) Adds a construction to extend a partial order to a linear order. Also fills in a missing Zorn variant.

Estimated changes