Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2022-04-25 03:54
65edf255
View on Github →
feat(set_theory/game/pgame):
x.move_left i < x
and variants (
#13654
)
Estimated changes
Modified
src/set_theory/game/pgame.lean
added
theorem
pgame.lt_mk
added
theorem
pgame.lt_move_right
added
theorem
pgame.mk_lt
added
theorem
pgame.move_left_lt
Modified
src/set_theory/surreal/basic.lean
deleted
theorem
pgame.numeric.lt_move_right
deleted
theorem
pgame.numeric.move_left_lt
Modified
src/set_theory/surreal/dyadic.lean