Commit 2023-05-15 10:06 23a970bf

View on Github →

feat: port Order.Category.FrmCat (#3970)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Category/FrmCat.lean

added def FrmCat.Iso.mk

added theorem FrmCat.coe_of

added def FrmCat.of

added def FrmCat

added def topCatOpToFrameCat