Commit 2023-06-28 10:21 3aa8632a

View on Github →

feat: port SetTheory.Game.Birthday (#5500)

Estimated changes

Modified Mathlib.lean

Created Mathlib/SetTheory/Game/Birthday.lean

added theorem PGame.Relabelling.birthday_congr

added theorem PGame.birthday_add

added theorem PGame.birthday_add_nat

added theorem PGame.birthday_add_one

added theorem PGame.birthday_add_zero

added theorem PGame.birthday_def

added theorem PGame.birthday_eq_zero

added theorem PGame.birthday_moveLeft_lt

added theorem PGame.birthday_moveRight_lt

added theorem PGame.birthday_nat_add

added theorem PGame.birthday_nat_cast

added theorem PGame.birthday_one

added theorem PGame.birthday_one_add

added theorem PGame.birthday_star

added theorem PGame.birthday_zero

added theorem PGame.birthday_zero_add

added theorem PGame.le_birthday

added theorem PGame.lt_birthday_iff

added theorem PGame.neg_birthday

added theorem PGame.neg_birthday_le

added theorem PGame.toPGame_birthday