Commit 2024-09-06 17:25 247ff18e

View on Github →

chore(SetTheory/Game/Impartial): cleanup proofs (#16517) We clean up remnants of the Lean 3 termination_by syntax, as well as some exposed setoid API.

Estimated changes

Modified Mathlib/SetTheory/Game/Basic.lean

modified theorem SetTheory.PGame.quot_add

modified theorem SetTheory.PGame.quot_mul_zero

modified theorem SetTheory.PGame.quot_neg

added theorem SetTheory.PGame.quot_one

modified theorem SetTheory.PGame.quot_sub

added theorem SetTheory.PGame.quot_zero

modified theorem SetTheory.PGame.quot_zero_mul

Modified Mathlib/SetTheory/Game/Impartial.lean

modified theorem SetTheory.PGame.Impartial.impartial_congr

modified theorem SetTheory.PGame.Impartial.mk'_add_self

modified theorem SetTheory.PGame.Impartial.mk'_neg_equiv_self

modified theorem SetTheory.PGame.Impartial.nonneg

modified theorem SetTheory.PGame.Impartial.nonpos

modified def SetTheory.PGame.ImpartialAux

modified theorem SetTheory.PGame.impartialAux_def