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

source
@[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.

source
@[protected, instance]
def has_mul.mul.is_idempotent {α : Type u_1} [boolean_ring α] :
is_idempotent α has_mul.mul
source
@[simp]
theorem mul_self {α : Type u_1} [boolean_ring α] (a : α) :
a * a = a
source
@[simp]
theorem add_self {α : Type u_1} [boolean_ring α] (a : α) :
a + a = 0
source
@[simp]
theorem neg_eq {α : Type u_1} [boolean_ring α] (a : α) :
-a = a
source
theorem add_eq_zero {α : Type u_1} [boolean_ring α] (a b : α) :
a + b = 0 ↔ a = b
source
@[simp]
theorem mul_add_mul {α : Type u_1} [boolean_ring α] (a b : α) :
a * b + b * a = 0
source
@[simp]
theorem sub_eq_add {α : Type u_1} [boolean_ring α] (a b : α) :
a - b = a + b
source
@[simp]
theorem mul_one_add_self {α : Type u_1} [boolean_ring α] (a : α) :
a * (1 + a) = 0
source
@[protected, instance]
def boolean_ring.comm_ring {α : Type u_1} [boolean_ring α] :
comm_ring α
Equations
source
@[instance]
def boolean_ring.has_sup {α : Type u_1} [boolean_ring α] :
has_sup α

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

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

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

Equations
source
theorem boolean_ring.sup_comm {α : Type u_1} [boolean_ring α] (a b : α) :
a ⊔ b = b ⊔ a
source
theorem boolean_ring.inf_comm {α : Type u_1} [boolean_ring α] (a b : α) :
a ⊓ b = b ⊓ a
source
theorem boolean_ring.sup_assoc {α : Type u_1} [boolean_ring α] (a b c : α) :
a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
source
theorem boolean_ring.inf_assoc {α : Type u_1} [boolean_ring α] (a b c : α) :
a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
source
theorem boolean_ring.sup_inf_self {α : Type u_1} [boolean_ring α] (a b : α) :
a ⊔ a ⊓ b = a
source
theorem boolean_ring.inf_sup_self {α : Type u_1} [boolean_ring α] (a b : α) :
a ⊓ (a ⊔ b) = a
source
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
source
theorem boolean_ring.le_sup_inf {α : Type u_1} [boolean_ring α] (a b c : α) :
(a ⊔ b) ⊓ (a ⊔ c) ⊔ (a ⊔ b ⊓ c) = a ⊔ b ⊓ c
source
@[instance]
def boolean_ring.has_sdiff {α : Type u_1} [boolean_ring α] :
has_sdiff α

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

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

The bottom element of a Boolean ring is 0.

Equations
source
theorem boolean_ring.sup_inf_sdiff {α : Type u_1} [boolean_ring α] (a b : α) :
a ⊓ b ⊔ a \ b = a
source
theorem boolean_ring.inf_inf_sdiff {α : Type u_1} [boolean_ring α] (a b : α) :
a ⊓ b ⊓ a \ b = ⊥
source
@[instance]
def boolean_ring.to_boolean_algebra {α : Type u_1} [boolean_ring α] :
boolean_algebra α

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