The category of Boolean rings #
This file defines BoolRing
, the category of Boolean rings.
TODO #
Finish the equivalence with BoolAlg
.
The category of Boolean rings.
- carrier : Type u
The underlying type.
- booleanRing : BooleanRing ↑self
Instances For
Equations
- BoolRing.instCoeSortType = { coe := BoolRing.carrier }
@[reducible, inline]
Construct a bundled BoolRing
from a BooleanRing
.
Equations
- BoolRing.of α = { carrier := α, booleanRing := inst✝ }
Instances For
Equations
- BoolRing.instInhabited = { default := BoolRing.of PUnit.{?u.2 + 1} }
Equations
- One or more equations did not get rendered due to their size.
instance
BoolRing.instConcreteCategoryRingHomCarrier :
CategoryTheory.ConcreteCategory BoolRing fun (x1 x2 : BoolRing) => ↑x1 →+* ↑x2
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
Equations
- One or more equations did not get rendered due to their size.
@[simp]
@[simp]
Equations
- One or more equations did not get rendered due to their size.
@[simp]
@[simp]
The equivalence between Boolean rings and Boolean algebras. This is actually an isomorphism.
Equations
- One or more equations did not get rendered due to their size.