Theorem Ordinal.toPGame_add

Modification history

2024-08-12 22:22

Mathlib/SetTheory/Game/Ordinal.lean

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

Deleted Ordinal.toPGame_add View on Github →

2023-06-26 14:46

Mathlib/SetTheory/Game/Ordinal.lean

feat: port SetTheory.Game.Ordinal (#5480)

Added Ordinal.toPGame_add View on Github →