Compfiles/Imo2009P1.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned compfiles documentation, Pinned compfiles corpus index

3 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2009, Problem 1

Let $n$ be a positive integer and let $a_1, a_2, \ldots, a_k$ ($k \ge 2$) be distinct integers in the set $\{1, 2, \ldots, n\}$ such that $n$ divides $a_i(a_{i+1} - 1)$ for $i = 1, 2, \ldots, k - 1$. Prove that $n$ does not divide $a_k(a_1 - 1)$.

Imports (2)
Imported by 1 file
  1. lemma Imo2009P1.telescope Telescoping: if c j * c (j+1) = c j for all j, then the product of any window c i, c (i+1), …, c (i+m) collapses to its first term c i line 32 source

    Source documentation

    Telescoping: if c j * c (j+1) = c j for all j, then the product of any window c i, c (i+1), …, c (i+m) collapses to its first term c i.

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

    Statement uses: CommMonoid, Nat, Eq, HMul.hMul, HAdd.hAdd, OfNat.ofNat, Finset.prod, Finset.range

    Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congrFun', congrArg, Singleton.singleton, Finset, zero_add, Finset.prod_singleton, add_zero, eq_self, Eq.mpr, id, Finset.prod_range_succ, mul_assoc, Eq.symm, add_assoc

    23 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

    lemma telescope {R : Type*} [CommMonoid R] (c : ℕ → R)
    (hc : ∀ j, c j * c (j + 1) = c j) :
    ∀ m i, ∏ x ∈ Finset.range (m + 1), c (i + x) = c i := by
…
  2. lemma Imo2009P1.const_of_cyclic If the relation c j * c (j+1) = c j holds and c is periodic with period k ≥ 1, then c is constant: c i = c (i+1) for all i line 44 source

    Source documentation

    If the relation c j * c (j+1) = c j holds and c is periodic with period k ≥ 1, then c is constant: c i = c (i+1) for all i.

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

    Statement uses: CommMonoid, Nat, LE.le, OfNat.ofNat, Eq, HMul.hMul, HAdd.hAdd

    Proof uses: Exists, Exists.intro, HSub.hSub, Finset.prod, Finset.range, Imo2009P1.telescope, Eq.mpr, id, congrArg, Eq.symm, Finset.prod_range_succ', Finset.prod_range_succ, HMul, Eq.rec, Eq.refl, Finset.prod_congr, rfl, Finset, Membership.mem, add_comm and 13 more

    46 instances, coercions and auxiliary constants left out.

    Tactic trace: 15 steps

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

    lemma const_of_cyclic {R : Type*} [CommMonoid R] (c : ℕ → R) (k : ℕ) (hk : 1 ≤ k)
    (hc : ∀ j, c j * c (j + 1) = c j) (hper : ∀ i, c i = c (i + k)) :
    ∀ i, c i = c (i + 1) := by
…
  3. problem Imo2009P1.imo2009_p1 line 62 source

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

    Statement uses: Nat, LT.lt, OfNat.ofNat, LE.le, Fin, Int, Membership.mem, Finset, Finset.Icc, Function.Injective, HAdd.hAdd, Dvd.dvd, HMul.hMul, HSub.hSub, Fin.mk, Not

    Proof uses: ZMod, HMod.hMod, Nat.mod_lt, Eq, rfl, Nat.mod_eq_of_lt, Nat.succ, Or, lt_or_eq_of_le, Nat.succ_le_of_lt, Eq.mpr, id, congrArg, Nat.add_mod, Eq.refl, Fin.ext, Nat.mod_self, Iff.mpr, ZMod.intCast_zmod_eq_zero_iff_dvd, congr and 73 more

    116 instances, coercions and auxiliary constants left out.

    Tactic trace: 65 steps

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