Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-22 23:41 684587b0

View on Github →

feat(set_theory/game/pgame): add_lf_add_of_lf_of_le (#14150) This generalizes the previously existing add_lf_add on numeric games.

Estimated changes

Modified src/set_theory/game/pgame.lean

added theorem pgame.add_lf_add_of_le_of_lf

added theorem pgame.add_lf_add_of_lf_of_le

Modified src/set_theory/surreal/basic.lean

deleted theorem pgame.add_lf_add