sums: a1 + a2 + ... + an = b1 + b2 + .. bm

Stream: new members

[Thomas Strohmann]

I am working through some basic number theory proofs (e.g. c | a and c | b implies c | a + b). Now I am stuck on a theorem that involves some finite sums: Let a1 + a2 + ... + an = b1 + b2 + ... + bm where n > 1. Prove that if each of a1,a2,a{n-1},b1,b2,...,bm is divisible by b, then an is divisible by b. I looked a bit around in the docs/API for list, finset, range but have been struggling even to properly state the theorem in Lean. Any help would be appreciated. Thank you.

[Mario Carneiro]

There is already a theorem saying that if the bi are divisible by b then \sum i in s, bi is too

[Mario Carneiro]

for the other part I would use the theorem that if c | a then c | a + b <-> c | b, where c is b, a is \sum i in s.erase n, ai, and b is an

[Mario Carneiro]

Or something like that. The details depend to some extent on the context in which the theorem appears

[Kevin Buzzard]

import tactic

open_locale big_operators -- for sum notation

open finset -- so I can write `range` not `finset.range`

-- my m is your m-1 (because it's more idiomatic in Lean to
-- sum from 0) and my n is your n-2 (because it's much easier to have a natural
-- variable than a natural with a hypothesis). Finally my d is your b
-- (because you use b to mean two different things)
example (a b : ℕ → ℤ) (n m : ℕ) (d : ℤ)
  (hab : ∑ i in range (n+1), a i = ∑ j in range m, b j)
  (ha : ∀ i, i < n → d ∣ a i) (hb : ∀ j, j < m → d ∣ b j) : d ∣ a n := sorry

would be one way to do it (I've renormalised things to make it more idiomatic but mathematically this is an equivalent statement)

[Thomas Strohmann]

Thank you Kevin!