Commit 2023-08-31 07:47 404fef6a

View on Github →

chore: move Game to SetTheory.Game (#6365) move Game and PGame into namespace SetTheory as _root_.Game might collide with other definitions (e.g. in projects depending on mathlib)

Estimated changes

deleted def Game.Fuzzy
deleted def Game.Lf
deleted theorem Game.PGame.le_iff_game_le
deleted theorem Game.PGame.lf_iff_game_lf
deleted theorem Game.PGame.lt_iff_game_lt
deleted theorem Game.add_lf_add_left
deleted theorem Game.add_lf_add_right
deleted def Game.neg
deleted theorem Game.not_le
deleted theorem Game.not_lf
deleted inductive PGame.InvTy
deleted def PGame.inv'
deleted def PGame.inv'One
deleted def PGame.inv'Zero
deleted theorem PGame.inv'_one_equiv
deleted theorem PGame.inv'_zero_equiv
deleted def PGame.invOne
deleted def PGame.invVal
deleted theorem PGame.invVal_isEmpty
deleted theorem PGame.inv_eq_of_lf_zero
deleted theorem PGame.inv_eq_of_pos
deleted theorem PGame.inv_one_equiv
deleted theorem PGame.inv_zero
deleted theorem PGame.leftMoves_mul
deleted theorem PGame.leftMoves_mul_cases
deleted theorem PGame.left_distrib_equiv
deleted theorem PGame.mk_mul_moveLeft_inl
deleted theorem PGame.mk_mul_moveLeft_inr
deleted theorem PGame.mul_assoc_equiv
deleted theorem PGame.mul_comm_equiv
deleted theorem PGame.mul_moveLeft_inl
deleted theorem PGame.mul_moveLeft_inr
deleted theorem PGame.mul_moveRight_inl
deleted theorem PGame.mul_moveRight_inr
deleted theorem PGame.mul_one_equiv
deleted theorem PGame.mul_zero_equiv
deleted theorem PGame.one_mul_equiv
deleted theorem PGame.quot_add
deleted theorem PGame.quot_left_distrib
deleted theorem PGame.quot_mul_assoc
deleted theorem PGame.quot_mul_comm
deleted theorem PGame.quot_mul_neg
deleted theorem PGame.quot_mul_one
deleted theorem PGame.quot_mul_zero
deleted theorem PGame.quot_neg
deleted theorem PGame.quot_neg_mul
deleted theorem PGame.quot_one_mul
deleted theorem PGame.quot_right_distrib
deleted theorem PGame.quot_sub
deleted theorem PGame.quot_zero_mul
deleted theorem PGame.rightMoves_mul
deleted theorem PGame.right_distrib_equiv
deleted theorem PGame.zero_lf_inv'
deleted theorem PGame.zero_mul_equiv
added theorem SetTheory.Game.not_le
added theorem SetTheory.Game.not_lf
added inductive SetTheory.PGame.InvTy
deleted theorem PGame.birthday_add
deleted theorem PGame.birthday_add_nat
deleted theorem PGame.birthday_add_one
deleted theorem PGame.birthday_add_zero
deleted theorem PGame.birthday_def
deleted theorem PGame.birthday_eq_zero
deleted theorem PGame.birthday_nat_add
deleted theorem PGame.birthday_nat_cast
deleted theorem PGame.birthday_one
deleted theorem PGame.birthday_one_add
deleted theorem PGame.birthday_star
deleted theorem PGame.birthday_zero
deleted theorem PGame.birthday_zero_add
deleted theorem PGame.le_birthday
deleted theorem PGame.lt_birthday_iff
deleted theorem PGame.neg_birthday
deleted theorem PGame.neg_birthday_le
deleted theorem PGame.toPGame_birthday
deleted def PGame.domineering.L
deleted def PGame.domineering
deleted theorem PGame.Impartial.add_self
deleted theorem PGame.Impartial.nonneg
deleted theorem PGame.Impartial.nonpos
deleted def PGame.ImpartialAux
deleted theorem PGame.impartialAux_def
deleted theorem PGame.impartial_def
deleted theorem PGame.impartial_iff_aux
deleted theorem PGame.grundyValue_add
deleted theorem PGame.grundyValue_neg
deleted theorem PGame.grundyValue_star
deleted theorem PGame.grundyValue_zero
deleted theorem PGame.leftMoves_nim
deleted theorem PGame.moveLeft_nim'
deleted theorem PGame.moveLeft_nim
deleted theorem PGame.moveLeft_nim_hEq
deleted theorem PGame.moveRight_nim'
deleted theorem PGame.moveRight_nim
deleted theorem PGame.moveRight_nim_hEq
deleted theorem PGame.neg_nim
deleted theorem PGame.nim_add_nim_equiv
deleted theorem PGame.nim_birthday
deleted theorem PGame.nim_def
deleted theorem PGame.nim_equiv_iff_eq
deleted theorem PGame.nim_grundyValue
deleted theorem PGame.nim_one_equiv
deleted theorem PGame.nim_one_moveLeft
deleted theorem PGame.nim_one_moveRight
deleted theorem PGame.nim_zero_equiv
deleted theorem PGame.rightMoves_nim
deleted theorem PGame.Equiv.ge
deleted theorem PGame.Equiv.isEmpty
deleted theorem PGame.Equiv.le
deleted theorem PGame.Equiv.not_fuzzy'
deleted theorem PGame.Equiv.not_fuzzy
deleted def PGame.Equiv
deleted theorem PGame.Fuzzy.not_equiv'
deleted theorem PGame.Fuzzy.not_equiv
deleted theorem PGame.Fuzzy.swap
deleted theorem PGame.Fuzzy.swap_iff
deleted def PGame.Fuzzy
deleted theorem PGame.IsOption.mk_left
deleted theorem PGame.IsOption.mk_right
deleted inductive PGame.IsOption
deleted def PGame.LeftMoves
deleted theorem PGame.Lf.not_equiv'
deleted theorem PGame.Lf.not_equiv
deleted theorem PGame.Lf.not_ge
deleted theorem PGame.Lf.not_gt
deleted def PGame.Lf
deleted theorem PGame.Relabelling.equiv
deleted theorem PGame.Relabelling.ge
deleted theorem PGame.Relabelling.le
deleted inductive PGame.Relabelling
deleted def PGame.RightMoves
deleted theorem PGame.Subsequent.mk_left
deleted theorem PGame.Subsequent.mk_right
deleted theorem PGame.Subsequent.moveLeft
deleted theorem PGame.Subsequent.trans
deleted def PGame.Subsequent
deleted theorem PGame.add_assoc_equiv
deleted theorem PGame.add_comm_equiv
deleted theorem PGame.add_comm_le
deleted theorem PGame.add_congr
deleted theorem PGame.add_congr_left
deleted theorem PGame.add_congr_right
deleted theorem PGame.add_left_neg_equiv
deleted theorem PGame.add_lf_add_left
deleted theorem PGame.add_lf_add_right
deleted theorem PGame.add_moveLeft_inl
deleted theorem PGame.add_moveLeft_inr
deleted theorem PGame.add_moveRight_inl
deleted theorem PGame.add_moveRight_inr
deleted theorem PGame.add_right_neg_equiv
deleted theorem PGame.add_zero_equiv
deleted theorem PGame.equiv_congr_left
deleted theorem PGame.equiv_congr_right
deleted theorem PGame.equiv_of_eq
deleted theorem PGame.equiv_of_mk_equiv
deleted theorem PGame.equiv_refl
deleted theorem PGame.equiv_rfl
deleted theorem PGame.fuzzy_congr
deleted theorem PGame.fuzzy_congr_imp
deleted theorem PGame.fuzzy_congr_left
deleted theorem PGame.fuzzy_congr_right
deleted theorem PGame.fuzzy_irrefl
deleted theorem PGame.isOption_neg
deleted theorem PGame.isOption_neg_neg
deleted theorem PGame.le_congr
deleted theorem PGame.le_congr_imp
deleted theorem PGame.le_congr_left
deleted theorem PGame.le_congr_right
deleted theorem PGame.le_def
deleted theorem PGame.le_iff_forall_lf
deleted theorem PGame.le_iff_sub_nonneg
deleted theorem PGame.le_neg_iff
deleted theorem PGame.le_of_equiv_of_le
deleted theorem PGame.le_of_forall_lf
deleted theorem PGame.le_of_forall_lt
deleted theorem PGame.le_of_le_of_equiv
deleted theorem PGame.le_or_gf
deleted theorem PGame.le_zero
deleted theorem PGame.le_zero_lf
deleted theorem PGame.leftMoves_add
deleted theorem PGame.leftMoves_add_cases
deleted theorem PGame.leftMoves_mk
deleted theorem PGame.leftMoves_neg
deleted theorem PGame.leftMoves_ofLists
deleted theorem PGame.leftResponse_spec
deleted theorem PGame.lf_congr
deleted theorem PGame.lf_congr_imp
deleted theorem PGame.lf_congr_left
deleted theorem PGame.lf_congr_right
deleted theorem PGame.lf_def
deleted theorem PGame.lf_iff_exists_le
deleted theorem PGame.lf_iff_lt_or_fuzzy
deleted theorem PGame.lf_iff_sub_zero_lf
deleted theorem PGame.lf_irrefl
deleted theorem PGame.lf_mk
deleted theorem PGame.lf_mk_of_le
deleted theorem PGame.lf_moveRight
deleted theorem PGame.lf_moveRight_of_le
deleted theorem PGame.lf_neg_iff
deleted theorem PGame.lf_of_equiv_of_lf
deleted theorem PGame.lf_of_fuzzy
deleted theorem PGame.lf_of_le_mk
deleted theorem PGame.lf_of_le_moveLeft
deleted theorem PGame.lf_of_le_of_lf
deleted theorem PGame.lf_of_lf_of_equiv
deleted theorem PGame.lf_of_lf_of_le
deleted theorem PGame.lf_of_lf_of_lt
deleted theorem PGame.lf_of_lt
deleted theorem PGame.lf_of_lt_of_lf
deleted theorem PGame.lf_of_mk_le
deleted theorem PGame.lf_of_moveRight_le
deleted theorem PGame.lf_or_equiv_or_gf
deleted theorem PGame.lf_zero
deleted theorem PGame.lf_zero_le
deleted theorem PGame.lt_congr
deleted theorem PGame.lt_congr_imp
deleted theorem PGame.lt_congr_left
deleted theorem PGame.lt_congr_right
deleted theorem PGame.lt_iff_le_and_lf
deleted theorem PGame.lt_iff_sub_pos
deleted theorem PGame.lt_neg_iff
deleted theorem PGame.lt_of_equiv_of_lt
deleted theorem PGame.lt_of_le_of_lf
deleted theorem PGame.lt_of_lt_of_equiv
deleted theorem PGame.lt_or_equiv_of_le
deleted theorem PGame.lt_or_equiv_or_gf
deleted theorem PGame.lt_or_fuzzy_of_lf
deleted theorem PGame.mk_add_moveLeft_inl
deleted theorem PGame.mk_add_moveLeft_inr
deleted theorem PGame.mk_le_mk
deleted theorem PGame.mk_lf
deleted theorem PGame.mk_lf_mk
deleted theorem PGame.mk_lf_of_le
deleted def PGame.moveLeft
deleted theorem PGame.moveLeft_lf
deleted theorem PGame.moveLeft_lf_of_le
deleted theorem PGame.moveLeft_mk
deleted theorem PGame.moveLeft_neg'
deleted theorem PGame.moveLeft_neg
deleted theorem PGame.moveLeft_neg_symm'
deleted theorem PGame.moveLeft_neg_symm
deleted def PGame.moveRecOn
deleted def PGame.moveRight
deleted theorem PGame.moveRight_mk
deleted theorem PGame.moveRight_neg'
deleted theorem PGame.moveRight_neg
deleted theorem PGame.moveRight_neg_symm'
deleted theorem PGame.moveRight_neg_symm
deleted def PGame.neg
deleted theorem PGame.neg_add_le
deleted theorem PGame.neg_def
deleted theorem PGame.neg_equiv_iff
deleted theorem PGame.neg_equiv_neg_iff
deleted theorem PGame.neg_equiv_zero_iff
deleted theorem PGame.neg_fuzzy_iff
deleted theorem PGame.neg_fuzzy_neg_iff
deleted theorem PGame.neg_fuzzy_zero_iff
deleted theorem PGame.neg_le_iff
deleted theorem PGame.neg_le_neg_iff
deleted theorem PGame.neg_le_zero_iff
deleted theorem PGame.neg_lf_iff
deleted theorem PGame.neg_lf_neg_iff
deleted theorem PGame.neg_lf_zero_iff
deleted theorem PGame.neg_lt_iff
deleted theorem PGame.neg_lt_neg_iff
deleted theorem PGame.neg_lt_zero_iff
deleted theorem PGame.neg_ofLists
deleted theorem PGame.neg_star
deleted theorem PGame.not_fuzzy_of_ge
deleted theorem PGame.not_fuzzy_of_le
deleted theorem PGame.not_lf
deleted def PGame.ofLists
deleted theorem PGame.ofLists_moveLeft'
deleted theorem PGame.ofLists_moveLeft
deleted theorem PGame.ofLists_moveRight'
deleted theorem PGame.ofLists_moveRight
deleted theorem PGame.one_leftMoves
deleted theorem PGame.one_moveLeft
deleted theorem PGame.one_rightMoves
deleted def PGame.relabel
deleted theorem PGame.relabel_moveLeft'
deleted theorem PGame.relabel_moveLeft
deleted theorem PGame.relabel_moveRight'
deleted theorem PGame.relabel_moveRight
deleted theorem PGame.rightMoves_add
deleted theorem PGame.rightMoves_mk
deleted theorem PGame.rightMoves_neg
deleted theorem PGame.rightMoves_ofLists
deleted theorem PGame.rightResponse_spec
deleted def PGame.star
deleted theorem PGame.star_fuzzy_zero
deleted theorem PGame.star_leftMoves
deleted theorem PGame.star_moveLeft
deleted theorem PGame.star_moveRight
deleted theorem PGame.star_rightMoves
deleted theorem PGame.sub_congr
deleted theorem PGame.sub_congr_left
deleted theorem PGame.sub_congr_right
deleted theorem PGame.sub_self_equiv
deleted theorem PGame.sub_zero
deleted theorem PGame.wf_isOption
deleted theorem PGame.wf_subsequent
deleted theorem PGame.zero_add_equiv
deleted theorem PGame.zero_equiv_neg_iff
deleted theorem PGame.zero_fuzzy_neg_iff
deleted theorem PGame.zero_le
deleted theorem PGame.zero_le_lf
deleted theorem PGame.zero_le_neg_iff
deleted theorem PGame.zero_leftMoves
deleted theorem PGame.zero_lf
deleted theorem PGame.zero_lf_le
deleted theorem PGame.zero_lf_neg_iff
deleted theorem PGame.zero_lf_one
deleted theorem PGame.zero_lt_neg_iff
deleted theorem PGame.zero_rightMoves
deleted inductive PGame
added inductive SetTheory.PGame.IsOption
added theorem SetTheory.PGame.le_def
added theorem SetTheory.PGame.lf_def
added theorem SetTheory.PGame.lf_mk
added theorem SetTheory.PGame.mk_lf
added theorem SetTheory.PGame.not_lf
added inductive SetTheory.PGame
deleted def PGame.Short.mk'
deleted inductive PGame.Short
deleted def PGame.fintypeLeft
deleted def PGame.fintypeRight
deleted def PGame.leLfDecidable
deleted theorem PGame.short_birthday
added inductive SetTheory.PGame.Short
deleted def Game.ofState
deleted def PGame.ofState
deleted def PGame.ofStateAux
deleted theorem PGame.turnBound_of_left
deleted theorem PGame.turnBound_of_right
deleted theorem PGame.Numeric.add
deleted theorem PGame.Numeric.mk
deleted theorem PGame.Numeric.moveLeft
deleted theorem PGame.Numeric.moveLeft_le
deleted theorem PGame.Numeric.moveLeft_lt
deleted theorem PGame.Numeric.moveRight
deleted theorem PGame.Numeric.neg
deleted theorem PGame.Numeric.sub
deleted def PGame.Numeric
deleted theorem PGame.le_iff_forall_lt
deleted theorem PGame.le_of_lf
deleted theorem PGame.lf_asymm
deleted theorem PGame.lf_iff_lt
deleted theorem PGame.lt_def
deleted theorem PGame.lt_iff_exists_le
deleted theorem PGame.lt_of_exists_le
deleted theorem PGame.lt_of_lf
deleted theorem PGame.lt_or_equiv_or_gt
deleted theorem PGame.not_fuzzy
deleted theorem PGame.numeric_def
deleted theorem PGame.numeric_nat
deleted theorem PGame.numeric_of_isEmpty
deleted theorem PGame.numeric_one
deleted theorem PGame.numeric_rec
deleted theorem PGame.numeric_toPGame
deleted theorem PGame.numeric_zero
added theorem SetTheory.PGame.lt_def
deleted theorem PGame.birthday_half
deleted theorem PGame.numeric_powHalf
deleted def PGame.powHalf
deleted theorem PGame.powHalf_le_one
deleted theorem PGame.powHalf_leftMoves
deleted theorem PGame.powHalf_moveLeft
deleted theorem PGame.powHalf_pos
deleted theorem PGame.powHalf_succ_lt_one
deleted theorem PGame.powHalf_zero
deleted theorem PGame.zero_le_powHalf