mathlib documentation

algebra.ring.boolean_ring

Boolean rings #

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

Main declarations #

Tags #

boolean ring, boolean algebra

@[class]
structure boolean_ring (α : Type u_1) :
Type u_1
  • to_ring : ring α
  • mul_self : ∀ (a : α), a * a = a

A Boolean ring is a ring where multiplication is idempotent.

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

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

Equations
@[instance]
def boolean_ring.has_inf {α : Type u_1} [boolean_ring α] :

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

Equations
theorem boolean_ring.sup_comm {α : Type u_1} [boolean_ring α] (a b : α) :
a b = b a
theorem boolean_ring.inf_comm {α : Type u_1} [boolean_ring α] (a b : α) :
a b = b a
theorem boolean_ring.sup_assoc {α : Type u_1} [boolean_ring α] (a b c : α) :
a b c = a (b c)
theorem boolean_ring.inf_assoc {α : Type u_1} [boolean_ring α] (a b c : α) :
a b c = a (b c)
theorem boolean_ring.sup_inf_self {α : Type u_1} [boolean_ring α] (a b : α) :
a a b = a
theorem boolean_ring.inf_sup_self {α : Type u_1} [boolean_ring α] (a b : α) :
a (a b) = a
theorem boolean_ring.le_sup_inf_aux {α : Type u_1} [boolean_ring α] (a b c : α) :
(a + b + a * b) * (a + c + a * c) = a + b * c + a * b * c
theorem boolean_ring.le_sup_inf {α : Type u_1} [boolean_ring α] (a b c : α) :
(a b) (a c) (a b c) = a b c
@[instance]
def boolean_ring.has_sdiff {α : Type u_1} [boolean_ring α] :

The "set difference" operation in a Boolean ring is x * (1 + y).

Equations
@[instance]
def boolean_ring.has_bot {α : Type u_1} [boolean_ring α] :

The bottom element of a Boolean ring is 0.

Equations
theorem boolean_ring.sup_inf_sdiff {α : Type u_1} [boolean_ring α] (a b : α) :
a b a \ b = a
theorem boolean_ring.inf_inf_sdiff {α : Type u_1} [boolean_ring α] (a b : α) :
a b (a \ b) =
@[instance]

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)
Equations