Theorem Ordinal.mk_toPGame

Modification history

2026-02-20 00:22

Mathlib/SetTheory/Game/Ordinal.lean

chore: remove deprecated material from CGT (#35550) …

Deleted Ordinal.mk_toPGame View on Github →

2025-01-02 23:22

Mathlib/SetTheory/Game/Ordinal.lean

chore(SetTheory/Game/Ordinal): make `Ordinal.toGame` an order embedding (#19417) …

Added Ordinal.mk_toPGame View on Github →