Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-03-23 10:21 dc9e5ba6

View on Github →

chore(set_theory/game/pgame): golf le and lf basic API (#18498)

Estimated changes

deleted def pgame.le_lf
modified theorem pgame.lf.not_ge
modified def pgame.lf
modified theorem pgame.not_lf