# Documentation

Mathlib.Algebra.Ring.BooleanRing

# Boolean rings #

A Boolean ring is a ring where multiplication is idempotent. They are equivalent to Boolean algebras.

## Main declarations #

• BooleanRing: a typeclass for rings where multiplication is idempotent.
• BooleanRing.toBooleanAlgebra: Turn a Boolean ring into a Boolean algebra.
• BooleanAlgebra.toBooleanRing: Turn a Boolean algebra into a Boolean ring.
• AsBoolAlg: Type-synonym for the Boolean algebra associated to a Boolean ring.
• AsBoolRing: Type-synonym for the Boolean ring associated to a Boolean algebra.

## Implementation notes #

We provide two ways of turning a Boolean algebra/ring into a Boolean ring/algebra:

• Instances on the same type accessible in locales BooleanAlgebraOfBooleanRing and BooleanRingOfBooleanAlgebra.
• Type-synonyms AsBoolAlg and AsBoolRing.

At this point in time, it is not clear the first way is useful, but we keep it for educational purposes and because it is easier than dealing with ofBoolAlg/toBoolAlg/ofBoolRing/toBoolRing explicitly.

## Tags #

boolean ring, boolean algebra

class BooleanRing (α : Type u_4) extends :
Type u_4
• add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : αα
• nsmul_zero : ∀ (x : α), = 0
• nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) x = x +
• add_comm : ∀ (a b : α), a + b = b + a
• mul : ααα
• left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
• right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
• zero_mul : ∀ (a : α), 0 * a = 0
• mul_zero : ∀ (a : α), a * 0 = 0
• mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
• one : α
• one_mul : ∀ (a : α), 1 * a = a
• mul_one : ∀ (a : α), a * 1 = a
• natCast : α
• natCast_zero :
• natCast_succ : ∀ (n : ), NatCast.natCast (n + 1) =
• npow : αα
• npow_zero : ∀ (x : α), = 1
• npow_succ : ∀ (n : ) (x : α), Semiring.npow (n + 1) x = x *
• neg : αα
• sub : ααα
• sub_eq_add_neg : ∀ (a b : α), a - b = a + -b
• zsmul : αα
• zsmul_zero' : ∀ (a : α), = 0
• zsmul_succ' : ∀ (n : ) (a : α), Ring.zsmul () a = a + Ring.zsmul () a
• zsmul_neg' : ∀ (n : ) (a : α), = -Ring.zsmul (↑()) a
• add_left_neg : ∀ (a : α), -a + a = 0
• intCast : α
• intCast_ofNat : ∀ (n : ), = n
• intCast_negSucc : ∀ (n : ), = -↑(n + 1)
• mul_self : ∀ (a : α), a * a = a

Multiplication in a boolean ring is idempotent.

A Boolean ring is a ring where multiplication is idempotent.

Instances
@[simp]
theorem mul_self {α : Type u_1} [] (a : α) :
a * a = a
@[simp]
theorem add_self {α : Type u_1} [] (a : α) :
a + a = 0
@[simp]
theorem neg_eq {α : Type u_1} [] (a : α) :
-a = a
theorem add_eq_zero' {α : Type u_1} [] (a : α) (b : α) :
a + b = 0 a = b
@[simp]
theorem mul_add_mul {α : Type u_1} [] (a : α) (b : α) :
a * b + b * a = 0
@[simp]
theorem sub_eq_add {α : Type u_1} [] (a : α) (b : α) :
a - b = a + b
@[simp]
theorem mul_one_add_self {α : Type u_1} [] (a : α) :
a * (1 + a) = 0
instance BooleanRing.toCommRing {α : Type u_1} [] :

### Turning a Boolean ring into a Boolean algebra #

def AsBoolAlg (α : Type u_4) :
Type u_4

Type synonym to view a Boolean ring as a Boolean algebra.

Instances For
def toBoolAlg {α : Type u_1} :
α

The "identity" equivalence between AsBoolAlg α and α.

Instances For
def ofBoolAlg {α : Type u_1} :
α

The "identity" equivalence between α and AsBoolAlg α.

Instances For
@[simp]
theorem toBoolAlg_symm_eq {α : Type u_1} :
toBoolAlg.symm = ofBoolAlg
@[simp]
theorem ofBoolAlg_symm_eq {α : Type u_1} :
ofBoolAlg.symm = toBoolAlg
@[simp]
theorem toBoolAlg_ofBoolAlg {α : Type u_1} (a : ) :
toBoolAlg (ofBoolAlg a) = a
@[simp]
theorem ofBoolAlg_toBoolAlg {α : Type u_1} (a : α) :
ofBoolAlg (toBoolAlg a) = a
theorem toBoolAlg_inj {α : Type u_1} {a : α} {b : α} :
toBoolAlg a = toBoolAlg b a = b
theorem ofBoolAlg_inj {α : Type u_1} {a : } {b : } :
ofBoolAlg a = ofBoolAlg b a = b
instance instInhabitedAsBoolAlg {α : Type u_1} [] :
def BooleanRing.sup {α : Type u_1} [] :
Sup α

