Sums and products over preimages of finite sets. #
theorem
Finset.prod_preimage
{ι : Type u_1}
{κ : Type u_2}
{β : Type u_3}
[CommMonoid β]
(f : ι → κ)
(s : Finset κ)
(hf : Set.InjOn f (f ⁻¹' ↑s))
(g : κ → β)
(hg : ∀ x ∈ s, x ∉ Set.range f → g x = 1)
:
∏ x ∈ s.preimage f hf, g (f x) = ∏ x ∈ s, g x
theorem
Finset.sum_preimage
{ι : Type u_1}
{κ : Type u_2}
{β : Type u_3}
[AddCommMonoid β]
(f : ι → κ)
(s : Finset κ)
(hf : Set.InjOn f (f ⁻¹' ↑s))
(g : κ → β)
(hg : ∀ x ∈ s, x ∉ Set.range f → g x = 0)
:
∑ x ∈ s.preimage f hf, g (f x) = ∑ x ∈ s, g x
theorem
Finset.prod_preimage_of_bij
{ι : Type u_1}
{κ : Type u_2}
{β : Type u_3}
[CommMonoid β]
(f : ι → κ)
(s : Finset κ)
(hf : Set.BijOn f (f ⁻¹' ↑s) ↑s)
(g : κ → β)
:
∏ x ∈ s.preimage f ⋯, g (f x) = ∏ x ∈ s, g x
theorem
Finset.sum_preimage_of_bij
{ι : Type u_1}
{κ : Type u_2}
{β : Type u_3}
[AddCommMonoid β]
(f : ι → κ)
(s : Finset κ)
(hf : Set.BijOn f (f ⁻¹' ↑s) ↑s)
(g : κ → β)
:
∑ x ∈ s.preimage f ⋯, g (f x) = ∑ x ∈ s, g x