Theorem Ordinal.toGame_zero

Modification history

2024-11-14 00:03

Mathlib/SetTheory/Game/Ordinal.lean

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

Added Ordinal.toGame_zero View on Github →