Commit 2023-04-05 14:47 e54ba225

View on Github →

feat: port Order.Category.LinOrd (#3281)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Category/LinOrdCat.lean

added def LinOrdCat.Iso.mk

added theorem LinOrdCat.coe_of

added def LinOrdCat.dual

added def LinOrdCat.dualEquiv

added def LinOrdCat.of

added def LinOrdCat

added theorem linOrdCat_dual_comp_forget_to_latCat