Commit 2023-09-16 08:38 96806534

View on Github →

chore: fix name *.Lf (#7163)

Estimated changes

Modified Mathlib/SetTheory/Game/Basic.lean

added def SetTheory.Game.LF

deleted def SetTheory.Game.Lf

modified theorem SetTheory.Game.PGame.lf_iff_game_lf

Modified Mathlib/SetTheory/Game/PGame.lean

added theorem SetTheory.PGame.LF.not_equiv'

added theorem SetTheory.PGame.LF.not_equiv

added theorem SetTheory.PGame.LF.not_ge

added theorem SetTheory.PGame.LF.not_gt

added def SetTheory.PGame.LF

deleted theorem SetTheory.PGame.Lf.not_equiv'

deleted theorem SetTheory.PGame.Lf.not_equiv

deleted theorem SetTheory.PGame.Lf.not_ge

deleted theorem SetTheory.PGame.Lf.not_gt

deleted def SetTheory.PGame.Lf

Modified Mathlib/SetTheory/Game/Short.lean

added def SetTheory.PGame.leLFDecidable

deleted def SetTheory.PGame.leLfDecidable

Modified Mathlib/SetTheory/Surreal/Basic.lean