Theorems · Definition · order theory

BooleanRing.toBooleanAlgebra

{α : Type u_1} → [BooleanRing α] → BooleanAlgebra α

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)

Defined in

Mathlib.Algebra.Ring.BooleanRing

Cited by

0 results in Mathlib

Foundations

Depth 28 from the axioms · uses propext, Quot.sound

Assumes

BooleanRing