## Stream: new members

### Topic: Symmetric difference

#### Daniel Fabian (May 31 2020 at 14:40):

I want to use symmetric difference but can't seem to find it in either mathlib or standard libary. Am I just missing the name or should I define it myself.?

#### Jeremy Avigad (May 31 2020 at 14:42):

I don't think it is in the library...

#### Kevin Buzzard (May 31 2020 at 16:33):

Is there more than one way to do it constructively?

#### Kevin Buzzard (May 31 2020 at 16:34):

and and or are unambiguous inductive types, but maybe there are several xor on Prop?

#### Kevin Buzzard (May 31 2020 at 16:35):

(as far as a constructivist is concerned)

#### Reid Barton (May 31 2020 at 16:40):

Yes, probably. Where does symmetric difference actually come up?

#### Bryan Gin-ge Chen (May 31 2020 at 16:47):

It's addition in the Boolean ring structure on power sets.

#### Kevin Buzzard (May 31 2020 at 17:46):

Right. Is this constructively a Boolean ring? Maybe it's only a Propian ring...

#### Chris Hughes (May 31 2020 at 18:07):

I think not (a iff b) also works constructively. I don't think a iff not b is constructively associative or commutative.

#### Kevin Buzzard (May 31 2020 at 19:04):

Maybe we should introduce niff

#### Mario Carneiro (May 31 2020 at 20:23):

Do we have that Prop is a boolean ring? (which is equivalent to LEM)

#### Mario Carneiro (May 31 2020 at 20:24):

If so then you can get sets using the pi instance

Last updated: May 08 2021 at 09:11 UTC