Commit 2023-03-29 01:18 074dad72

View on Github →

feat: port IMO 2006 Q5 helper results (#3136) We don't port the IMO proof itself since it seems there's no archive in Mathlib4. Mathlib 3: https://github.com/leanprover-community/mathlib/pull/15613

Estimated changes

Modified Mathlib/Data/Int/Basic.lean

added theorem Int.sign_coe_add_one

added theorem Int.sign_negSucc

Modified Mathlib/Data/Int/Order/Basic.lean

added theorem Int.sign_add_eq_of_sign_eq

Modified Mathlib/Data/List/Cycle.lean

added theorem Cycle.mem_map

Modified Mathlib/Data/Polynomial/Degree/Lemmas.lean

added theorem Polynomial.natDegree_iterate_comp

Modified Mathlib/Data/Polynomial/Eval.lean

added theorem Polynomial.iterate_comp_eval₂