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 }
Equations
- BoolRing.instInhabited = { default := BoolRing.of PUnit.{?u.3 + 1} }
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.
Constructs an isomorphism of Boolean rings from a ring isomorphism between them.
Equations
- BoolRing.Iso.mk e = { hom := { hom := ↑e }, inv := { hom := ↑e.symm }, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
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.
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.