Commit 2023-06-16 11:12 a9540a65

View on Github →

feat: port Algebra.Category.BoolRingCat (#5053)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Category/BoolRingCat.lean

added def BoolRingCat.Iso.mk

added theorem BoolRingCat.coe_of

added def BoolRingCat.of

added def BoolRingCat

added def boolRingCatEquivBoolAlgCat

Modified Mathlib/Order/Category/BoolAlgCat.lean