Mathlib.Algebra.BigOperators.Group.Finset.Preimage

Finset.prod_preimage' theorem

 (f : ι → κ) [DecidablePred (· ∈ Set.range f)] (s : Finset κ) (hf) (g : κ → β) :
  ∏ x ∈ s.preimage f hf, g (f x) = ∏ x ∈ s with x ∈ Set.range f, g x

Full source

@[to_additive]
lemma prod_preimage' (f : ι → κ) [DecidablePred (· ∈ Set.range f)] (s : Finset κ) (hf) (g : κ → β) :
    ∏ x ∈ s.preimage f hf, g (f x) = ∏ x ∈ s with x ∈ Set.range f, g x := by
  classical
  calc
    ∏ x ∈ preimage s f hf, g (f x) = ∏ x ∈ image f (preimage s f hf), g x :=
      Eq.symm <| prod_image <| by simpa only [mem_preimage, Set.InjOn] using hf
    _ = ∏ x ∈ s with x ∈ Set.range f, g x := by rw [image_preimage]

Product over Preimage Equals Product over Range Intersection for Finite Sets

Informal description

Let $f : \iota \to \kappa$ be a function, $s$ be a finite subset of $\kappa$, and $g : \kappa \to \beta$ be a function into a commutative monoid $\beta$. Suppose that $f$ is injective on the preimage $f^{-1}(s)$. Then the product of $g(f(x))$ over all $x$ in the preimage of $s$ under $f$ is equal to the product of $g(x)$ over all $x$ in $s$ that lie in the range of $f$. In symbols: $$ \prod_{x \in f^{-1}(s)} g(f(x)) = \prod_{\substack{x \in s \\ x \in \text{range}(f)}} g(x) $$

Finset.prod_preimage theorem

 (f : ι → κ) (s : Finset κ) (hf) (g : κ → β) (hg : ∀ x ∈ s, x ∉ Set.range f → g x = 1) :
  ∏ x ∈ s.preimage f hf, g (f x) = ∏ x ∈ s, g x

Full source

@[to_additive]
lemma prod_preimage (f : ι → κ) (s : Finset κ) (hf) (g : κ → β)
    (hg : ∀ x ∈ s, x ∉ Set.range f → g x = 1) :
    ∏ x ∈ s.preimage f hf, g (f x) = ∏ x ∈ s, g x := by
  classical rw [prod_preimage', prod_filter_of_ne]; exact fun x hx ↦ Not.imp_symm (hg x hx)

Product over Preimage Equals Product over Entire Finite Set under Range Condition

Informal description

Let $f : \iota \to \kappa$ be a function, $s$ be a finite subset of $\kappa$, and $g : \kappa \to \beta$ be a function into a commutative monoid $\beta$. Suppose that $f$ is injective on the preimage $f^{-1}(s)$, and for every $x \in s$ not in the range of $f$, $g(x) = 1$. Then the product of $g(f(x))$ over all $x$ in the preimage of $s$ under $f$ is equal to the product of $g(x)$ over all $x$ in $s$. In symbols: $$ \prod_{x \in f^{-1}(s)} g(f(x)) = \prod_{x \in s} g(x) $$

Finset.prod_preimage_of_bij theorem

 (f : ι → κ) (s : Finset κ) (hf : Set.BijOn f (f ⁻¹' ↑s) ↑s) (g : κ → β) :
  ∏ x ∈ s.preimage f hf.injOn, g (f x) = ∏ x ∈ s, g x

Full source

@[to_additive]
lemma prod_preimage_of_bij (f : ι → κ) (s : Finset κ) (hf : Set.BijOn f (f ⁻¹' ↑s) ↑s) (g : κ → β) :
    ∏ x ∈ s.preimage f hf.injOn, g (f x) = ∏ x ∈ s, g x :=
  prod_preimage _ _ hf.injOn g fun _ hs h_f ↦ (h_f <| hf.subset_range hs).elim

Product Equality under Bijective Preimage for Finite Sets

Informal description

Let $f : \iota \to \kappa$ be a function, $s$ be a finite subset of $\kappa$, and $g : \kappa \to \beta$ be a function into a commutative monoid $\beta$. Suppose that $f$ is bijective from the preimage $f^{-1}(s)$ to $s$. Then the product of $g(f(x))$ over all $x$ in the preimage of $s$ under $f$ is equal to the product of $g(x)$ over all $x$ in $s$. In symbols: $$ \prod_{x \in f^{-1}(s)} g(f(x)) = \prod_{x \in s} g(x) $$