Theorem Ordinal.toGame_lt_iff

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_lt_iffView on Github →