Commit 2024-11-14 00:03 85ec5bfd

View on Github →

feat(SetTheory/Game/Birthday): basic API for Ordinal.toGame (#17015)

Estimated changes

added theorem Ordinal.toGame_eq_iff
added theorem Ordinal.toGame_le_iff
added theorem Ordinal.toGame_lf_iff
added theorem Ordinal.toGame_lt_iff
added theorem Ordinal.toGame_one
added theorem Ordinal.toGame_zero
modified theorem Ordinal.toPGame_nadd
modified theorem Ordinal.toPGame_nmul
added theorem Ordinal.toPGame_one
added theorem Ordinal.toPGame_zero