The join operation in a Boolean ring is x + y + x * y.

Instances For
def BooleanRing.inf {α : Type u_1} [] :
Inf α

The meet operation in a Boolean ring is x * y.

Instances For
theorem BooleanRing.sup_comm {α : Type u_1} [] (a : α) (b : α) :
a b = b a
theorem BooleanRing.inf_comm {α : Type u_1} [] (a : α) (b : α) :
a b = b a
theorem BooleanRing.sup_assoc {α : Type u_1} [] (a : α) (b : α) (c : α) :
a b c = a (b c)
theorem BooleanRing.inf_assoc {α : Type u_1} [] (a : α) (b : α) (c : α) :
a b c = a (b c)
theorem BooleanRing.sup_inf_self {α : Type u_1} [] (a : α) (b : α) :
a a b = a
theorem BooleanRing.inf_sup_self {α : Type u_1} [] (a : α) (b : α) :
a (a b) = a
theorem BooleanRing.le_sup_inf_aux {α : Type u_1} [] (a : α) (b : α) (c : α) :
(a + b + a * b) * (a + c + a * c) = a + b * c + a * (b * c)
theorem BooleanRing.le_sup_inf {α : Type u_1} [] (a : α) (b : α) (c : α) :
(a b) (a c) (a b c) = a b c

The Boolean algebra structure on a Boolean ring.

The data is defined so that:

• a ⊔ b unfolds to a + b + a * b
• a ⊓ b unfolds to a * b
• a ≤ b unfolds to a + b + a * b = b
• ⊥ unfolds to 0
• ⊤ unfolds to 1
• aᶜ unfolds to 1 + a
• a \ b unfolds to a * (1 + b)
Instances For
instance instBooleanAlgebraAsBoolAlg {α : Type u_1} [] :
@[simp]
theorem ofBoolAlg_top {α : Type u_1} [] :
ofBoolAlg = 1
@[simp]
theorem ofBoolAlg_bot {α : Type u_1} [] :
ofBoolAlg = 0
@[simp]
theorem ofBoolAlg_sup {α : Type u_1} [] (a : ) (b : ) :
ofBoolAlg (a b) = ofBoolAlg a + ofBoolAlg b + ofBoolAlg a * ofBoolAlg b
@[simp]
theorem ofBoolAlg_inf {α : Type u_1} [] (a : ) (b : ) :
ofBoolAlg (a b) = ofBoolAlg a * ofBoolAlg b
@[simp]
theorem ofBoolAlg_compl {α : Type u_1} [] (a : ) :
ofBoolAlg a = 1 + ofBoolAlg a
@[simp]
theorem ofBoolAlg_sdiff {α : Type u_1} [] (a : ) (b : ) :
ofBoolAlg (a \ b) = ofBoolAlg a * (1 + ofBoolAlg b)
@[simp]
theorem ofBoolAlg_symmDiff {α : Type u_1} [] (a : ) (b : ) :
ofBoolAlg (a b) = ofBoolAlg a + ofBoolAlg b
@[simp]
theorem ofBoolAlg_mul_ofBoolAlg_eq_left_iff {α : Type u_1} [] {a : } {b : } :
ofBoolAlg a * ofBoolAlg b = ofBoolAlg a a b
@[simp]
theorem toBoolAlg_zero {α : Type u_1} [] :
toBoolAlg 0 =
@[simp]
theorem toBoolAlg_one {α : Type u_1} [] :
toBoolAlg 1 =
@[simp]
theorem toBoolAlg_mul {α : Type u_1} [] (a : α) (b : α) :
toBoolAlg (a * b) = toBoolAlg a toBoolAlg b
@[simp]
theorem toBoolAlg_add_add_mul {α : Type u_1} [] (a : α) (b : α) :
toBoolAlg (a + b + a * b) = toBoolAlg a toBoolAlg b
@[simp]
theorem toBoolAlg_add {α : Type u_1} [] (a : α) (b : α) :
toBoolAlg (a + b) = toBoolAlg a toBoolAlg b
@[simp]
theorem RingHom.asBoolAlg_toLatticeHom_toSupHom_toFun {α : Type u_1} {β : Type u_2} [] [] (f : α →+* β) :
∀ (a : ), ().toLatticeHom.toSupHom a = (toBoolAlg f ofBoolAlg) a
def RingHom.asBoolAlg {α : Type u_1} {β : Type u_2} [] [] (f : α →+* β) :

Turn a ring homomorphism from Boolean rings α to β into a bounded lattice homomorphism from α to β considered as Boolean algebras.

Instances For
@[simp]
theorem RingHom.asBoolAlg_id {α : Type u_1} [] :
@[simp]
theorem RingHom.asBoolAlg_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] (g : β →+* γ) (f : α →+* β) :

### Turning a Boolean algebra into a Boolean ring #

def AsBoolRing (α : Type u_4) :
Type u_4

Type synonym to view a Boolean ring as a Boolean algebra.

Instances For
def toBoolRing {α : Type u_1} :
α

The "identity" equivalence between AsBoolRing α and α.

