Compfiles/Imo1993P1.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1993, Problem 1

Let $f\left(x\right)=x^n+5x^{n-1}+3$, where $n>1$ is an integer. Prove that $f\left(x\right)$ cannot be expressed as the product of two non-constant polynomials with integer coefficients.

Imports (2)
Imported by 1 file
  1. def Imo1993P1.f line 28 source

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

    Statement uses: Nat, Polynomial, Int

    Proof uses: HAdd.hAdd, HPow.hPow, Polynomial.X, HMul.hMul, OfNat.ofNat, HSub.hSub

    18 instances, coercions and auxiliary constants left out.

  2. def Imo1993P1.isConstant line 30 source

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

    Statement uses: Semiring, Polynomial

    Proof uses: Nat, GT.gt, OfNat.ofNat, Eq, Finsupp, Polynomial.coeff

    7 instances, coercions and auxiliary constants left out.

  3. problem Imo1993P1.imo1993_p1 line 32 source

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

    Statement uses: Nat, GT.gt, OfNat.ofNat, Not, Exists, Polynomial, Int, And, Eq, Imo1993P1.f, HMul.hMul, Imo1993P1.isConstant

    Proof uses: id, False, Polynomial.eval, Eq.mpr, congrArg, Eq.symm, Polynomial.eval_mul, HAdd.hAdd, HPow.hPow, Polynomial.X, HSub.hSub, Eq.trans, congrFun', Polynomial.eval_add, congr, Polynomial.eval_pow, Polynomial.eval_X, Polynomial.eval_ofNat, zero_pow, Nat.ne_zero_of_lt and 194 more

    295 instances, coercions and auxiliary constants left out.

    Tactic trace: 277 steps (first 200 of 277)

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