Zulip Chat Archive

Stream: new members

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


Thomas Strohmann (Sep 06 2021 at 17:16):

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 (Sep 06 2021 at 17:22):

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

Mario Carneiro (Sep 06 2021 at 17:24):

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 (Sep 06 2021 at 17:25):

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

Kevin Buzzard (Sep 06 2021 at 17:48):

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 (Sep 06 2021 at 18:09):

Thank you Kevin!


Last updated: Dec 20 2023 at 11:08 UTC