Commit 2022-05-06 15:42 40bedd62

View on Github →

refactor(set_theory/game/pgame): Remove pgame.omega (#13960) This barely had any API to begin with. Thanks to ordinal.to_pgame, it is now entirely redundant.

Estimated changes

Modified src/set_theory/game/pgame.lean

deleted def pgame.omega

Modified src/set_theory/game/winner.lean

deleted theorem pgame.omega_left_wins

Modified src/set_theory/surreal/basic.lean

deleted theorem pgame.numeric_omega