Commit 2023-06-17 11:16 5d8d41fa

View on Github →

feat: port Archive.Imo.Imo2006Q5 (#5178)

Estimated changes

Modified Archive.lean

Created Archive/Imo/Imo2006Q5.lean

added theorem Imo2006Q5.Int.add_eq_add_of_natAbs_eq_of_natAbs_eq

added theorem Imo2006Q5.Int.natAbs_eq_of_chain_dvd

added theorem Imo2006Q5.Polynomial.isPeriodicPt_eval_two

added theorem Imo2006Q5.Polynomial.iterate_comp_sub_X_ne

added theorem Imo2006Q5.imo2006_q5'

added theorem imo2006_q5

Modified Mathlib/Data/Polynomial/Eval.lean

added theorem Polynomial.iterate_comp_eval