Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-05 09:10 93451afd

View on Github →

feat(order/category/BoolAlg): The category of Boolean algebras (#12452) Define BoolAlg, the category of Boolean algebras with bounded lattice homs.

Estimated changes

Modified src/order/boolean_algebra.lean

Created src/order/category/BoolAlg.lean

added def BoolAlg.dual

added def BoolAlg.dual_equiv

added def BoolAlg.iso.mk

added def BoolAlg.of

added def BoolAlg.to_BoundedDistribLattice

added def BoolAlg

added theorem BoolAlg_dual_comp_forget_to_BoundedDistribLattice