Theorem Ordinal.mk_toPGame

Modification history

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 →