Zulip Chat Archive

Stream: new members

Topic: Reindexing sums


view this post on Zulip Julian Külshammer (Feb 06 2021 at 22:48):

I want to prove the following lemma:

import algebra.group_with_zero.power
import algebra.big_operators.intervals

variable {α : Type}

open finset

open_locale big_operators

lemma somelemma [ring α] (x y : α) (n : ):  i in range n, x^i*y^(n-1-i)=  j in range n, x^(n-1-j)*y^j :=
begin
  sorry
end

Using library_search I found rw ← sum_range_reflect as a possible first step. But then I wasn't able to convince lean that n-1-(n-1-j)=j because I wasn't able to apply nat.sub_sub_self since I didn't know how to extract the hypothesis that j\leq n-1 from the context. How can I do that or is there a better lemma to apply in mathlib?

view this post on Zulip Patrick Massot (Feb 06 2021 at 22:55):

Your second line should be refine sum_congr rfl (λ j j_in, _)

view this post on Zulip Patrick Massot (Feb 06 2021 at 22:55):

(after the rw you found)

view this post on Zulip Patrick Massot (Feb 06 2021 at 22:58):

view this post on Zulip Kevin Buzzard (Feb 06 2021 at 23:10):

This sum_congr rfl trick comes up again and again, it's well worth knowing!

view this post on Zulip Julian Külshammer (Feb 06 2021 at 23:10):

Thanks a lot.

view this post on Zulip Eric Wieser (Feb 07 2021 at 01:41):

For more complex reindexings by different argument types, you want docs#finset.sum_bij


Last updated: May 13 2021 at 18:26 UTC