feat: port SetTheory.Game.PGame (#1512)

Co-authored-by: Maxwell Thum <maxwell.thum2718@gmail.com> Co-authored-by: Lukas Miaskiwskyi <lukas.mias@gmail.com> Co-authored-by: Gabriel Ebner <gebner@gebner.org> Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
leanprover-community · May 19, 2023 · b963857 · b963857
1 parent 83998c1
commit b963857
Show file tree

Hide file tree

Showing 2 changed files with 1,896 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1896,6 +1896,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.PGame
 import Mathlib.SetTheory.Lists
 import Mathlib.SetTheory.Ordinal.Arithmetic
 import Mathlib.SetTheory.Ordinal.Basic