Theorem Ordinal.toPGame_nmul

Modification history

2024-11-14 00:03

Mathlib/SetTheory/Game/Ordinal.lean

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

Modified Ordinal.toPGame_nmul View on Github →

2024-08-12 22:22

Mathlib/SetTheory/Game/Ordinal.lean

feat(SetTheory/Game/Ordinal): game product of ordinals is natural product (#15690) …

Added Ordinal.toPGame_nmul View on Github →