Commit 2023-06-14 21:27 fc5d0810

View on Github →

feat: port Order.Category.HeytAlgCat (#5021)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Category/Ring/Basic.lean

Modified Mathlib/MeasureTheory/Category/MeasCat.lean

Modified Mathlib/Order/Category/DistLatCat.lean

Modified Mathlib/Order/Category/FrmCat.lean

Created Mathlib/Order/Category/HeytAlgCat.lean

added def HeytAlgCat.Iso.mk

added theorem HeytAlgCat.coe_of

added def HeytAlgCat.of

added def HeytAlgCat

Modified Mathlib/Order/Category/LinOrdCat.lean

Modified Mathlib/Order/Category/NonemptyFinLinOrdCat.lean

Modified Mathlib/Order/Category/PartOrdCat.lean

Modified Mathlib/Order/Category/PreordCat.lean

Modified Mathlib/Order/Heyting/Hom.lean

Modified Mathlib/Topology/Category/TopCat/Basic.lean