Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-09 02:37 4f386e66

View on Github →

feat(set_theory/pgame/birthday): Birthdays of ordinals (#13714)

Estimated changes

Modified src/set_theory/game/birthday.lean

added theorem pgame.le_birthday

added theorem pgame.neg_birthday

added theorem pgame.neg_birthday_le

added theorem pgame.to_pgame_birthday

Modified src/set_theory/game/ordinal.lean