Commit 2023-06-26 05:06 1bd4b776

View on Github →

feat: port SetTheory.Game.Basic (#4311)

Estimated changes

Modified Mathlib.lean

Created Mathlib/SetTheory/Game/Basic.lean

added def Game.Fuzzy

added def Game.Lf

added theorem Game.PGame.equiv_iff_game_eq

added theorem Game.PGame.fuzzy_iff_game_fuzzy

added theorem Game.PGame.le_iff_game_le

added theorem Game.PGame.lf_iff_game_lf

added theorem Game.PGame.lt_iff_game_lt

added theorem Game.add_lf_add_left

added theorem Game.add_lf_add_right

added def Game.neg

added theorem Game.not_le

added theorem Game.not_lf

added inductive PGame.InvTy

added def PGame.inv'

added def PGame.inv'One

added def PGame.inv'Zero

added theorem PGame.inv'_one_equiv

added theorem PGame.inv'_zero_equiv

added def PGame.invOne

added def PGame.invVal

added theorem PGame.invVal_isEmpty

added theorem PGame.inv_eq_of_equiv_zero

added theorem PGame.inv_eq_of_lf_zero

added theorem PGame.inv_eq_of_pos

added theorem PGame.inv_one_equiv

added theorem PGame.inv_zero

added theorem PGame.leftMoves_mul

added theorem PGame.leftMoves_mul_cases

added theorem PGame.left_distrib_equiv

added theorem PGame.mk_mul_moveLeft_inl

added theorem PGame.mk_mul_moveLeft_inr

added theorem PGame.mk_mul_moveRight_inl

added theorem PGame.mk_mul_moveRight_inr

added def PGame.mulCommRelabelling

added def PGame.mulNegRelabelling

added def PGame.mulOneRelabelling

added def PGame.mulZeroRelabelling

added theorem PGame.mul_assoc_equiv

added theorem PGame.mul_comm_equiv

added theorem PGame.mul_moveLeft_inl

added theorem PGame.mul_moveLeft_inr

added theorem PGame.mul_moveRight_inl

added theorem PGame.mul_moveRight_inr

added theorem PGame.mul_one_equiv

added theorem PGame.mul_zero_equiv

added def PGame.negMulRelabelling

added theorem PGame.neg_mk_mul_moveLeft_inl

added theorem PGame.neg_mk_mul_moveLeft_inr

added theorem PGame.neg_mk_mul_moveRight_inl

added theorem PGame.neg_mk_mul_moveRight_inr

added def PGame.oneMulRelabelling

added theorem PGame.one_mul_equiv

added theorem PGame.quot_add

added theorem PGame.quot_eq_of_mk'_quot_eq

added theorem PGame.quot_left_distrib

added theorem PGame.quot_left_distrib_sub

added theorem PGame.quot_mul_assoc

added theorem PGame.quot_mul_comm

added theorem PGame.quot_mul_neg

added theorem PGame.quot_mul_one

added theorem PGame.quot_mul_zero

added theorem PGame.quot_neg

added theorem PGame.quot_neg_mul

added theorem PGame.quot_one_mul

added theorem PGame.quot_right_distrib

added theorem PGame.quot_right_distrib_sub

added theorem PGame.quot_sub

added theorem PGame.quot_zero_mul

added theorem PGame.rightMoves_mul

added theorem PGame.rightMoves_mul_cases

added theorem PGame.right_distrib_equiv

added def PGame.toLeftMovesMul

added def PGame.toRightMovesMul

added def PGame.zeroMulRelabelling

added theorem PGame.zero_lf_inv'

added theorem PGame.zero_mul_equiv

Modified Mathlib/SetTheory/Game/PGame.lean