Commit 2024-01-31 03:53 0a0bb6ec

View on Github →

feat: formalize IMO 1960 Q2 (#9885)

Estimated changes

Modified Archive.lean

Created Archive/Imo/Imo1960Q2.lean

added structure Imo1960Q2.IsGood

added theorem Imo1960Q2.isGood_iff