Instances For
def ofBoolRing {α : Type u_1} :
α

The "identity" equivalence between α and AsBoolRing α.

Instances For
@[simp]
theorem toBoolRing_symm_eq {α : Type u_1} :
toBoolRing.symm = ofBoolRing
@[simp]
theorem ofBoolRing_symm_eq {α : Type u_1} :
ofBoolRing.symm = toBoolRing
@[simp]
theorem toBoolRing_ofBoolRing {α : Type u_1} (a : ) :
toBoolRing (ofBoolRing a) = a
@[simp]
theorem ofBoolRing_toBoolRing {α : Type u_1} (a : α) :
ofBoolRing (toBoolRing a) = a
theorem toBoolRing_inj {α : Type u_1} {a : α} {b : α} :
toBoolRing a = toBoolRing b a = b
theorem ofBoolRing_inj {α : Type u_1} {a : } {b : } :
ofBoolRing a = ofBoolRing b a = b
instance instInhabitedAsBoolRing {α : Type u_1} [] :
@[reducible]

Every generalized Boolean algebra has the structure of a non unital commutative ring with the following data:

• a + b unfolds to a ∆ b (symmetric difference)
• a * b unfolds to a ⊓ b
• -a unfolds to a
• 0 unfolds to ⊥
Instances For
@[reducible]

Every Boolean algebra has the structure of a Boolean ring with the following data:

• a + b unfolds to a ∆ b (symmetric difference)
• a * b unfolds to a ⊓ b
• -a unfolds to a
• 0 unfolds to ⊥
• 1 unfolds to ⊤
Instances For
instance instBooleanRingAsBoolRing {α : Type u_1} [] :
@[simp]
theorem ofBoolRing_zero {α : Type u_1} [] :
ofBoolRing 0 =
@[simp]
theorem ofBoolRing_one {α : Type u_1} [] :
ofBoolRing 1 =
@[simp]
theorem ofBoolRing_neg {α : Type u_1} [] (a : ) :
ofBoolRing (-a) = ofBoolRing a
@[simp]
theorem ofBoolRing_add {α : Type u_1} [] (a : ) (b : ) :
ofBoolRing (a + b) = ofBoolRing a ofBoolRing b
@[simp]
theorem ofBoolRing_sub {α : Type u_1} [] (a : ) (b : ) :
ofBoolRing (a - b) = ofBoolRing a ofBoolRing b
@[simp]
theorem ofBoolRing_mul {α : Type u_1} [] (a : ) (b : ) :
ofBoolRing (a * b) = ofBoolRing a ofBoolRing b
@[simp]
theorem ofBoolRing_le_ofBoolRing_iff {α : Type u_1} [] {a : } {b : } :
ofBoolRing a ofBoolRing b a * b = a
@[simp]
theorem toBoolRing_bot {α : Type u_1} [] :
toBoolRing = 0
@[simp]
theorem toBoolRing_top {α : Type u_1} [] :
toBoolRing = 1
@[simp]
theorem toBoolRing_inf {α : Type u_1} [] (a : α) (b : α) :
toBoolRing (a b) = toBoolRing a * toBoolRing b
@[simp]
theorem toBoolRing_symmDiff {α : Type u_1} [] (a : α) (b : α) :
toBoolRing (a b) = toBoolRing a + toBoolRing b
@[simp]
theorem BoundedLatticeHom.asBoolRing_apply {α : Type u_1} {β : Type u_2} [] [] (f : ) :
∀ (a : ), = (toBoolRing f ofBoolRing) a
def BoundedLatticeHom.asBoolRing {α : Type u_1} {β : Type u_2} [] [] (f : ) :

Turn a bounded lattice homomorphism from Boolean algebras α to β into a ring homomorphism from α to β considered as Boolean rings.

Instances For
@[simp]
theorem BoundedLatticeHom.asBoolRing_id {α : Type u_1} [] :
@[simp]
theorem BoundedLatticeHom.asBoolRing_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [] (g : ) (f : ) :

### Equivalence between Boolean rings and Boolean algebras #

@[simp]
theorem OrderIso.asBoolAlgAsBoolRing_symm_apply (α : Type u_4) [] :
∀ (a : α), = toBoolAlg (toBoolRing a)
@[simp]
theorem OrderIso.asBoolAlgAsBoolRing_apply (α : Type u_4) [] :
∀ (a : ), = ofBoolRing (ofBoolAlg a)
def OrderIso.asBoolAlgAsBoolRing (α : Type u_4) [] :
≃o α

Order isomorphism between α considered as a Boolean ring considered as a Boolean algebra and α.

Instances For
@[simp]
theorem RingEquiv.asBoolRingAsBoolAlg_symm_apply (α : Type u_4) [] :
∀ (a : α), = toBoolRing (toBoolAlg a)
@[simp]
theorem RingEquiv.asBoolRingAsBoolAlg_apply (α : Type u_4) [] :
∀ (a : ), = ofBoolAlg (ofBoolRing a)

Ring isomorphism between α considered as a Boolean algebra considered as a Boolean ring and α.

Instances For