Lean4
/-- Every generalized Boolean algebra has the structure of a nonunital 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 `⊥`
-/
abbrev toNonUnitalCommRing [GeneralizedBooleanAlgebra α] : NonUnitalCommRing α
where
add := (· ∆ ·)
add_assoc := symmDiff_assoc
zero := ⊥
zero_add := bot_symmDiff
add_zero := symmDiff_bot
zero_mul := bot_inf_eq
mul_zero := inf_bot_eq
neg := id
neg_add_cancel := symmDiff_self
add_comm := symmDiff_comm
mul := (· ⊓ ·)
mul_assoc := inf_assoc
mul_comm := inf_comm
left_distrib := inf_symmDiff_distrib_left
right_distrib := inf_symmDiff_distrib_right
nsmul :=
letI : Zero α := ⟨⊥⟩;
letI : Add α := ⟨(· ∆ ·)⟩;
nsmulRec
zsmul :=
letI : Zero α := ⟨⊥⟩;
letI : Add α := ⟨(· ∆ ·)⟩;
letI : Neg α := ⟨id⟩;
zsmulRec
