Compfiles/Imo2019P4.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2019, Problem 4

Determine all positive integers n,k that satisfy the equation

k! = (2ⁿ - 2⁰)(2ⁿ - 2¹) ... (2ⁿ - 2ⁿ⁻¹).

Imports (4)
Imported by 1 file
  1. theorem Imo2019P4.upper_bound line 46 source

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

    Statement uses: Nat, GT.gt, OfNat.ofNat, Eq, Int, Nat.factorial, Finset.prod, Finset.range, HSub.hSub, HPow.hPow, LT.lt

    Proof uses: Finset.sum, ENat, emultiplicity, Eq.mpr, id, congrArg, Finset.emultiplicity_prod, Int.prime_two, Nat.cast_sum, Finset.sum_congr, rfl, Finset, Membership.mem, emultiplicity_sub_of_gt, emultiplicity_pow_self_of_prime, propext, Nat.cast_lt, Eq.symm, Finset.mem_range, Eq.refl and 108 more

    165 instances, coercions and auxiliary constants left out.

    Tactic trace: 46 steps

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

  2. determine Imo2019P4.solution_set line 90 source

    no axioms what this means

    Statement uses: Set, Prod, Nat

    Proof uses: Insert.insert, Prod.mk, OfNat.ofNat, Singleton.singleton

    3 instances, coercions and auxiliary constants left out.

  3. problem Imo2019P4.imo2019_p4 line 92 source

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

    Statement uses: Nat, Iff, Membership.mem, Prod, Set, Imo2019P4.solution_set, Prod.mk, And, LT.lt, OfNat.ofNat, Eq, Int, Nat.factorial, Finset.prod, Finset.range, HSub.hSub, HPow.hPow

    Proof uses: Iff.intro, Or, Eq.mp, Eq.trans, Insert.insert, Singleton.singleton, congr, congrArg, Prod.mk.injEq, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl, Eq.symm, Imo2019P4.upper_bound, dite, LE.le, False.elim and 54 more

    70 instances, coercions and auxiliary constants left out.

    Tactic trace: 34 steps

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