Commit 2025-01-02 23:22 ba6854b0
View on Github →chore(SetTheory/Game/Ordinal): make Ordinal.toGame an order embedding (#19417)
The original reasoning against doing this was that it would disable dot notation, which is no longer an issue in the latest version of Lean.