Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-03-27 13:45 728baa2f

View on Github →

feat(archive/imo/imo2006_q5): IMO 2006 Q5 (#15613) See module docstring for a thorough explanation of the proof.

Estimated changes

Created archive/imo/imo2006_q5.lean

added theorem imo2006_q5'

added theorem imo2006_q5

added theorem int.add_eq_add_of_nat_abs_eq_of_nat_abs_eq

added theorem int.nat_abs_eq_of_chain_dvd

added theorem polynomial.is_periodic_pt_eval_two

added theorem polynomial.iterate_comp_sub_X_ne

Modified src/data/int/basic.lean

added theorem int.sign_coe_add_one

added theorem int.sign_neg_succ_of_nat

Modified src/data/int/order/basic.lean

added theorem int.sign_add_eq_of_sign_eq

Modified src/data/list/cycle.lean

added theorem cycle.mem_map

Modified src/data/polynomial/degree/lemmas.lean

added theorem polynomial.nat_degree_iterate_comp

Modified src/data/polynomial/eval.lean

added theorem polynomial.iterate_comp_eval

added theorem polynomial.iterate_comp_eval₂