Theorem Ordinal.toGame_inj

Modification history

2025-01-02 23:22

Mathlib/SetTheory/Game/Ordinal.lean

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

Modified Ordinal.toGame_inj View on Github →

2024-12-30 10:07

Mathlib/SetTheory/Game/Ordinal.lean

chore: Rename injectivity theorems for consistency (#20329) …

Added Ordinal.toGame_inj View on Github →