Commit 2026-02-20 00:22 08657ed7

View on Github →

chore: remove deprecated material from CGT (#35550) The modules have been deprecated for 6 months. See #28063.

Estimated changes

deleted def SetTheory.Game.LF
deleted theorem SetTheory.Game.not_le
deleted theorem SetTheory.Game.not_lf
deleted theorem SetTheory.Game.zero_def
deleted inductive SetTheory.PGame.InvTy
deleted theorem SetTheory.PGame.inv'_one
deleted theorem SetTheory.PGame.inv_one
deleted theorem SetTheory.PGame.inv_zero
deleted theorem SetTheory.PGame.mul_neg
deleted theorem SetTheory.PGame.neg_mul
deleted theorem SetTheory.PGame.quot_add
deleted theorem SetTheory.PGame.quot_neg
deleted theorem SetTheory.PGame.quot_one
deleted theorem SetTheory.PGame.quot_sub
deleted theorem SetTheory.PGame.quot_zero
deleted theorem SetTheory.PGame.neg_nim
deleted theorem Ordinal.mk_toPGame
deleted theorem Ordinal.toGame_inj
deleted theorem Ordinal.toGame_injective
deleted theorem Ordinal.toGame_le_iff
deleted theorem Ordinal.toGame_lf_iff
deleted theorem Ordinal.toGame_lt_iff
deleted theorem Ordinal.toGame_nadd
deleted theorem Ordinal.toGame_natCast
deleted theorem Ordinal.toGame_nmul
deleted theorem Ordinal.toGame_one
deleted theorem Ordinal.toGame_zero
deleted theorem Ordinal.toPGame_equiv_iff
deleted theorem Ordinal.toPGame_inj
deleted theorem Ordinal.toPGame_injective
deleted theorem Ordinal.toPGame_le
deleted theorem Ordinal.toPGame_le_iff
deleted theorem Ordinal.toPGame_leftMoves
deleted theorem Ordinal.toPGame_lf
deleted theorem Ordinal.toPGame_lf_iff
deleted theorem Ordinal.toPGame_lt
deleted theorem Ordinal.toPGame_lt_iff
deleted theorem Ordinal.toPGame_moveLeft'
deleted theorem Ordinal.toPGame_moveLeft
deleted theorem Ordinal.toPGame_nadd
deleted theorem Ordinal.toPGame_natCast
deleted theorem Ordinal.toPGame_nmul
deleted theorem Ordinal.toPGame_nonneg
deleted theorem Ordinal.toPGame_one
deleted theorem Ordinal.toPGame_zero
deleted inductive SetTheory.PGame.Short
deleted theorem Nimber.add_cancel_left
deleted theorem Nimber.add_cancel_right
deleted theorem Nimber.add_def
deleted theorem Nimber.add_eq_zero
deleted theorem Nimber.add_nat
deleted theorem Nimber.add_ne_zero_iff
deleted theorem Nimber.add_self
deleted theorem Nimber.add_trichotomy
deleted theorem Nimber.bot_eq_zero
deleted theorem Nimber.eq_nat_of_le_nat
deleted theorem Nimber.exists_of_lt_add
deleted theorem Nimber.induction
deleted theorem Nimber.lt_add_cases
deleted theorem Nimber.lt_one_iff_zero
deleted theorem Nimber.lt_wf
deleted theorem Nimber.one_le_iff_ne_zero
deleted theorem Nimber.succ_def
deleted def Nimber.toOrdinal
deleted theorem Nimber.toOrdinal_eq_one
deleted theorem Nimber.toOrdinal_eq_zero
deleted theorem Nimber.toOrdinal_max
deleted theorem Nimber.toOrdinal_min
deleted theorem Nimber.toOrdinal_one
deleted theorem Nimber.toOrdinal_symm_eq
deleted theorem Nimber.toOrdinal_toNimber
deleted theorem Nimber.toOrdinal_zero
deleted def Nimber
deleted def Ordinal.toNimber
deleted theorem Ordinal.toNimber_eq_one
deleted theorem Ordinal.toNimber_eq_zero
deleted theorem Ordinal.toNimber_max
deleted theorem Ordinal.toNimber_min
deleted theorem Ordinal.toNimber_one
deleted theorem Ordinal.toNimber_symm_eq
deleted theorem Ordinal.toNimber_zero
deleted theorem not_small_nimber
deleted theorem Nimber.cons_mem_invSet
deleted theorem Nimber.exists_of_lt_mul
deleted def Nimber.invAux
deleted theorem Nimber.invAux_ne_zero
deleted def Nimber.invSet
deleted theorem Nimber.invSet_recOn
deleted theorem Nimber.inv_eq_invAux
deleted theorem Nimber.mul_def
deleted theorem Nimber.mul_invAux_cancel
deleted theorem Nimber.zero_mem_invSet
deleted theorem NatOrdinal.add_le_iff
deleted theorem NatOrdinal.bot_eq_zero
deleted theorem NatOrdinal.induction
deleted theorem NatOrdinal.lt_add_iff
deleted theorem NatOrdinal.lt_mul_iff
deleted theorem NatOrdinal.lt_wf
deleted theorem NatOrdinal.mul_add_lt
deleted theorem NatOrdinal.mul_le_iff
deleted theorem NatOrdinal.nmul_nadd_le
deleted theorem NatOrdinal.not_lt_zero
deleted theorem NatOrdinal.succ_def
deleted theorem NatOrdinal.toOrdinal_max
deleted theorem NatOrdinal.toOrdinal_min
deleted theorem NatOrdinal.toOrdinal_one
deleted theorem NatOrdinal.toOrdinal_zero
deleted def NatOrdinal
deleted theorem Ordinal.add_le_nadd
deleted theorem Ordinal.add_one_nmul
deleted theorem Ordinal.le_nadd_left
deleted theorem Ordinal.le_nadd_right
deleted theorem Ordinal.le_nadd_self
deleted theorem Ordinal.le_self_nadd
deleted theorem Ordinal.lt_nadd_iff
deleted theorem Ordinal.lt_nmul_iff
deleted theorem Ordinal.lt_nmul_iff₃
deleted theorem Ordinal.mul_le_nmul
deleted theorem Ordinal.nadd_assoc
deleted theorem Ordinal.nadd_comm
deleted theorem Ordinal.nadd_eq_add
deleted theorem Ordinal.nadd_le_iff
deleted theorem Ordinal.nadd_le_nadd
deleted theorem Ordinal.nadd_le_nadd_left
deleted theorem Ordinal.nadd_left_cancel
deleted theorem Ordinal.nadd_left_comm
deleted theorem Ordinal.nadd_lt_nadd
deleted theorem Ordinal.nadd_lt_nadd_left
deleted theorem Ordinal.nadd_nat
deleted theorem Ordinal.nadd_nmul
deleted theorem Ordinal.nadd_one
deleted theorem Ordinal.nadd_one_nmul
deleted theorem Ordinal.nadd_right_cancel
deleted theorem Ordinal.nadd_right_comm
deleted theorem Ordinal.nadd_succ
deleted theorem Ordinal.nadd_zero
deleted theorem Ordinal.nat_nadd
deleted theorem Ordinal.nmul_add_one
deleted theorem Ordinal.nmul_assoc
deleted theorem Ordinal.nmul_comm
deleted theorem Ordinal.nmul_eq_mul
deleted theorem Ordinal.nmul_le_iff
deleted theorem Ordinal.nmul_le_iff₃
deleted theorem Ordinal.nmul_le_nmul
deleted theorem Ordinal.nmul_le_nmul_left
deleted theorem Ordinal.nmul_nadd
deleted theorem Ordinal.nmul_nadd_le
deleted theorem Ordinal.nmul_nadd_le₃
deleted theorem Ordinal.nmul_nadd_lt
deleted theorem Ordinal.nmul_nadd_lt₃
deleted theorem Ordinal.nmul_nadd_one
deleted theorem Ordinal.nmul_one
deleted theorem Ordinal.nmul_succ
deleted theorem Ordinal.nmul_zero
deleted theorem Ordinal.one_nadd
deleted theorem Ordinal.one_nmul
deleted theorem Ordinal.succ_nadd
deleted theorem Ordinal.succ_nmul
deleted theorem Ordinal.toNatOrdinal_max
deleted theorem Ordinal.toNatOrdinal_min
deleted theorem Ordinal.toNatOrdinal_one
deleted theorem Ordinal.toNatOrdinal_zero
deleted theorem Ordinal.zero_nadd
deleted theorem Ordinal.zero_nmul
deleted theorem SetTheory.PGame.add_congr
deleted theorem SetTheory.PGame.down_neg
deleted def SetTheory.PGame.neg
deleted theorem SetTheory.PGame.neg_def
deleted theorem SetTheory.PGame.neg_down
deleted theorem SetTheory.PGame.neg_star
deleted theorem SetTheory.PGame.neg_up
deleted theorem SetTheory.PGame.sub_congr
deleted def SetTheory.PGame.up
deleted theorem SetTheory.PGame.up_neg
deleted inductive SetTheory.PGame.IsOption
deleted inductive SetTheory.PGame.Relabelling
deleted theorem SetTheory.PGame.ext
deleted inductive SetTheory.PGame
deleted theorem LE.le.not_gf
deleted theorem SetTheory.PGame.Equiv.ge
deleted theorem SetTheory.PGame.Equiv.le
deleted theorem SetTheory.PGame.LF.not_ge
deleted theorem SetTheory.PGame.LF.not_gt
deleted def SetTheory.PGame.LF
deleted theorem SetTheory.PGame.equiv_def
deleted theorem SetTheory.PGame.equiv_rfl
deleted theorem SetTheory.PGame.le_congr
deleted theorem SetTheory.PGame.le_def
deleted theorem SetTheory.PGame.le_or_gf
deleted theorem SetTheory.PGame.le_zero
deleted theorem SetTheory.PGame.lf_congr
deleted theorem SetTheory.PGame.lf_def
deleted theorem SetTheory.PGame.lf_irrefl
deleted theorem SetTheory.PGame.lf_mk
deleted theorem SetTheory.PGame.lf_of_lt
deleted theorem SetTheory.PGame.lf_zero
deleted theorem SetTheory.PGame.lt_congr
deleted theorem SetTheory.PGame.mk_le_mk
deleted theorem SetTheory.PGame.mk_lf
deleted theorem SetTheory.PGame.mk_lf_mk
deleted theorem SetTheory.PGame.not_lf
deleted theorem SetTheory.PGame.zero_le
deleted theorem SetTheory.PGame.zero_lf
deleted theorem SetTheory.PGame.le_of_lf
deleted theorem SetTheory.PGame.lf_asymm
deleted theorem SetTheory.PGame.lf_iff_lt
deleted theorem SetTheory.PGame.lt_def
deleted theorem SetTheory.PGame.lt_of_lf
deleted theorem SetTheory.PGame.not_fuzzy
deleted theorem Surreal.bddAbove_of_small
deleted theorem Surreal.bddBelow_of_small
deleted def Surreal.lift
deleted def Surreal.lift₂
deleted def Surreal.mk
deleted theorem Surreal.mk_add
deleted theorem Surreal.mk_eq_mk
deleted theorem Surreal.mk_eq_zero
deleted theorem Surreal.mk_le_mk
deleted theorem Surreal.mk_lt_mk
deleted theorem Surreal.mk_moveLeft_lt_mk
deleted theorem Surreal.mk_sub
deleted theorem Surreal.nat_toGame
deleted theorem Surreal.one_toGame
deleted def Surreal.toGame
deleted theorem Surreal.zero_def
deleted theorem Surreal.zero_le_mk
deleted theorem Surreal.zero_lt_mk
deleted theorem Surreal.zero_toGame
deleted def Surreal
deleted def Surreal.dyadic
deleted theorem Surreal.dyadicMap_apply
deleted theorem Surreal.dyadic_aux
deleted def Surreal.powHalf
deleted theorem Surreal.powHalf_zero
deleted theorem SetTheory.PGame.P24
deleted inductive Surreal.Multiplication.Args