mathlib3

6bcb12c1 - feat(order/antisymmetrization): Turning a preorder into a partial order (#11728)

feat(order/antisymmetrization): Turning a preorder into a partial order (#11728) Define `antisymmetrization`, the quotient of a preorder by the "less than both ways" relation. This effectively turns a preorder into a partial order, and this operation is functorial as shown by the new `Preorder_to_PartialOrder`.