A boolean algebra is an ordered comm monoid

Stream: Is there code for X?

[Kenny Lau]

Boolean algebra: https://github.com/leanprover-community/mathlib/blob/master/src/order/boolean_algebra.lean
Ordered comm monoid: https://github.com/leanprover-community/mathlib/blob/master/src/algebra/ordered_group.lean

[Kenny Lau]

Currently a Boolean algebra is not a ring

[Kenny Lau]

what should we do about this?

[Scott Morrison]

Sorry, @Kenny Lau, could you be less telegraphic? I'm not sure what it is you're worried about.

[Kenny Lau]

sorry for not expressing myself clearly, I'm just wondering whether we should define a ring structure on a boolean algebra

[Kenny Lau]

and then prove that any Boolean algebra is an ordered comm monoid

[Scott Morrison]

as in http://math.mit.edu/~jerison/103/handouts/rings.pdf

[Scott Morrison]

I guess I don't know how useful it is to do this...?

[Kenny Lau]

well, ordered_comm_monoid was introduced 5 days ago in #2844 and I thought it would be useful to have some examples

[Scott Morrison]

I just worry that allowing people to use + to mean "symmetric difference of sets" is unlikely to lead to clarity. :-)

[Scott Morrison]

But I guess if it's done with def and not instance it's fine for constructing examples.

[Bryan Gin-ge Chen]

I think adding boolean rings is a fine idea. Maybe we could get Stone's representation theorem too.

[Yury G. Kudryashov]

Please don't add this as a ring instance on prop/set.

[Aaron Anderson]

There are also times where you do want to have an additive or multiplicative structure on a lattice, which might conflict with a boolean_ring instance

[Aaron Anderson]

I would be interested in working on an implementation of the Stone representation theorem though, just with a function that takes a boolean algebra lattice instance to a boolean ring ordered ring instance