Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-20 14:41 15b14619

View on Github →

feat(archive/imo): IMO 2006 Q3 (#8052) Formalization of IMO 2006/3

Estimated changes

added theorem four_pow_four_pos
added theorem imo2006_q3
added theorem lhs_identity
added theorem lhs_ineq
added theorem mid_ineq
added theorem proof₁
added theorem proof₂
added theorem rhs_ineq
added theorem subst_proof₁
added theorem subst_wlog
added theorem zero_lt_32
added theorem mul_nonneg_of_three