Compfiles/Poland2016S1P8.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Polish Mathematical Olympiad 2016, Stage 1, Problem 8 Author of the problem: Nguyen Hung Son Source of the problem: https://om.sem.edu.pl/static/app_main/problems/om68_1r.pdf

Let a, b, c be integers. Show that there exists a positive integer n, such that

n³ + an² + bn + c

is not a square of any integer.

Imports (3)
Imported by 1 file
  1. lemma Poland2016S1P8.even_of_add line 34 source

    standard axioms: Quot.sound, propext what this means

    Statement uses: Int, Even, HAdd.hAdd

    Proof uses: Eq.mpr, HSub.hSub, id, Eq, congrArg, Mathlib.Tactic.Ring.of_eq, HMul.hMul, HPow.hPow, Nat, Nat.rawCast, OfNat.ofNat, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.symm, Eq.refl, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.add_pf_add_gt, Mathlib.Tactic.Ring.Common.add_pf_add_zero, Mathlib.Tactic.Ring.Common.sub_pf and 21 more

    32 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  2. lemma Poland2016S1P8.div_4_mul_of_both_even line 38 source

    standard axioms: propext what this means

    Statement uses: Int, And, Even, Dvd.dvd, OfNat.ofNat, HMul.hMul

    Proof uses: Eq, HAdd.hAdd, Exists.intro, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr, id, congrArg, Eq.symm, Eq.refl, Mathlib.Tactic.Ring.Common.add_pf_add_overlap, Mathlib.Tactic.Ring.Common.add_overlap_pf, Mathlib.Meta.NormNum.IsNat.to_raw_eq, Mathlib.Meta.NormNum.isNat_add and 12 more

    33 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  3. problem Poland2016S1P8.poland2016_s1_p8 line 45 source

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

    Statement uses: Int, Exists, And, GT.gt, OfNat.ofNat, Not, IsSquare, HAdd.hAdd, HPow.hPow, Nat, HMul.hMul

    Proof uses: Iff.mp, not_forall_not, And.intro, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Nat.ble, Eq, False, HSub.hSub, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf and 46 more

    60 instances, coercions and auxiliary constants left out.

    Tactic trace: 69 steps

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