Commit 2023-06-16 04:31 bef17213

View on Github →

feat: port Order.Category.FinBoolAlgCat (#5052)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Category/FinBoolAlgCat.lean

added def FinBoolAlgCat.Iso.mk

added theorem FinBoolAlgCat.coe_of

added def FinBoolAlgCat.dual

added def FinBoolAlgCat.dualEquiv

added def FinBoolAlgCat.of

added structure FinBoolAlgCat

added theorem finBoolAlgCat_dual_comp_forget_to_finBddDistLatCat

added def fintypeToFinBoolAlgCatOp

Modified Mathlib/Order/Hom/Lattice.lean