Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-07 10:30 a6024f10

View on Github →

feat(archive/imo): formalize IMO 2008 Q4 (#7039) feat(archive/imo): formalize IMO 2008 Q4

Estimated changes

Created archive/imo/imo2008_q4.lean

added theorem abs_eq_one_of_pow_eq_one

added theorem imo2008_q4