mathlib

d052c527 - feat(order/extension): extend partial order to linear order (#7142)

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.