ordinal): golf `to_pgame_injective` (#14661)

Commit

3 years ago

feat(set_theory/game/ordinal): golf `to_pgame_injective` (#14661) We also add the `eq_iff` version and remove an outdated todo comment.

Author

vihdzp

Parents