Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-06 07:42 5962c76f

View on Github →

feat(algebra/ring/boolean_ring): Boolean rings (#6464) boolean_ring.to_boolean_algebra is the Boolean algebra structure on a Boolean ring.

Estimated changes

Created src/algebra/ring/boolean_ring.lean

added theorem add_eq_zero

added theorem add_self

added def boolean_ring.has_inf

added def boolean_ring.has_sup

added theorem boolean_ring.inf_assoc

added theorem boolean_ring.inf_comm

added theorem boolean_ring.inf_sup_self

added theorem boolean_ring.le_sup_inf

added theorem boolean_ring.le_sup_inf_aux

added theorem boolean_ring.sup_assoc

added theorem boolean_ring.sup_comm

added theorem boolean_ring.sup_inf_self

added def boolean_ring.to_boolean_algebra

added theorem mul_add_mul

added theorem mul_self

added theorem neg_eq

added theorem sub_eq_add