Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2022-06-27 03:03
0b18823c
View on Github →
feat(set_theory/game/pgame): make
lt_iff_le_and_lf
true by def-eq (
#14983
)
Estimated changes
Modified
src/set_theory/game/basic.lean
Modified
src/set_theory/game/ordinal.lean
Modified
src/set_theory/game/pgame.lean
modified
theorem
pgame.lf_of_lt
modified
theorem
pgame.lt_iff_le_and_lf
modified
theorem
pgame.lt_of_le_of_lf
Modified
src/set_theory/game/short.lean
Modified
src/set_theory/surreal/basic.lean