Zulip Chat Archive

Stream: Is there code for X?

Topic: Big op products with rearranged indices


view this post on Zulip Yakov Pechersky (Aug 02 2020 at 12:52):

Do we have a lemma stating

lemma equiv.prod_map {α : Type u} {β : Type v} [comm_monoid β] (σ : α  α) (f : α  β) (s : finset α) :
   x in s, f (σ x) =  x in s, f x := sorry

?

view this post on Zulip Yakov Pechersky (Aug 02 2020 at 13:01):

I guess this isn't totally correct as stated. Really, it is

lemma equiv.map_prod {α : Type u} {β : Type v} [fintype α] [comm_monoid β] (σ : α  α) (f : α  β) :
   x, f (σ x) =  x, f x := sorry

view this post on Zulip Yakov Pechersky (Aug 02 2020 at 13:07):

Aha, finset.prod_equiv in fintype.card


Last updated: May 17 2021 at 15:13 UTC