Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-27 23:19 6585eff9

View on Github →

feat(archive/imo): formalize IMO 2013 problem Q5 (#5787)

Estimated changes

added theorem f_pos_of_pos
added theorem fixed_point_of_gt_1
added theorem fx_gt_xm1
added theorem imo2013_q5
added theorem le_of_all_pow_lt_succ'
added theorem le_of_all_pow_lt_succ
added theorem pow_f_le_f_pow