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: port SetTheory.Game.Basic #4311

Closed
wants to merge 19 commits into from
Closed

[Merged by Bors] - feat: port SetTheory.Game.Basic #4311

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
19 commits
Select commit Hold shift + click to select a range
9c119be
feat: port SetTheory.Game.Basic
QuinnLesquimau May 23, 2023
d0587c3
Initial file copy from mathport
QuinnLesquimau May 23, 2023
7f0ad5d
automated fixes
QuinnLesquimau May 23, 2023
269e975
move setoid instance to PGame
QuinnLesquimau May 24, 2023
e255839
Correction of all the easy problems
QuinnLesquimau May 24, 2023
eb7ca6b
hmm, many errors remain
Jun 12, 2023
a21edd2
fix some problems
semorrison Jun 25, 2023
d93bc9f
fixes
semorrison Jun 25, 2023
19524b5
fix another
semorrison Jun 25, 2023
c008589
explicitly write out arguments to recursive calls in quot_left_distri…
dwrensha Jun 25, 2023
2ca963c
placate the style linter
dwrensha Jun 25, 2023
6517e09
don't need the simp[invImage, InvImage]
dwrensha Jun 25, 2023
89135b1
Merge branch 'master' into port/SetTheory.Game.Basic
Parcly-Taxel Jun 26, 2023
850893e
lint
Parcly-Taxel Jun 26, 2023
c7a1333
cleanup
semorrison Jun 26, 2023
3b2c4f1
Remove redundant lemmas
Parcly-Taxel Jun 26, 2023
df6fe3c
Merge branch 'port/SetTheory.Game.Basic' of github.com:leanprover-com…
Parcly-Taxel Jun 26, 2023
30e7cfa
add link to lean4 issue
semorrison Jun 26, 2023
5d7b872
Update Basic.lean
Parcly-Taxel Jun 26, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions Mathlib.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2722,6 +2722,7 @@ import Mathlib.SetTheory.Cardinal.Divisibility
import Mathlib.SetTheory.Cardinal.Finite
import Mathlib.SetTheory.Cardinal.Ordinal
import Mathlib.SetTheory.Cardinal.SchroederBernstein
import Mathlib.SetTheory.Game.Basic
import Mathlib.SetTheory.Game.PGame
import Mathlib.SetTheory.Lists
import Mathlib.SetTheory.Ordinal.Arithmetic
Expand Down
Loading
Loading