Compfiles/Imo2004P2.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2004, Problem 2

Find all polynomials P with real coefficients such that for all reals a,b,c such that ab + bc + ca = 0 we have

P(a - b) + P(b - c) + P(c - a) = 2P(a + b + c).

Imports (2)
Imported by 1 file
  1. determine Imo2004P2.SolutionSet line 30 source

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

    Statement uses: Set, Polynomial, Real

    Proof uses: Set.ofPred, Exists, Eq, HAdd.hAdd, HSMul.hSMul, HPow.hPow, Nat, Polynomial.X, OfNat.ofNat

    15 instances, coercions and auxiliary constants left out.

  2. problem Imo2004P2.imo2004_p2 line 32 source

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

    Statement uses: Polynomial, Real, Iff, Membership.mem, Set, Imo2004P2.SolutionSet, Eq, HAdd.hAdd, HMul.hMul, OfNat.ofNat, Polynomial.eval, HSub.hSub, Nat

    Proof uses: Iff.intro, Exists, HSMul.hSMul, HPow.hPow, Polynomial.X, Eq.mpr, id, congr, congrArg, Eq.trans, Polynomial.eval_add, Polynomial.eval_smul, Polynomial.eval_pow, congrFun', Polynomial.eval_X, Eq.symm, propext, sub_eq_zero, Neg.neg, MulZeroClass.zero_mul and 192 more

    236 instances, coercions and auxiliary constants left out.

    Tactic trace: 91 steps

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