Compfiles/Imo2020P5.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2020, Problem 5

A deck of n > 1 cards is given. A positive integer is written on each card. The deck has the property that the arithmetic mean of the numbers on each pair of cards is also the geometric mean of the numbers on some collection of one or more cards.

For which n does it follow that the numbers on the cards are all equal?

Imports (3)
Imported by 1 file
  1. determine Imo2020P5.SolutionSet line 30 source

    no axioms what this means

    Statement uses: Set, Nat

    Proof uses: Set.ofPred, LT.lt, OfNat.ofNat

    2 instances, coercions and auxiliary constants left out.

  2. def Imo2020P5.geometric_mean line 32 source

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

    Statement uses: Nat, Fin, PNat, Finset, Real

    Proof uses: HPow.hPow, Finset.prod, HDiv.hDiv, OfNat.ofNat, Finset.card

    11 instances, coercions and auxiliary constants left out.

  3. lemma Imo2020P5.rpow_inv_eq_iff line 48 source

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

    Statement uses: Real, LE.le, OfNat.ofNat, Nat, Ne, Iff, Eq, HPow.hPow, HDiv.hDiv

    Proof uses: Eq.mpr, Inv.inv, id, congrArg, one_div, Iff.intro, Eq.symm, Real.rpow_inv_natCast_pow, Eq.refl, Real.rpow_natCast, HMul.hMul, Real.rpow_mul, mul_inv_cancel₀, cast, Not, Eq.trans, Nat.cast_zero, Real.rpow_one

    66 instances, coercions and auxiliary constants left out.

    Tactic trace: 10 steps

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

  4. lemma Imo2020P5.all_equal line 59 source

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

    Statement uses: Nat, LT.lt, OfNat.ofNat, Fin, PNat, Pairwise, Exists, Finset, And, Finset.Nonempty, Eq, Real, Imo2020P5.geometric_mean, HDiv.hDiv, HAdd.hAdd

    Proof uses: Finset.gcd, Finset.univ, rfl, Dvd.dvd, Finset.gcd_dvd, Finset.mem_univ, Fin.mk, Nat.pos_of_dvd_of_pos, PNat.pos, Subtype.mk, Nat.div_pos, Nat.le_of_dvd, HMul.hMul, Eq.mpr, id, congrArg, Eq.symm, Nat.mul_div_cancel', Ne, Exists.intro and 152 more

    200 instances, coercions and auxiliary constants left out.

    Tactic trace: 128 steps

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

  5. problem Imo2020P5.imo2020_p5 line 206 source

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

    Statement uses: Nat, Iff, Membership.mem, Set, Imo2020P5.SolutionSet, And, LT.lt, OfNat.ofNat, Fin, PNat, Pairwise, Exists, Finset, Finset.Nonempty, Eq, Real, Imo2020P5.geometric_mean, HDiv.hDiv, HAdd.hAdd

    Proof uses: Iff.intro, And.intro, Imo2020P5.all_equal, And.left

    28 instances, coercions and auxiliary constants left out.