Upstream to Mathlib

Stream: Equational

[Pietro Monticone]

I am golfing and upstreaming some of our code to Mathlib.

I'm prefixing all the Mathlib branches with EquationalTheories/ and adding the sentence "Upstreamed from the EquationalTheories project." to make sure they're findable when we need to mention them in the paper.

[Pietro Monticone]

Opened #17971

[Pietro Monticone]

Opened #17973

[Pietro Monticone]

Opened #17976

[Pietro Monticone]

Opened #17977

[Shreyas Srinivas]

Sounds like this should be brought up on the mathlib channel

[Shreyas Srinivas]

(deleted)

[Pietro Monticone]

Here it is #mathlib4 > Upstream from the EquationalTheories Project .

For archival purposes I'll keep posting here too.

[Pietro Monticone]

If you want to keep track of the ET-related Mathlib PRs, see here.

We have also added it to the Wiki homepage and in the plan of the paper together with the LeanBlueprint ones.

[Michael Bucko]

Pietro Monticone schrieb:

Opened #17971.

Can this be somehow seen as Set:Action:Modify:Preserve-Bijection? (or JS-wise OnSetModify (Preserve Bijection)?)

[Pietro Monticone]

All of the above Mathlib PRs have been merged.

[Alex Meiburg]

Opened #19618

[Alex Meiburg]

And opened #19695

[Bernhard Reinke]

Opened #22507

[Bernhard Reinke]

Opened #22510

[Bernhard Reinke]

Opened #22511

[Bernhard Reinke]

Opened #22513

[Bernhard Reinke]

Opened #22639

[Bernhard Reinke]

This one was a bit too big so I decided to split it into some smaller PRs, see #PR reviews > #22639 (cyclically) reduced words @ 💬 here.

[Bernhard Reinke]

@Joachim Breitner, could you maybe have a look at them? I get you as a suggested reviewer on GitHub

[Joachim Breitner]

It’s been a long time that I touched that code; I’d rather not get involved in mathlib pr reviewing at the moment, sorry.

[Bernhard Reinke]

No worries!