Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-24 19:36 2ecd65e6

View on Github →

feat(archive/imo): IMO 2001 Q2 (#7238) Formalization of IMO 2001/2

Estimated changes

added theorem bound
added theorem denom_pos
added theorem imo2001_q2'
added theorem imo2001_q2