Commit 2023-06-27 07:58 bf1157dd

View on Github →

feat: port SetTheory.Game.Impartial (#5517)

Estimated changes

Modified Mathlib.lean

Created Mathlib/SetTheory/Game/Impartial.lean

added theorem PGame.Impartial.add_self

added theorem PGame.Impartial.equiv_iff_add_equiv_zero'

added theorem PGame.Impartial.equiv_iff_add_equiv_zero

added theorem PGame.Impartial.equiv_or_fuzzy_zero

added theorem PGame.Impartial.equiv_zero_iff_ge

added theorem PGame.Impartial.equiv_zero_iff_le

added theorem PGame.Impartial.exists_left_move_equiv_iff_fuzzy_zero

added theorem PGame.Impartial.exists_right_move_equiv_iff_fuzzy_zero

added theorem PGame.Impartial.forall_leftMoves_fuzzy_iff_equiv_zero

added theorem PGame.Impartial.forall_rightMoves_fuzzy_iff_equiv_zero

added theorem PGame.Impartial.fuzzy_zero_iff_gf

added theorem PGame.Impartial.fuzzy_zero_iff_lf

added theorem PGame.Impartial.impartial_congr

added theorem PGame.Impartial.le_zero_iff

added theorem PGame.Impartial.lf_zero_iff

added theorem PGame.Impartial.mk'_add_self

added theorem PGame.Impartial.mk'_neg_equiv_self

added theorem PGame.Impartial.neg_equiv_self

added theorem PGame.Impartial.nonneg

added theorem PGame.Impartial.nonpos

added theorem PGame.Impartial.not_equiv_zero_iff

added theorem PGame.Impartial.not_fuzzy_zero_iff

added def PGame.ImpartialAux

added theorem PGame.impartialAux_def

added theorem PGame.impartial_def

added theorem PGame.impartial_iff_aux