# Zulip Chat Archive

## Stream: Is there code for X?

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

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

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 (Jun 14 2020 at 09:34):

Currently a Boolean algebra is not a ring

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

what should we do about this?

#### 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):

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

#### 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.

#### Yury G. Kudryashov (Jun 14 2020 at 22:39):

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

#### Aaron Anderson (Jun 30 2020 at 06:47):

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 (Jun 30 2020 at 06:49):

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

Last updated: May 16 2021 at 05:21 UTC