Compfiles/IntegersInACircle.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

There are 101 positive integers arranged in a circle. Suppose that the integers sum to 300. Prove that there exists a contiguous subarray that sums to 200.

https://mathstodon.xyz/@alexdbolton/110292738044661739https://math.stackexchange.com/questions/282589/101-positive-integers-placed-on-a-circle

Imports (5)
Imported by 1 file
  1. lemma IntegersInACircle.lemma1 line 33 source

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

    Statement uses: Int, Eq, HMod.hMod, OfNat.ofNat, LT.lt, Or

    9 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  2. lemma IntegersInACircle.lemma2 line 37 source

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

    Statement uses: ZMod, OfNat.ofNat, Nat, Int, Eq, Finset.sum, Finset.univ, Finset.range, HAdd.hAdd

    Proof uses: Membership.mem, Finset, Mathlib.Tactic.LinearCombination.eq_of_eq, Mathlib.Tactic.LinearCombination.eq_rearrange, Mathlib.Tactic.Ring.of_eq, HSub.hSub, Mathlib.Tactic.Ring.Common.sub_congr, HMul.hMul, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr, id, congrArg, Eq.symm, Eq.refl, Mathlib.Tactic.Ring.Common.add_pf_add_lt, Mathlib.Tactic.Ring.Common.add_pf_zero_add and 57 more

    71 instances, coercions and auxiliary constants left out.

    Tactic trace: 22 steps

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

  3. problem IntegersInACircle.integers_in_a_circle line 62 source

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

    Statement uses: ZMod, OfNat.ofNat, Nat, Int, LE.le, Eq, Finset.sum, Finset.univ, Exists, Finset.range, HAdd.hAdd

    Proof uses: ZMod.val, And, Ne, Function.comp, Fintype.exists_ne_map_eq_of_card_lt, Nat.lt_add_one, Fintype.card, LT.lt, Not, Or, Classical.em, Int.ModEq, Finset.Ico, Finset.sum_pos, Membership.mem, Finset, Eq.mp, Iff.mpr, Finset.Nonempty, Finset.nonempty_Ico and 63 more

    94 instances, coercions and auxiliary constants left out.

    Tactic trace: 76 steps

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