Theorem Ordinal.toPGame_one

Modification history

2026-02-20 00:22

Mathlib/SetTheory/Game/Ordinal.lean

chore: remove deprecated material from CGT (#35550) …

Deleted Ordinal.toPGame_one View on Github →

2024-11-14 00:03

Mathlib/SetTheory/Game/Ordinal.lean

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

Added Ordinal.toPGame_one View on Github →