Big op products with rearranged indices

Stream: Is there code for X?

[Yakov Pechersky]

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

?

[Yakov Pechersky]

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

[Yakov Pechersky]

Aha, finset.prod_equiv in fintype.card