ordinal): API for casting ordinals into games
#18703

Open

feat(set_theory/game/ordinal): API for casting ordinals into games #18703

vihdzp wants to merge 4 commits into master from to_pgame_more_lemmas_p1

split off

011f981b

vihdzp added awaiting-review

vihdzp requested a review from

astrainfinita 2 years ago

vihdzp changed the title ~~feat(set_theory/game/ordinal): addition of ordinal games corresponds with natural ordinal addition~~ feat(set_theory/game/ordinal): API for casting ordinals into games 2 years ago

fix

0efd925d

fix

73868a40

eric-wieser commented on 2023-03-31

eric-wieser removed awaiting-review

eric-wieser added awaiting-author

apply suggestions

bb63d6b5

kim-em added too-late

Reviewers

eric-wieser

astrainfinita

Assignees

No one assigned

Labels

awaiting-author too-late

Milestone

No milestone

mathlib3 feat(set_theory/game/ordinal): API for casting ordinals into games #18703 Open

feat(set_theory/game/ordinal): API for casting ordinals into games #18703

mathlib3
feat(set_theory/game/ordinal): API for casting ordinals into games
#18703

Open