Commit 2024-07-14 01:52 2d55389b

View on Github →

fix(SetTheory/Game/Basic): Fix the definition of surreal inverse (#14463) fix the definition of surreal inverse

Estimated changes

Modified Mathlib/SetTheory/Game/Basic.lean

modified def SetTheory.PGame.invVal

modified theorem SetTheory.PGame.invVal_isEmpty