finprod of constant func

Stream: Is there code for X?

[Ella Yu]

Hi, I wonder is there code to prove that, the big product of a constant function over a finite set can be written as that constant^(cardinality of the finite set)? My goal is like this, which looks obvious but I'm not sure how to prove
↑a ^ fintype.card ↥set_of_coprime = ∏ᶠ (j : ↥set_of_coprime), ↑a

Thanks in advance!

[Yakov Pechersky]

Is your set_of_coprime a set or a finset?

[Ella Yu]

it's a finset.

[Eric Rodriguez]

btw Ella, if you put your code in `s it gets code formatting, for example:

↑a ^ fintype.card ↥set_of_coprime = ∏ᶠ (j : ↥set_of_coprime), ↑a

(this is done with `↑a ^ fintype.card ↥set_of_coprime = ∏ᶠ (j : ↥set_of_coprime), ↑a` )

[Ella Yu]

thanks for your reminder! I'm new to zulip:D

[Yakov Pechersky]

Then this is a lemma about finset.card. I'd go through traditional products. There's docs#finprod_eq_prod_of_fintype

[Yakov Pechersky]

And docs#finset.prod_const

[Yakov Pechersky]

And docs#finset.prod_finset_coe

[Ella Yu]

Thanks a lot! It helps!