Compfiles/Imo1998P4.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1998, Problem 4

Determine all pairs (a, b) of positive integers such that ab^2 + b + 7 divides a^2b + a + b.

Imports (2)
Imported by 1 file
  1. determine Imo1998P4.solution_set line 25 source

    standard axioms: propext what this means

    Statement uses: Set, Prod, Int

    Proof uses: Union.union, Insert.insert, Prod.mk, OfNat.ofNat, Singleton.singleton, Set.ofPred, Imo1998P4.solution_set.match_1, Exists, And, LT.lt, Eq, HMul.hMul, HPow.hPow, Nat

    12 instances, coercions and auxiliary constants left out.

  2. problem Imo1998P4.imo1998_p4 line 28 source

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

    Statement uses: Int, Iff, And, LT.lt, OfNat.ofNat, Dvd.dvd, HAdd.hAdd, HMul.hMul, HPow.hPow, Nat, Membership.mem, Prod, Set, Imo1998P4.solution_set, Prod.mk

    Proof uses: Iff.intro, Eq.mpr, Or, Eq, Exists, id, Eq.trans, Union.union, Insert.insert, Singleton.singleton, Set.ofPred, Imo1998P4.solution_set.match_1, congrFun', congrArg, congr, Prod.mk.injEq, dvd_mul_of_dvd_left, dite, Neg.neg, Or.inr and 134 more

    163 instances, coercions and auxiliary constants left out.

    Tactic trace: 98 steps

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