Converting a finset to a list

Stream: Is there code for X?

[Eric Wieser]

I want to express the statement:

lemma sign.map_prod {α β : Sort*} [decidable_eq α] [fintype α] : ∀ (f : β → perm α) (s : finset β),
    sign (∏ x in s, f x) = ∏ x in s, sign (f x)

But I can't, because ∏ requires its argument to be commutative, and the one on the LHS is not.
How can I convert s into a list so that I can express the LHS using list.prod?

[Reid Barton]

How about starting with a list?

[Reid Barton]

Otherwise the product is not well-defined

[Eric Wieser]

Well, the lemma is true whichever of the non well-defined definitions you pick

[Reid Barton]

but... the lemma has to mean something...

[Eric Wieser]

To un-#xy my problem, I'm trying to show that (sigma_congr_right σ).sign = ∏ a, (σ a).sign, and I thought I'd do so by breaking down (sigma_congr_right σ) into a product of function.update 1 a (σ a)

[Eric Wieser]

Since the analogous approach worked for the simpler version expressed with sum

[Eric Wieser]

But I don't know how to express that product

[Reid Barton]

You lost me at function.update... but surely if you want to write a permutation as a product, it has to be a product of a list

[Eric Wieser]

The elements in the list all commute

[Eric Wieser]

But yes, I guess I could

[Eric Wieser]

But then I need to push finset.univ αinto that list

[Reid Barton]

docs#equiv.perm.sign_prod_congr_right looks similar except all the permutations are of the same set there

[Eric Wieser]

Far from a #mwe, but the sorry in question is here: https://github.com/leanprover-community/mathlib/compare/eric-wieser/sigma_congr_right_sign?expand=1#diff-126733ed2b8b67441355f6f20dbb566366f0dd0844a7d7b6ee5e7c6671c46e68R844

[Eric Wieser]

Oh sure enough, that contains the fintype.exists_univ_list α which I needed

[Eric Wieser]

Thanks for point me at that, that's enough to get me going.