Compfiles/Usa1974P1.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 1974, Problem 1

Let a, b, c be three distinct integers, and let P be a polynomial with integer coefficients. Show that in this case the conditions P (a) = b, P (b) = c, P (c) = a cannot be satisfied simultaneously.

Imports (3)
Imported by 1 file
  1. problem Usa1974P1.usa1974_p1 line 32 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Polynomial, Int, And, Ne, Not, Eq, Polynomial.eval

    Proof uses: False, Dvd.dvd, HSub.hSub, Eq.mpr, id, congrArg, Eq.symm, Polynomial.sub_dvd_eval_sub, dvd_trans, Nat, Int.natAbs, Int.natAbs_eq_of_dvd_dvd, Neg.neg, Or, Eq.mp, propext, Int.natAbs_eq_natAbs_iff, False.elim, Eq.trans, neg_sub and 1 more

    20 instances, coercions and auxiliary constants left out.

    Tactic trace: 25 steps

    Open to load the checked before-and-after goal states.