pgame): Remove `pgame.omega` (#13960)

Commit

3 years ago

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.

Author

vihdzp

Parents

c9f5cee2

mathlib 40bedd62 - refactor(set_theory/game/pgame): Remove `pgame.omega` (#13960)

mathlib
40bedd62 - refactor(set_theory/game/pgame): Remove `pgame.omega` (#13960)