Zulip Chat Archive

Stream: new members

Topic: About my theorem

view this post on Zulip Adrian Chu (Jun 28 2019 at 14:35):

I am getting close to finishing proving my theorem

theorem mythm (n : ) (r : fin n  ) (s : )
    (hn : n  1) (hr :  i, r i  1) (hs : s  1)
    (coprime :  i : fin n, nat.gcd (r i) s = 1) :
     x : fin n  ,  y : ,
    ( i, x i  1)  (finset.univ.sum (λ i, (x i)^(r i)) = y^s) := sorry

Now I have some lemmas remains to be proven. They all involves the recursive function n_lcm, as defined below.

def fin_n_to_list {n : } (x: fin n  ) : list  :=
    (list.range n).map (λ i, if h : i < n then x i, h else 0)

def n_lcm {n : } (x : fin n  ) :  :=
    list.foldl nat.lcm 1 (fin_n_to_list x)

lemma n_lcm_geq_1 {n : } (x : fin n  ) (hx :  i, x i  1):
    n_lcm x  1 := sorry

I have read the chapter about induction TPIN a bit, but unfortunately have no idea on how to start proving the above lemma. Can anyone give some directions? Tganks

view this post on Zulip Kevin Buzzard (Jun 28 2019 at 14:37):

induction on n, and a proof for the n=2 case, will be the two ingredients that you need.

view this post on Zulip Adrian Chu (Jun 29 2019 at 08:45):

I start to see this is a big task. If we use induction, we at least need that lcm (a_1,...,a_n)=lcm(lcm(a_1,..a_(n-1)),a_n). and we dont yet have that either...

view this post on Zulip Mario Carneiro (Jun 29 2019 at 08:47):

You can use the multiset fold operation. It requires a proof that the operation is associative, but then you get that theorem for free

view this post on Zulip Kevin Buzzard (Jun 29 2019 at 18:48):

You should just need the base case and the n=2 case (for the inductive step). There will be some general theory in the library about how doing an operation to n things via folding is the same as doing it to n-1 things and then doing it once more. The proof will be short.

view this post on Zulip Kevin Buzzard (Jun 29 2019 at 18:50):

Well, the proof of the theorem for lists will be short. You'll then have to convert back to your fin n representation.

Last updated: May 13 2021 at 06:15 UTC