Commit 2024-09-16 17:23 db1926d7

View on Github →

feat(SetTheory/Game/Birthday): Define birthday of a game (#15716) The updated module description explains how this differs from the birthday of a pre-game.

Estimated changes

Modified Mathlib/SetTheory/Game/Basic.lean

added theorem SetTheory.Game.zero_def

added theorem SetTheory.PGame.quot_natCast

Modified Mathlib/SetTheory/Game/Birthday.lean

added theorem SetTheory.Game.birthday_add_le

added theorem SetTheory.Game.birthday_eq_pGameBirthday

added theorem SetTheory.Game.birthday_eq_zero

added theorem SetTheory.Game.birthday_natCast

added theorem SetTheory.Game.birthday_neg

added theorem SetTheory.Game.birthday_ofNat

added theorem SetTheory.Game.birthday_one

added theorem SetTheory.Game.birthday_ordinalToGame

added theorem SetTheory.Game.birthday_quot_le_pGameBirthday

added theorem SetTheory.Game.birthday_star

added theorem SetTheory.Game.birthday_sub_le

added theorem SetTheory.Game.birthday_zero

added theorem SetTheory.Game.le_birthday

added theorem SetTheory.Game.neg_birthday_le

modified theorem SetTheory.PGame.birthday_add

deleted theorem SetTheory.PGame.birthday_add_nat

deleted theorem SetTheory.PGame.birthday_add_one

deleted theorem SetTheory.PGame.birthday_add_zero

deleted theorem SetTheory.PGame.birthday_nat_add

added theorem SetTheory.PGame.birthday_neg

deleted theorem SetTheory.PGame.birthday_one_add

added theorem SetTheory.PGame.birthday_ordinalToPGame

added theorem SetTheory.PGame.birthday_sub

deleted theorem SetTheory.PGame.birthday_zero_add

deleted theorem SetTheory.PGame.neg_birthday

deleted theorem SetTheory.PGame.toPGame_birthday

Modified Mathlib/SetTheory/Game/Ordinal.lean

added theorem Ordinal.toGame_natCast

added theorem Ordinal.toPGame_natCast

Modified Mathlib/SetTheory/Game/PGame.lean

Modified Mathlib/SetTheory/Ordinal/NaturalOps.lean