Commit 2023-06-15 03:07 ac61d012

View on Github →

feat: port Order.Category.BoolAlgCat (#5023)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Category/BoolAlgCat.lean

added def BoolAlgCat.Iso.mk

added theorem BoolAlgCat.coe_of

added theorem BoolAlgCat.coe_toBddDistLatCat

added def BoolAlgCat.dual

added def BoolAlgCat.dualEquiv

added def BoolAlgCat.of

added def BoolAlgCat.toBddDistLatCat

added def BoolAlgCat

added theorem boolAlgCat_dual_comp_forget_to_bddDistLatCat