Skip to content

Commit 08657ed

Browse files
committed
chore: remove deprecated material from CGT (#35550)
The modules have been deprecated for 6 months. See #28063.
1 parent e318a59 commit 08657ed

23 files changed

+1
-8017
lines changed

Counterexamples.lean

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,6 @@ import Counterexamples.DimensionPolynomial
77
import Counterexamples.DirectSumIsInternal
88
import Counterexamples.DiscreteTopologyNonDiscreteUniformity
99
import Counterexamples.EulerSumOfPowers
10-
import Counterexamples.GameMultiplication
1110
import Counterexamples.Girard
1211
import Counterexamples.HeawoodUnitDistance
1312
import Counterexamples.HomogeneousPrimeNotPrime

Counterexamples/GameMultiplication.lean

Lines changed: 0 additions & 87 deletions
This file was deleted.

Mathlib.lean

Lines changed: 0 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -6648,17 +6648,7 @@ public import Mathlib.SetTheory.Cardinal.Subfield
66486648
public import Mathlib.SetTheory.Cardinal.ToNat
66496649
public import Mathlib.SetTheory.Cardinal.UnivLE
66506650
public import Mathlib.SetTheory.Descriptive.Tree
6651-
public import Mathlib.SetTheory.Game.Basic
6652-
public import Mathlib.SetTheory.Game.Birthday
6653-
public import Mathlib.SetTheory.Game.Domineering
6654-
public import Mathlib.SetTheory.Game.Impartial
6655-
public import Mathlib.SetTheory.Game.Nim
6656-
public import Mathlib.SetTheory.Game.Ordinal
6657-
public import Mathlib.SetTheory.Game.Short
6658-
public import Mathlib.SetTheory.Game.State
66596651
public import Mathlib.SetTheory.Lists
6660-
public import Mathlib.SetTheory.Nimber.Basic
6661-
public import Mathlib.SetTheory.Nimber.Field
66626652
public import Mathlib.SetTheory.Ordinal.Arithmetic
66636653
public import Mathlib.SetTheory.Ordinal.Basic
66646654
public import Mathlib.SetTheory.Ordinal.CantorNormalForm
@@ -6667,18 +6657,11 @@ public import Mathlib.SetTheory.Ordinal.Exponential
66676657
public import Mathlib.SetTheory.Ordinal.Family
66686658
public import Mathlib.SetTheory.Ordinal.FixedPoint
66696659
public import Mathlib.SetTheory.Ordinal.FixedPointApproximants
6670-
public import Mathlib.SetTheory.Ordinal.NaturalOps
66716660
public import Mathlib.SetTheory.Ordinal.Notation
66726661
public import Mathlib.SetTheory.Ordinal.Principal
66736662
public import Mathlib.SetTheory.Ordinal.Rank
66746663
public import Mathlib.SetTheory.Ordinal.Topology
66756664
public import Mathlib.SetTheory.Ordinal.Veblen
6676-
public import Mathlib.SetTheory.PGame.Algebra
6677-
public import Mathlib.SetTheory.PGame.Basic
6678-
public import Mathlib.SetTheory.PGame.Order
6679-
public import Mathlib.SetTheory.Surreal.Basic
6680-
public import Mathlib.SetTheory.Surreal.Dyadic
6681-
public import Mathlib.SetTheory.Surreal.Multiplication
66826665
public import Mathlib.SetTheory.ZFC.Basic
66836666
public import Mathlib.SetTheory.ZFC.Cardinal
66846667
public import Mathlib.SetTheory.ZFC.Class

0 commit comments

Comments
 (0)