Skip to content

[Merged by Bors] - feat(SetTheory/Game/Ordinal): game product of ordinals is natural product#15690

Closed
vihdzp wants to merge 13 commits intomasterfrom
ordinal_game_mul
Closed

[Merged by Bors] - feat(SetTheory/Game/Ordinal): game product of ordinals is natural product#15690
vihdzp wants to merge 13 commits intomasterfrom
ordinal_game_mul

Conversation

@vihdzp
Copy link
Copy Markdown
Collaborator

@vihdzp vihdzp commented Aug 11, 2024 •
edited
Loading

I also flipped and renamed toPGame_nadd at the request of Yaël.

It's been a long while since I wrote any Lean code, so it might be possible to golf my proofs a bit.

Open in Gitpod

@vihdzp vihdzp added the t-logic Logic (model theory, etc) label Aug 11, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Aug 11, 2024 •
edited
Loading

PR summary 5f215656cd

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ _
+ game_eq
+ isEmpty_leftMoves_mul
+ isEmpty_rightMoves_mul
+ toGame_nadd
+ toGame_nmul
+ toPGame_nadd
+ toPGame_nmul
- isEmpty_mul_zero_leftMoves
- isEmpty_mul_zero_rightMoves
- isEmpty_zero_mul_leftMoves
- isEmpty_zero_mul_rightMoves
- toPGame_add
- toPGame_add_mk'

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

YaelDillies
YaelDillies reviewed Aug 11, 2024
View reviewed changes
YaelDillies
YaelDillies reviewed Aug 11, 2024
View reviewed changes
YaelDillies
YaelDillies reviewed Aug 11, 2024
View reviewed changes
YaelDillies
YaelDillies reviewed Aug 11, 2024
View reviewed changes
Copy link
Copy Markdown
Contributor

@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.

Do you mind fixing the Game.PGame namespace issue in a preliminary PR? I have a hard time understanding what's going on

@ghost ghost added blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) and removed blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels Aug 11, 2024
@ghost
Copy link
Copy Markdown

ghost commented Aug 12, 2024

This PR/issue depends on:

@ghost ghost 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 12, 2024
YaelDillies
YaelDillies reviewed Aug 12, 2024
View reviewed changes
@ghost ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Aug 12, 2024
vihdzp and others added 2 commits August 12, 2024 00:09
@vihdzp @YaelDillies
Update Mathlib/SetTheory/Game/Basic.lean
aca0c95 
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
@vihdzp
Apply name replacements
ece8e26
@vihdzp vihdzp mentioned this pull request Aug 12, 2024
Closed
1 task
YaelDillies
YaelDillies reviewed Aug 12, 2024
View reviewed changes
YaelDillies
YaelDillies reviewed Aug 12, 2024
View reviewed changes
YaelDillies
YaelDillies reviewed Aug 12, 2024
View reviewed changes
YaelDillies
YaelDillies reviewed Aug 12, 2024
View reviewed changes
@vihdzp @YaelDillies
Update Mathlib/SetTheory/Game/Ordinal.lean
5f21565 
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
YaelDillies
YaelDillies approved these changes Aug 12, 2024
View reviewed changes
Copy link
Copy Markdown
Contributor

@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 merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Aug 12, 2024

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

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Aug 12, 2024
@eric-wieser
Copy link
Copy Markdown
Member

eric-wieser commented Aug 12, 2024

bors merge

Thanks!

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Aug 12, 2024
mathlib-bors bot pushed a commit that referenced this pull request Aug 12, 2024
@vihdzp
feat(SetTheory/Game/Ordinal): game product of ordinals is natural pro…
7a462dc 
…duct (#15690)

I also flipped and renamed `toPGame_nadd` at the request of Yaël.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Aug 12, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(SetTheory/Game/Ordinal): game product of ordinals is natural product [Merged by Bors] - feat(SetTheory/Game/Ordinal): game product of ordinals is natural product Aug 12, 2024
@mathlib-bors mathlib-bors bot closed this Aug 12, 2024
@mathlib-bors mathlib-bors bot deleted the ordinal_game_mul branch August 12, 2024 22:32
bjoernkjoshanssen pushed a commit that referenced this pull request Sep 9, 2024
@vihdzp @bjoernkjoshanssen
feat(SetTheory/Game/Ordinal): game product of ordinals is natural pro…
92146a7 
…duct (#15690)

I also flipped and renamed `toPGame_nadd` at the request of Yaël.
bjoernkjoshanssen pushed a commit that referenced this pull request Sep 9, 2024
@vihdzp @bjoernkjoshanssen
feat(SetTheory/Game/Ordinal): game product of ordinals is natural pro…
bad9e40 
…duct (#15690)

I also flipped and renamed `toPGame_nadd` at the request of Yaël.
bjoernkjoshanssen pushed a commit that referenced this pull request Sep 12, 2024
@vihdzp @bjoernkjoshanssen
feat(SetTheory/Game/Ordinal): game product of ordinals is natural pro…
f93232e 
…duct (#15690)

I also flipped and renamed `toPGame_nadd` at the request of Yaël.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@YaelDillies YaelDillies YaelDillies approved these changes

+1 more reviewer

@nomeata nomeata nomeata left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. ready-to-merge This PR has been sent to bors. t-logic Logic (model theory, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@vihdzp @eric-wieser @nomeata @YaelDillies