# mathlibdocumentation

algebra.category.BoolRing

# The category of Boolean rings #

This file defines BoolRing, the category of Boolean rings.

## TODO #

Finish the equivalence with BoolAlg.

def BoolRing  :
Type (u_1+1)

The category of Boolean rings.

Equations
Instances for BoolRing
@[protected, instance]
def BoolRing.has_coe_to_sort  :
(Type u_1)
Equations
@[protected, instance]
Equations
def BoolRing.of (α : Type u_1) [boolean_ring α] :

Construct a bundled BoolRing from a boolean_ring.

Equations
@[simp]
theorem BoolRing.coe_of (α : Type u_1) [boolean_ring α] :
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
@[simp]
@[simp]
theorem BoolRing.has_forget_to_CommRing_forget₂_obj_str_add (ᾰ ᾰ_1 : X.α) :
+ ᾰ_1 = ᾰ_1
@[protected, instance]
Equations
@[simp]
@[simp]
theorem BoolRing.has_forget_to_CommRing_forget₂_obj_str_nsmul (ᾰ : ) (ᾰ_1 : X.α) :
ᾰ_1 = ᾰ_1
@[simp]
theorem BoolRing.has_forget_to_CommRing_forget₂_obj_str_sub (ᾰ ᾰ_1 : X.α) :
- ᾰ_1 = ᾰ_1
@[simp]
theorem BoolRing.has_forget_to_CommRing_forget₂_obj_str_mul (ᾰ ᾰ_1 : X.α) :
* ᾰ_1 = ᾰ_1
@[simp]
theorem BoolRing.has_forget_to_CommRing_forget₂_obj_str_npow (ᾰ : ) (ᾰ_1 : X.α) :
ᾰ_1 = ᾰ_1
@[simp]
@[simp]
theorem BoolRing.has_forget_to_CommRing_forget₂_obj_str_zsmul (ᾰ : ) (ᾰ_1 : X.α) :
ᾰ_1 = ᾰ_1
@[simp]
@[simp]
def BoolRing.iso.mk {α β : BoolRing} (e : α ≃+* β) :
α β

Constructs an isomorphism of Boolean rings from a ring isomorphism between them.

Equations
@[simp]
theorem BoolRing.iso.mk_inv {α β : BoolRing} (e : α ≃+* β) :
@[simp]
theorem BoolRing.iso.mk_hom {α β : BoolRing} (e : α ≃+* β) :

### Equivalence between BoolAlg and BoolRing#

@[protected, instance]
Equations
@[simp]
@[protected, instance]
Equations
@[simp]
@[simp]

The equivalence between Boolean rings and Boolean algebras. This is actually an isomorphism.

Equations