Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat: more PGame.identical PGame.memₗ PGame.memᵣ APIs #5901

Closed
wants to merge 64 commits into from
Closed

[Merged by Bors] - feat: more PGame.identical PGame.memₗ PGame.memᵣ APIs #5901

wants to merge 64 commits into from

Conversation

FR-vdash-bot
Copy link
Collaborator

@FR-vdash-bot FR-vdash-bot commented Jul 14, 2023 •
edited by alreadydone
Loading

This PR is the first step to remove PGame.Relabelling (which is only for implementing things in lean and not real identity) and define games with identity as Eq.

Zulip

Open in Gitpod

(Was a mathlib3 PR)

@FR-vdash-bot
feat: add lemmas about Relator.LeftTotal Relator.RightTotal `Rela…
3cc4bd5 
…tor.BiTotal`
@FR-vdash-bot
feat: define pgame.identical pgame.memₗ pgame.memᵣ
088ac08 
This PR is the first step to remove `PGame.Relabelling` (which is only for implementing things in lean and not real identity) and define games with identity as `Eq`.
@kim-em kim-em added the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Jul 14, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 19, 2023
@kim-em kim-em mentioned this pull request Jul 27, 2023
Closed
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Jul 31, 2023
@leanprover-community leanprover-community deleted a comment from kim-em Jul 31, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 31, 2023
@kim-em kim-em added the t-combinatorics Combinatorics label Aug 6, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Aug 31, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Sep 10, 2023
@FR-vdash-bot FR-vdash-bot changed the title feat: define pgame.identical pgame.memₗ pgame.memᵣ feat: define PGame.identical PGame.memₗ PGame.memᵣ Sep 14, 2023
@FR-vdash-bot FR-vdash-bot mentioned this pull request Sep 14, 2023
Open
2 tasks
@bors bors bot changed the base branch from master to ScottCarnahan/BinomialRing2 September 17, 2023 03:24
@FR-vdash-bot FR-vdash-bot changed the base branch from ScottCarnahan/BinomialRing2 to master September 17, 2023 11:45
@FR-vdash-bot FR-vdash-bot changed the title feat: add PGame.identical PGame.memₗ PGame.memᵣ APIs feat: more PGame.identical PGame.memₗ PGame.memᵣ APIs Sep 25, 2024
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Sep 25, 2024
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Sep 26, 2024
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Nov 18, 2024
@mathlib4-dependent-issues-bot
Copy link
Collaborator

This PR/issue depends on:

@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Dec 1, 2024
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Dec 21, 2024
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Dec 26, 2024
vihdzp
vihdzp reviewed Jan 1, 2025
View reviewed changes
Mathlib/SetTheory/Game/Basic.lean
@@ -380,6 +378,17 @@ theorem rightMoves_mul_cases {x y : PGame} (k) {P : (x * y).RightMoves → Prop}
· apply hl
· apply hr

/-- `x * y` and `y * x` have the same moves. -/
protected lemma mul_comm (x y : PGame) : x * y ≡ y * x :=
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Just a small note to maintainers: since the ultimate goal is to replace Relabelling in favor of Identical, this proof is preferrable to the more direct one that makes use of mulCommRelabelling.

Mathlib/SetTheory/Game/Basic.lean Outdated Show resolved Hide resolved
Mathlib/SetTheory/Game/PGame.lean Show resolved Hide resolved
Mathlib/SetTheory/Game/PGame.lean Outdated Show resolved Hide resolved
Mathlib/SetTheory/Game/PGame.lean Outdated Show resolved Hide resolved
Mathlib/SetTheory/Game/PGame.lean Show resolved Hide resolved
YaelDillies
YaelDillies approved these changes Jan 4, 2025
View reviewed changes
Copy link
Collaborator

@YaelDillies YaelDillies left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!

maintainer delegate

Mathlib/SetTheory/Game/PGame.lean Outdated Show resolved Hide resolved
Mathlib/SetTheory/Game/PGame.lean Outdated Show resolved Hide resolved
Mathlib/SetTheory/Game/PGame.lean Outdated Show resolved Hide resolved
@github-actions GitHub Actions
Copy link

github-actions bot commented Jan 4, 2025

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

TwoFX
TwoFX reviewed Jan 20, 2025
View reviewed changes
Copy link
Member

@TwoFX TwoFX left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

bors r+

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the ready-to-merge This PR has been sent to bors. label Jan 20, 2025
mathlib-bors bot pushed a commit that referenced this pull request Jan 20, 2025
@FR-vdash-bot @hwatheod @vihdzp
feat: more PGame.identical PGame.memₗ PGame.memᵣ APIs (#5901)
f68a59e 
This PR is the first step to remove `PGame.Relabelling` (which is only for implementing things in lean and not real identity) and define games with identity as `Eq`.

[Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Well-founded.20recursion.20for.20pgames/near/338664567)



Co-authored-by: hwatheod <[email protected]>
Co-authored-by: Theodore Hwa <[email protected]>
Co-authored-by: Violeta Hernández <[email protected]>
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Jan 20, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: more PGame.identical PGame.memₗ PGame.memᵣ APIs [Merged by Bors] - feat: more PGame.identical PGame.memₗ PGame.memᵣ APIs Jan 20, 2025
@mathlib-bors mathlib-bors bot closed this Jan 20, 2025
@mathlib-bors mathlib-bors bot deleted the FR_game_identical branch January 20, 2025 10:09
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@urkud urkud urkud left review comments

@hwatheod hwatheod hwatheod left review comments

@TwoFX TwoFX TwoFX left review comments

@YaelDillies YaelDillies YaelDillies approved these changes

@vihdzp vihdzp vihdzp approved these changes

@timotree3 timotree3 Awaiting requested review from timotree3

Assignees

@kmill kmill

Labels
maintainer-merge ready-to-merge This PR has been sent to bors. t-combinatorics Combinatorics
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.