## Stream: Is there code for X?

### Topic: A boolean algebra is an ordered comm monoid

#### Kenny Lau (Jun 14 2020 at 09:34):

Currently a Boolean algebra is not a ring

#### Scott Morrison (Jun 14 2020 at 10:28):

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

#### Kenny Lau (Jun 14 2020 at 10:28):

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

#### Kenny Lau (Jun 14 2020 at 10:29):

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

#### Scott Morrison (Jun 14 2020 at 10:55):

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

#### Kenny Lau (Jun 14 2020 at 10:57):

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

#### Scott Morrison (Jun 14 2020 at 10:58):

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

#### Scott Morrison (Jun 14 2020 at 10:59):

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

#### Bryan Gin-ge Chen (Jun 14 2020 at 15:20):

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