feat: define PGame.identical PGame.memₗ PGame.memᵣ #5901

Stream: PR reviews

[Johan Commelin]

I'm looking for reviewers for a game theory PR. I know nothing about this topic, so all assistance is welcome!

feat: define PGame.identical PGame.memₗ PGame.memᵣ #5901

If you have a bit of experience with mathlib style, but you don't really know what a review should look like, here are some helpful guidelines: https://leanprover-community.github.io/contribute/pr-review.html

[Timo Carlin-Burns]

I would be happy to try to help! I know a bit about Combinatorial Game Theory and find it fascinating. Since reading the discussion in the old Zulip thread, I have been eagerly awaiting the introduction of Identical and removal of Relabelling, so I was very happy to see this PR.

[Johan Commelin]

Thanks! Feel free to ping in this thread when you've left a review.

[Timo Carlin-Burns]

I think part of what makes the diff of this PR daunting is that it's almost all additions, when in fact, the new Identical is supposed to replace the old Relabelling. The next PR on top of this one, #7162 almost has an easier diff to read because with each theorem added about Identical, the corresponding theorem about Relabelling is deleted, so it's easy to see that the API surface isn't really increasing. Is there general guidance about whether adding a replacement and deleting the old thing should be combined into one PR or split?

[Johan Commelin]

It depends a bit, also on how large the total diff will become.

[Johan Commelin]

But you are very welcome to review the two PRs as a pair!

[Johan Commelin]

And cross-ref your reviews, if you want to.

[Timo Carlin-Burns]

@Johan Commelin I posted an initial review. Sorry for the delay, I was exploring a relevant refactor (draft PR #10609) before commenting. I hope you assigning Kyle isn't a signal that you've given up on me :sweat_smile:

[Johan Commelin]

No, it certainly isn't!

[Johan Commelin]

Thanks a lot for your efforts!

[Johan Commelin]

I'm just assigning maintainers to various PRs, to somewhat distribute the load of hitting the merge button (-;

[Timo Carlin-Burns]

Now that I've posted a request, should I change the PR to awaiting-author as well?

[Kevin Buzzard]

Many thanks for your review!

[Kyle Miller]

Yeah, if you make a request to have things changed before you make your next review, it's encouraged changing the label to awaiting-author