Compfiles/Imo1968P2.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1968, Problem 2

Determine the set of natural numbers x such that the product of the decimal digits of x is equal to x² - 10x - 22.

Imports (3)
Imported by 1 file
  1. lemma Imo1968P2.lemma0 line 29 source

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

    Statement uses: Nat, List, Ne, List.nil, Eq, List.getLast, List.mapIdx, Iff.mpr, List.mapIdx_ne_nil_iff, List.length, List.dropLast

    Proof uses: Eq.mpr, HSub.hSub, OfNat.ofNat, id, congrArg, List.getLast_mapIdx, List.length_dropLast, Eq.refl

    4 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  2. lemma Imo1968P2.prod_digits_le line 34 source

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

    Statement uses: Nat, LE.le, OfNat.ofNat, LT.lt, List.prod, Nat.digits

    Proof uses: Ne, List, List.nil, Iff.mpr, Nat.digits_ne_nil_iff_ne_zero, Iff.mp, Nat.pos_iff_ne_zero, Eq.mpr, HAppend.hAppend, List.dropLast, List.cons, List.getLast, id, Eq, congrArg, Eq.symm, List.dropLast_append_getLast, HMul.hMul, List.prod_append, List.prod_singleton and 22 more

    40 instances, coercions and auxiliary constants left out.

    Tactic trace: 17 steps

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

  3. determine Imo1968P2.solution_set line 64 source

    no axioms what this means

    Statement uses: Set, Nat

    Proof uses: Singleton.singleton, OfNat.ofNat

    2 instances, coercions and auxiliary constants left out.

  4. problem Imo1968P2.imo1968_p2 line 66 source

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

    Statement uses: Nat, Iff, Membership.mem, Set, Imo1968P2.solution_set, Eq, HPow.hPow, OfNat.ofNat, HAdd.hAdd, HMul.hMul, List.prod, Nat.digits

    Proof uses: Iff.intro, of_eq_true, Eq.trans, True, congr, congrArg, Mathlib.Meta.NormNum.IsNat.to_eq, Mathlib.Meta.NormNum.isNat_pow, Eq.refl, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Meta.NormNum.IsNatPowT.run, Mathlib.Meta.NormNum.IsNatPowT.bit0, Mathlib.Meta.NormNum.isNat_add, Mathlib.Meta.NormNum.isNat_mul, List.cons, List.nil, List, HMod.hMod, HDiv.hDiv, Nat.digits_of_two_le_of_pos and 119 more

    147 instances, coercions and auxiliary constants left out.

    Tactic trace: 15 steps

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