Commit 2024-08-12 22:22 7a462dc8

View on Github →

feat(SetTheory/Game/Ordinal): game product of ordinals is natural product (#15690) I also flipped and renamed toPGame_nadd at the request of Yaël.

Estimated changes

Modified Mathlib/SetTheory/Game/Basic.lean

Modified Mathlib/SetTheory/Game/Ordinal.lean

added theorem Ordinal.toGame_nadd

added theorem Ordinal.toGame_nmul

deleted theorem Ordinal.toPGame_add

deleted theorem Ordinal.toPGame_add_mk'

added theorem Ordinal.toPGame_nadd

added theorem Ordinal.toPGame_nmul