MATHLIB: What Should We Upstream?

Stream: Equational

[Pietro Monticone]

It's probably time to start planning what we should upstream to Mathlib. I'd like to know your views on the following:

1. What do you consider Mathlib-relevant?
2. If Mathlib-relevant, what is ready to port?
3. If ready to port, what should be prioritised?
4. If not ready to port, what requires more work?

[Cody Roux]

I just finished a fiddly proof involving "boolean rings" taking from here: https://en.wikipedia.org/wiki/Boolean_algebra_(structure). I was surprised no one had done this, though the proof of associativity is finicky.

[Cody Roux]

Not particularly crucial, I imagine; this is 1930s stuff.

[Bryan Gin-ge Chen]

Out of curiosity, what did you prove about Boolean rings? We have them in mathlib4 (see docs4#BooleanRing) but there isn't anything there other than the equivalence with Boolean algebras.

[Cody Roux]

I gave an alternate definition (the one from wikipedia) and proved that the multiplication is indeed associative; this is fiddly, requires a careful setup, thankfully fully explained in the article.

Then I proved that the Sheffer laws axiomatizing the Sheffer stroke encode such a thing.

[Cody Roux]

But I'm getting pushback on this, so maybe I'll refactor it to omit creating such a structure

[Shreyas Srinivas]

I think you could also go for Option 2 you suggested in the PR comments, where you show that the Sheffer definition is indeed a BooleanRing in the mathlib sense

[Shreyas Srinivas]

But then upstreaming it to Mathlib is going to be difficult

[Cody Roux]

The main obstruction is just time, I'm a little busy ATM to do all this

[Cody Roux]

I'm happy with option 3, I think

[Cody Roux]

though it is confusing that the +-like operation does not become the ring +.

[Bryan Gin-ge Chen]

I gather the PR in question is equational#708. Feel free to ping me if / when you decide to upstream any parts to mathlib!

[Cody Roux]

Thanks! Probably not right away, unless someone wants to step in.