doc-next-gen

Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Module docstring

{"# Interaction of big operators with piecewise functions

This file proves lemmas on the sum and product of piecewise functions, including ite and dite. "}

Finset.prod_apply_dite theorem
{s : Finset α} {p : α → Prop} {hp : DecidablePred p} [DecidablePred fun x => ¬p x] (f : ∀ x : α, p x → γ) (g : ∀ x : α, ¬p x → γ) (h : γ → β) : (∏ x ∈ s, h (if hx : p x then f x hx else g x hx)) = (∏ x : {x ∈ s | p x}, h (f x.1 <| by simpa using (mem_filter.mp x.2).2)) * ∏ x : {x ∈ s | ¬p x}, h (g x.1 <| by simpa using (mem_filter.mp x.2).2)
Full source 
@[to_additive]
theorem prod_apply_dite {s : Finset α} {p : α → Prop} {hp : DecidablePred p}
    [DecidablePred fun x => ¬p x] (f : ∀ x : α, p x → γ) (g : ∀ x : α, ¬p x → γ) (h : γ → β) :
    (∏ x ∈ s, h (if hx : p x then f x hx else g x hx)) =
      (∏ x : {x ∈ s | p x}, h (f x.1 <| by simpa using (mem_filter.mp x.2).2)) *
        ∏ x : {x ∈ s | ¬p x}, h (g x.1 <| by simpa using (mem_filter.mp x.2).2) :=
  calc
    (∏ x ∈ s, h (if hx : p x then f x hx else g x hx)) =
        (∏ x ∈ s with p x, h (if hx : p x then f x hx else g x hx)) *
          ∏ x ∈ s with ¬p x, h (if hx : p x then f x hx else g x hx) :=
      (prod_filter_mul_prod_filter_not s p _).symm
    _ = (∏ x : {x ∈ s | p x}, h (if hx : p x.1 then f x.1 hx else g x.1 hx)) *
          ∏ x : {x ∈ s | ¬p x}, h (if hx : p x.1 then f x.1 hx else g x.1 hx) :=
      congr_arg₂ _ (prod_attach _ _).symm (prod_attach _ _).symm
    _ = (∏ x : {x ∈ s | p x}, h (f x.1 <| by simpa using (mem_filter.mp x.2).2)) *
          ∏ x : {x ∈ s | ¬p x}, h (g x.1 <| by simpa using (mem_filter.mp x.2).2) :=
      congr_arg₂ _ (prod_congr rfl fun x _hx ↦
        congr_arg h (dif_pos <| by simpa using (mem_filter.mp x.2).2))
        (prod_congr rfl fun x _hx => congr_arg h (dif_neg <| by simpa using (mem_filter.mp x.2).2))
Product of Piecewise Function via Dependent If-Then-Else Decomposition
Informal description
Let $s$ be a finite set of elements of type $\alpha$, $p$ a decidable predicate on $\alpha$ (with decidable negation), and $f$ and $g$ functions defined on the elements of $\alpha$ satisfying $p$ and $\neg p$ respectively, mapping to a type $\gamma$. Let $h : \gamma \to \beta$ be a function where $\beta$ is a commutative monoid. Then the product over $s$ of $h$ applied to the piecewise function (defined by $f$ on $p(x)$ and $g$ otherwise) is equal to the product of $h \circ f$ over the subset of $s$ satisfying $p$ multiplied by the product of $h \circ g$ over the subset of $s$ not satisfying $p$. That is, \[ \prod_{x \in s} h\left(\begin{cases} f(x) & \text{if } p(x) \\ g(x) & \text{otherwise} \end{cases}\right) = \left(\prod_{\substack{x \in s \\ p(x)}} h(f(x))\right) \cdot \left(\prod_{\substack{x \in s \\ \neg p(x)}} h(g(x))\right). \]
Finset.prod_apply_ite theorem
{s : Finset α} {p : α → Prop} {_hp : DecidablePred p} (f g : α → γ) (h : γ → β) : (∏ x ∈ s, h (if p x then f x else g x)) = (∏ x ∈ s with p x, h (f x)) * ∏ x ∈ s with ¬p x, h (g x)
Full source 
@[to_additive]
theorem prod_apply_ite {s : Finset α} {p : α → Prop} {_hp : DecidablePred p} (f g : α → γ)
    (h : γ → β) :
    (∏ x ∈ s, h (if p x then f x else g x)) =
      (∏ x ∈ s with p x, h (f x)) * ∏ x ∈ s with ¬p x, h (g x) :=
  (prod_apply_dite _ _ _).trans <| congr_arg₂ _ (prod_attach _ (h ∘ f)) (prod_attach _ (h ∘ g))
Product of Piecewise Function via If-Then-Else Decomposition
Informal description
Let $s$ be a finite set of elements of type $\alpha$, $p$ a decidable predicate on $\alpha$, and $f, g : \alpha \to \gamma$ functions. Given a function $h : \gamma \to \beta$ where $\beta$ is a commutative monoid, the product over $s$ of $h$ applied to the piecewise function (defined by $f$ on $p(x)$ and $g$ otherwise) equals the product of $h \circ f$ over the elements of $s$ satisfying $p$ multiplied by the product of $h \circ g$ over the elements of $s$ not satisfying $p$. That is, \[ \prod_{x \in s} h\left(\begin{cases} f(x) & \text{if } p(x) \\ g(x) & \text{otherwise} \end{cases}\right) = \left(\prod_{\substack{x \in s \\ p(x)}} h(f(x))\right) \cdot \left(\prod_{\substack{x \in s \\ \neg p(x)}} h(g(x))\right). \]
Finset.prod_dite theorem
{s : Finset α} {p : α → Prop} {hp : DecidablePred p} (f : ∀ x : α, p x → β) (g : ∀ x : α, ¬p x → β) : ∏ x ∈ s, (if hx : p x then f x hx else g x hx) = (∏ x : {x ∈ s | p x}, f x.1 (by simpa using (mem_filter.mp x.2).2)) * ∏ x : {x ∈ s | ¬p x}, g x.1 (by simpa using (mem_filter.mp x.2).2)
Full source 
@[to_additive]
theorem prod_dite {s : Finset α} {p : α → Prop} {hp : DecidablePred p} (f : ∀ x : α, p x → β)
    (g : ∀ x : α, ¬p x → β) :
    ∏ x ∈ s, (if hx : p x then f x hx else g x hx) =
      (∏ x : {x ∈ s | p x}, f x.1 (by simpa using (mem_filter.mp x.2).2)) *
        ∏ x : {x ∈ s | ¬p x}, g x.1 (by simpa using (mem_filter.mp x.2).2) := by
  simp [prod_apply_dite _ _ fun x => x]
Product of Piecewise Function via Dependent If-Then-Else Decomposition
Informal description
Let $s$ be a finite set of elements of type $\alpha$, and let $p : \alpha \to \mathrm{Prop}$ be a decidable predicate on $\alpha$. Given functions $f : \Pi (x : \alpha), p(x) \to \beta$ and $g : \Pi (x : \alpha), \neg p(x) \to \beta$ where $\beta$ is a commutative monoid, the product over $s$ of the piecewise function (which evaluates to $f(x)$ if $p(x)$ holds and $g(x)$ otherwise) is equal to the product of $f$ over the subset of $s$ satisfying $p$ multiplied by the product of $g$ over the subset of $s$ not satisfying $p$. That is, \[ \prod_{x \in s} \begin{cases} f(x) & \text{if } p(x) \\ g(x) & \text{otherwise} \end{cases} = \left(\prod_{\substack{x \in s \\ p(x)}} f(x)\right) \cdot \left(\prod_{\substack{x \in s \\ \neg p(x)}} g(x)\right). \]
Finset.prod_ite theorem
{s : Finset α} {p : α → Prop} {hp : DecidablePred p} (f g : α → β) : ∏ x ∈ s, (if p x then f x else g x) = (∏ x ∈ s with p x, f x) * ∏ x ∈ s with ¬p x, g x
Full source 
@[to_additive]
theorem prod_ite {s : Finset α} {p : α → Prop} {hp : DecidablePred p} (f g : α → β) :
    ∏ x ∈ s, (if p x then f x else g x) = (∏ x ∈ s with p x, f x) * ∏ x ∈ s with ¬p x, g x := by
  simp [prod_apply_ite _ _ fun x => x]
Product of Piecewise Function via If-Then-Else Decomposition
Informal description
Let $s$ be a finite set of elements of type $\alpha$, and let $p : \alpha \to \mathrm{Prop}$ be a decidable predicate on $\alpha$. Given functions $f, g : \alpha \to \beta$ where $\beta$ is a commutative monoid, the product over $s$ of the piecewise function (which evaluates to $f(x)$ if $p(x)$ holds and $g(x)$ otherwise) equals the product of $f$ over the subset of $s$ satisfying $p$ multiplied by the product of $g$ over the subset of $s$ not satisfying $p$. That is, \[ \prod_{x \in s} \begin{cases} f(x) & \text{if } p(x) \\ g(x) & \text{otherwise} \end{cases} = \left(\prod_{\substack{x \in s \\ p(x)}} f(x)\right) \cdot \left(\prod_{\substack{x \in s \\ \neg p(x)}} g(x)\right). \]
Finset.prod_dite_of_false theorem
{p : α → Prop} {_ : DecidablePred p} (h : ∀ i ∈ s, ¬p i) (f : ∀ i, p i → β) (g : ∀ i, ¬p i → β) : ∏ i ∈ s, (if hi : p i then f i hi else g i hi) = ∏ i : s, g i.1 (h _ i.2)
Full source 
@[to_additive]
lemma prod_dite_of_false {p : α → Prop} {_ : DecidablePred p} (h : ∀ i ∈ s, ¬ p i)
    (f : ∀ i, p i → β) (g : ∀ i, ¬ p i → β) :
    ∏ i ∈ s, (if hi : p i then f i hi else g i hi) = ∏ i : s, g i.1 (h _ i.2) := by
  refine prod_bij' (fun x hx => ⟨x, hx⟩) (fun x _ ↦ x) ?_ ?_ ?_ ?_ ?_ <;> aesop
Product of Piecewise Function over False Predicate Equals Product of Second Branch
Informal description
Let $s$ be a finite set of elements of type $\alpha$, and let $p : \alpha \to \mathrm{Prop}$ be a decidable predicate on $\alpha$. Suppose that for every $i \in s$, the predicate $p(i)$ is false. Given functions $f : \Pi (i : \alpha), p(i) \to \beta$ and $g : \Pi (i : \alpha), \neg p(i) \to \beta$ where $\beta$ is a commutative monoid, the product over $s$ of the piecewise function (which evaluates to $f(i)$ if $p(i)$ holds and $g(i)$ otherwise) is equal to the product over $s$ of $g(i)$ evaluated with the proof that $\neg p(i)$ holds for each $i \in s$.
Finset.prod_ite_of_false theorem
{p : α → Prop} {_ : DecidablePred p} (h : ∀ x ∈ s, ¬p x) (f g : α → β) : ∏ x ∈ s, (if p x then f x else g x) = ∏ x ∈ s, g x
Full source 
@[to_additive]
lemma prod_ite_of_false {p : α → Prop} {_ : DecidablePred p} (h : ∀ x ∈ s, ¬p x) (f g : α → β) :
    ∏ x ∈ s, (if p x then f x else g x) = ∏ x ∈ s, g x :=
  (prod_dite_of_false h _ _).trans (prod_attach _ _)
Product of Piecewise Function over False Predicate Equals Product of Second Branch
Informal description
Let $s$ be a finite set of elements of type $\alpha$, and let $p : \alpha \to \mathrm{Prop}$ be a decidable predicate on $\alpha$. Suppose that for every $x \in s$, the predicate $p(x)$ is false. Given functions $f, g : \alpha \to \beta$ where $\beta$ is a commutative monoid, the product over $s$ of the piecewise function (which evaluates to $f(x)$ if $p(x)$ holds and $g(x)$ otherwise) is equal to the product over $s$ of $g(x)$.
Finset.prod_dite_of_true theorem
{p : α → Prop} {_ : DecidablePred p} (h : ∀ i ∈ s, p i) (f : ∀ i, p i → β) (g : ∀ i, ¬p i → β) : ∏ i ∈ s, (if hi : p i then f i hi else g i hi) = ∏ i : s, f i.1 (h _ i.2)
Full source 
@[to_additive]
lemma prod_dite_of_true {p : α → Prop} {_ : DecidablePred p} (h : ∀ i ∈ s, p i) (f : ∀ i, p i → β)
    (g : ∀ i, ¬ p i → β) :
    ∏ i ∈ s, (if hi : p i then f i hi else g i hi) = ∏ i : s, f i.1 (h _ i.2) := by
  refine prod_bij' (fun x hx => ⟨x, hx⟩) (fun x _ ↦ x) ?_ ?_ ?_ ?_ ?_ <;> aesop
Product of Dependent If-Then-Else Over True Predicate
Informal description
Let $s$ be a finite set of elements of type $\alpha$, and let $p : \alpha \to \mathrm{Prop}$ be a decidable predicate on $\alpha$. Suppose that for every $i \in s$, the predicate $p(i)$ holds. Given functions $f : \forall i, p(i) \to \beta$ and $g : \forall i, \neg p(i) \to \beta$ where $\beta$ is a commutative monoid, the product $\prod_{i \in s} (\text{if } p(i) \text{ then } f(i) \text{ else } g(i))$ is equal to $\prod_{i \in s} f(i)$, where the latter product is taken over the subtype $\{i \mid i \in s\}$.
Finset.prod_ite_of_true theorem
{p : α → Prop} {_ : DecidablePred p} (h : ∀ x ∈ s, p x) (f g : α → β) : ∏ x ∈ s, (if p x then f x else g x) = ∏ x ∈ s, f x
Full source 
@[to_additive]
lemma prod_ite_of_true {p : α → Prop} {_ : DecidablePred p} (h : ∀ x ∈ s, p x) (f g : α → β) :
    ∏ x ∈ s, (if p x then f x else g x) = ∏ x ∈ s, f x :=
  (prod_dite_of_true h _ _).trans (prod_attach _ _)
Product of If-Then-Else Over True Predicate
Informal description
Let $s$ be a finite set of elements of type $\alpha$, and let $p : \alpha \to \mathrm{Prop}$ be a decidable predicate on $\alpha$. Suppose that for every $x \in s$, the predicate $p(x)$ holds. Given functions $f, g : \alpha \to \beta$ where $\beta$ is a commutative monoid, the product $\prod_{x \in s} (\text{if } p(x) \text{ then } f(x) \text{ else } g(x))$ is equal to $\prod_{x \in s} f(x)$.
Finset.prod_apply_ite_of_false theorem
{p : α → Prop} {hp : DecidablePred p} (f g : α → γ) (k : γ → β) (h : ∀ x ∈ s, ¬p x) : (∏ x ∈ s, k (if p x then f x else g x)) = ∏ x ∈ s, k (g x)
Full source 
@[to_additive]
theorem prod_apply_ite_of_false {p : α → Prop} {hp : DecidablePred p} (f g : α → γ) (k : γ → β)
    (h : ∀ x ∈ s, ¬p x) : (∏ x ∈ s, k (if p x then f x else g x)) = ∏ x ∈ s, k (g x) := by
  simp_rw [apply_ite k]
  exact prod_ite_of_false h _ _
Product of Composed Piecewise Function over False Predicate Equals Product of Composed Second Branch
Informal description
Let $s$ be a finite set of elements of type $\alpha$, and let $p : \alpha \to \mathrm{Prop}$ be a decidable predicate on $\alpha$. Suppose that for every $x \in s$, the predicate $p(x)$ is false. Given functions $f, g : \alpha \to \gamma$ and $k : \gamma \to \beta$ where $\beta$ is a commutative monoid, the product $\prod_{x \in s} k(\text{if } p(x) \text{ then } f(x) \text{ else } g(x))$ is equal to $\prod_{x \in s} k(g(x))$.
Finset.prod_apply_ite_of_true theorem
{p : α → Prop} {hp : DecidablePred p} (f g : α → γ) (k : γ → β) (h : ∀ x ∈ s, p x) : (∏ x ∈ s, k (if p x then f x else g x)) = ∏ x ∈ s, k (f x)
Full source 
@[to_additive]
theorem prod_apply_ite_of_true {p : α → Prop} {hp : DecidablePred p} (f g : α → γ) (k : γ → β)
    (h : ∀ x ∈ s, p x) : (∏ x ∈ s, k (if p x then f x else g x)) = ∏ x ∈ s, k (f x) := by
  simp_rw [apply_ite k]
  exact prod_ite_of_true h _ _
Product of Composed If-Then-Else Over True Predicate
Informal description
Let $s$ be a finite set of elements of type $\alpha$, and let $p : \alpha \to \mathrm{Prop}$ be a decidable predicate on $\alpha$. Suppose that for every $x \in s$, the predicate $p(x)$ holds. Given functions $f, g : \alpha \to \gamma$ and $k : \gamma \to \beta$ where $\beta$ is a commutative monoid, the product $\prod_{x \in s} k(\text{if } p(x) \text{ then } f(x) \text{ else } g(x))$ is equal to $\prod_{x \in s} k(f(x))$.
Finset.prod_ite_mem theorem
[DecidableEq α] (s t : Finset α) (f : α → β) : ∏ i ∈ s, (if i ∈ t then f i else 1) = ∏ i ∈ s ∩ t, f i
Full source 
@[to_additive (attr := simp)]
theorem prod_ite_mem [DecidableEq α] (s t : Finset α) (f : α → β) :
    ∏ i ∈ s, (if i ∈ t then f i else 1) = ∏ i ∈ s ∩ t, f i := by
  rw [← Finset.prod_filter, Finset.filter_mem_eq_inter]
Product of Piecewise Function over Finite Set Equals Product over Intersection
Informal description
Let $\alpha$ be a type with decidable equality, and let $s$ and $t$ be finite subsets of $\alpha$. For any function $f : \alpha \to \beta$ where $\beta$ is a commutative monoid, the product over $s$ of the piecewise function that evaluates to $f(i)$ if $i \in t$ and to $1$ otherwise is equal to the product of $f$ over the intersection $s \cap t$. That is, \[ \prod_{i \in s} \begin{cases} f(i) & \text{if } i \in t, \\ 1 & \text{otherwise} \end{cases} = \prod_{i \in s \cap t} f(i). \]
Finset.prod_attach_eq_prod_dite theorem
[Fintype α] (s : Finset α) (f : s → β) [DecidablePred (· ∈ s)] : ∏ i ∈ s.attach, f i = ∏ i, if h : i ∈ s then f ⟨i, h⟩ else 1
Full source 
@[to_additive]
lemma prod_attach_eq_prod_dite [Fintype α] (s : Finset α) (f : s → β) [DecidablePred (· ∈ s)] :
    ∏ i ∈ s.attach, f i = ∏ i, if h : i ∈ s then f ⟨i, h⟩ else 1 := by
  rw [Finset.prod_dite, Finset.univ_eq_attach, Finset.prod_const_one, mul_one]
  congr
  · ext; simp
  · ext; simp
  · apply Function.hfunext <;> simp +contextual [Subtype.heq_iff_coe_eq]
Product over Attached Finset Equals Piecewise Product over Entire Type
Informal description
Let $\alpha$ be a finite type and $s$ be a finite subset of $\alpha$. For any function $f : s \to \beta$ where $\beta$ is a commutative monoid, and any decidable membership predicate on $s$, the product of $f$ over the attached finset $s.\mathrm{attach}$ equals the product over all elements $i \in \alpha$ of the piecewise function that evaluates to $f(i)$ if $i \in s$ and to $1$ otherwise. That is, \[ \prod_{i \in s.\mathrm{attach}} f(i) = \prod_{i \in \alpha} \begin{cases} f(i) & \text{if } i \in s \\ 1 & \text{otherwise} \end{cases}. \]
Finset.prod_dite_eq theorem
[DecidableEq α] (s : Finset α) (a : α) (b : ∀ x : α, a = x → β) : ∏ x ∈ s, (if h : a = x then b x h else 1) = ite (a ∈ s) (b a rfl) 1
Full source 
@[to_additive (attr := simp)]
theorem prod_dite_eq [DecidableEq α] (s : Finset α) (a : α) (b : ∀ x : α, a = x → β) :
    ∏ x ∈ s, (if h : a = x then b x h else 1) = ite (a ∈ s) (b a rfl) 1 := by
  split_ifs with h
  · rw [Finset.prod_eq_single a, dif_pos rfl]
    · intros _ _ h
      rw [dif_neg]
      exact h.symm
    · simp [h]
  · rw [Finset.prod_eq_one]
    intros
    rw [dif_neg]
    rintro rfl
    contradiction
Product of Conditional Function Equals Conditional Evaluation
Informal description
Let $\alpha$ be a type with decidable equality, $s$ a finite subset of $\alpha$, and $a \in \alpha$. Given a function $b : \alpha \to \beta$ (where $\beta$ is a commutative monoid) defined conditionally on the equality $a = x$, the product over $s$ of the piecewise function that evaluates to $b(x)$ if $a = x$ and to $1$ otherwise is equal to $b(a)$ if $a \in s$ and to $1$ otherwise. That is, \[ \prod_{x \in s} \begin{cases} b(x) & \text{if } a = x, \\ 1 & \text{otherwise} \end{cases} = \begin{cases} b(a) & \text{if } a \in s, \\ 1 & \text{otherwise}. \end{cases} \]
Finset.prod_dite_eq' theorem
[DecidableEq α] (s : Finset α) (a : α) (b : ∀ x : α, x = a → β) : ∏ x ∈ s, (if h : x = a then b x h else 1) = ite (a ∈ s) (b a rfl) 1
Full source 
@[to_additive (attr := simp)]
theorem prod_dite_eq' [DecidableEq α] (s : Finset α) (a : α) (b : ∀ x : α, x = a → β) :
    ∏ x ∈ s, (if h : x = a then b x h else 1) = ite (a ∈ s) (b a rfl) 1 := by
  split_ifs with h
  · rw [Finset.prod_eq_single a, dif_pos rfl]
    · intros _ _ h
      rw [dif_neg]
      exact h
    · simp [h]
  · rw [Finset.prod_eq_one]
    intros
    rw [dif_neg]
    rintro rfl
    contradiction
Product of Piecewise Function Equals Value at Point or One
Informal description
Let $\alpha$ be a type with decidable equality, $s$ a finite subset of $\alpha$, $a \in \alpha$, and $b : \alpha \to \beta$ a function defined only when its argument equals $a$ (where $\beta$ is a commutative monoid). Then the product over $s$ of the piecewise function that evaluates to $b(x)$ when $x = a$ and to $1$ otherwise equals $b(a)$ if $a \in s$ and $1$ otherwise. That is, \[ \prod_{x \in s} \begin{cases} b(x) & \text{if } x = a \\ 1 & \text{otherwise} \end{cases} = \begin{cases} b(a) & \text{if } a \in s \\ 1 & \text{otherwise.} \end{cases} \]
Finset.prod_ite_eq theorem
[DecidableEq α] (s : Finset α) (a : α) (b : α → β) : (∏ x ∈ s, ite (a = x) (b x) 1) = ite (a ∈ s) (b a) 1
Full source 
@[to_additive (attr := simp)]
theorem prod_ite_eq [DecidableEq α] (s : Finset α) (a : α) (b : α → β) :
    (∏ x ∈ s, ite (a = x) (b x) 1) = ite (a ∈ s) (b a) 1 :=
  prod_dite_eq s a fun x _ => b x
Product of Piecewise Function Equals Value at Point or One
Informal description
Let $\alpha$ be a type with decidable equality, $s$ a finite subset of $\alpha$, $a \in \alpha$, and $b : \alpha \to \beta$ a function where $\beta$ is a commutative monoid. Then the product over $s$ of the piecewise function that evaluates to $b(x)$ when $a = x$ and to $1$ otherwise equals $b(a)$ if $a \in s$ and $1$ otherwise. That is, \[ \prod_{x \in s} \begin{cases} b(x) & \text{if } a = x, \\ 1 & \text{otherwise} \end{cases} = \begin{cases} b(a) & \text{if } a \in s, \\ 1 & \text{otherwise}. \end{cases} \]
Finset.prod_ite_eq' theorem
[DecidableEq α] (s : Finset α) (a : α) (b : α → β) : (∏ x ∈ s, ite (x = a) (b x) 1) = ite (a ∈ s) (b a) 1
Full source 
/-- A product taken over a conditional whose condition is an equality test on the index and whose
alternative is `1` has value either the term at that index or `1`.

The difference with `Finset.prod_ite_eq` is that the arguments to `Eq` are swapped. -/
@[to_additive (attr := simp) "A sum taken over a conditional whose condition is an equality
test on the index and whose alternative is `0` has value either the term at that index or `0`.

The difference with `Finset.sum_ite_eq` is that the arguments to `Eq` are swapped."]
theorem prod_ite_eq' [DecidableEq α] (s : Finset α) (a : α) (b : α → β) :
    (∏ x ∈ s, ite (x = a) (b x) 1) = ite (a ∈ s) (b a) 1 :=
  prod_dite_eq' s a fun x _ => b x
Product of Piecewise Function Equals Value at Point or One (Swapped Equality)
Informal description
Let $\alpha$ be a type with decidable equality, $s$ a finite subset of $\alpha$, $a \in \alpha$, and $b : \alpha \to \beta$ a function where $\beta$ is a commutative monoid. Then the product over $s$ of the piecewise function that evaluates to $b(x)$ when $x = a$ and to $1$ otherwise equals $b(a)$ if $a \in s$ and $1$ otherwise. That is, \[ \prod_{x \in s} \begin{cases} b(x) & \text{if } x = a, \\ 1 & \text{otherwise} \end{cases} = \begin{cases} b(a) & \text{if } a \in s, \\ 1 & \text{otherwise}. \end{cases} \]
Finset.prod_ite_eq_of_mem theorem
[DecidableEq α] (s : Finset α) (a : α) (b : α → β) (h : a ∈ s) : (∏ x ∈ s, if a = x then b x else 1) = b a
Full source 
@[to_additive]
theorem prod_ite_eq_of_mem [DecidableEq α] (s : Finset α) (a : α) (b : α → β) (h : a ∈ s) :
    (∏ x ∈ s, if a = x then b x else 1) = b a := by
  simp only [prod_ite_eq, if_pos h]
Product of Piecewise Function Equals Value at Point When Point is in Set
Informal description
Let $\alpha$ be a type with decidable equality, $s$ a finite subset of $\alpha$, $a \in \alpha$ an element of $s$, and $b : \alpha \to \beta$ a function where $\beta$ is a commutative monoid. Then the product over $s$ of the piecewise function that evaluates to $b(x)$ when $a = x$ and to $1$ otherwise equals $b(a)$. That is, \[ \prod_{x \in s} \begin{cases} b(x) & \text{if } a = x, \\ 1 & \text{otherwise} \end{cases} = b(a). \]
Finset.prod_ite_eq_of_mem' theorem
[DecidableEq α] (s : Finset α) (a : α) (b : α → β) (h : a ∈ s) : (∏ x ∈ s, if x = a then b x else 1) = b a
Full source 
/-- The difference with `Finset.prod_ite_eq_of_mem` is that the arguments to `Eq` are swapped. -/
@[to_additive]
theorem prod_ite_eq_of_mem' [DecidableEq α] (s : Finset α) (a : α) (b : α → β) (h : a ∈ s) :
    (∏ x ∈ s, if x = a then b x else 1) = b a := by
  simp only [prod_ite_eq', if_pos h]
Product of Piecewise Function Equals Value at Point (Membership Version)
Informal description
Let $\alpha$ be a type with decidable equality, $s$ a finite subset of $\alpha$, $a \in \alpha$ with $a \in s$, and $b : \alpha \to \beta$ a function where $\beta$ is a commutative monoid. Then the product over $s$ of the piecewise function that evaluates to $b(x)$ when $x = a$ and to $1$ otherwise equals $b(a)$. That is, \[ \prod_{x \in s} \begin{cases} b(x) & \text{if } x = a, \\ 1 & \text{otherwise} \end{cases} = b(a). \]
Finset.prod_pi_mulSingle' theorem
[DecidableEq α] (a : α) (x : β) (s : Finset α) : ∏ a' ∈ s, Pi.mulSingle a x a' = if a ∈ s then x else 1
Full source 
@[to_additive (attr := simp)]
theorem prod_pi_mulSingle' [DecidableEq α] (a : α) (x : β) (s : Finset α) :
    ∏ a' ∈ s, Pi.mulSingle a x a' = if a ∈ s then x else 1 :=
  prod_dite_eq' _ _ _
Product of Multiplicative Single Function over Finite Set: $\prod_{a' \in s} \text{mulSingle}\ a\ x\ a' = \text{ite}\ (a \in s)\ x\ 1$
Informal description
Let $\alpha$ be a type with decidable equality, $\beta$ a commutative monoid, $a \in \alpha$, $x \in \beta$, and $s$ a finite subset of $\alpha$. The product over $s$ of the multiplicative single function $\text{mulSingle}\ a\ x$ is equal to $x$ if $a \in s$ and $1$ otherwise. That is, \[ \prod_{a' \in s} \begin{cases} x & \text{if } a' = a \\ 1 & \text{otherwise} \end{cases} = \begin{cases} x & \text{if } a \in s \\ 1 & \text{otherwise.} \end{cases} \]
Finset.prod_pi_mulSingle theorem
{β : α → Type*} [DecidableEq α] [∀ a, CommMonoid (β a)] (a : α) (f : ∀ a, β a) (s : Finset α) : (∏ a' ∈ s, Pi.mulSingle a' (f a') a) = if a ∈ s then f a else 1
Full source 
@[to_additive (attr := simp)]
theorem prod_pi_mulSingle {β : α → Type*} [DecidableEq α] [∀ a, CommMonoid (β a)] (a : α)
    (f : ∀ a, β a) (s : Finset α) :
    (∏ a' ∈ s, Pi.mulSingle a' (f a') a) = if a ∈ s then f a else 1 :=
  prod_dite_eq _ _ _
Product of Multiplicative Single Functions: $\prod_{a' \in s} \text{mulSingle}_{a'}(f(a'))(a) = \text{ite}(a \in s, f(a), 1)$
Informal description
Let $\alpha$ be a type with decidable equality, $\beta : \alpha \to \text{Type}$ a family of commutative monoids, $s$ a finite subset of $\alpha$, and $f : \forall a, \beta(a)$ a dependent function. Then the product over $s$ of the multiplicative single functions $\text{mulSingle}_{a'}(f(a'))$ evaluated at $a$ equals $f(a)$ if $a \in s$ and $1$ otherwise. That is, \[ \prod_{a' \in s} \text{mulSingle}_{a'}(f(a'))(a) = \begin{cases} f(a) & \text{if } a \in s, \\ 1 & \text{otherwise.} \end{cases} \]
Finset.prod_piecewise theorem
[DecidableEq α] (s t : Finset α) (f g : α → β) : (∏ x ∈ s, (t.piecewise f g) x) = (∏ x ∈ s ∩ t, f x) * ∏ x ∈ s \ t, g x
Full source 
@[to_additive]
theorem prod_piecewise [DecidableEq α] (s t : Finset α) (f g : α → β) :
    (∏ x ∈ s, (t.piecewise f g) x) = (∏ x ∈ s ∩ t, f x) * ∏ x ∈ s \ t, g x := by
  simp only [piecewise]
  rw [prod_ite, filter_mem_eq_inter, ← sdiff_eq_filter]
Product of Piecewise Function over Finite Sets: $\prod_{x \in s} (t.\text{piecewise}\ f\ g)(x) = (\prod_{x \in s \cap t} f(x)) \cdot (\prod_{x \in s \setminus t} g(x))$
Informal description
Let $\alpha$ be a type with decidable equality, $s$ and $t$ be finite subsets of $\alpha$, and $f, g : \alpha \to \beta$ be functions where $\beta$ is a commutative monoid. The product over $s$ of the piecewise function (which equals $f(x)$ for $x \in t$ and $g(x)$ otherwise) is equal to the product of $f$ over the intersection $s \cap t$ multiplied by the product of $g$ over the set difference $s \setminus t$. That is, \[ \prod_{x \in s} \begin{cases} f(x) & \text{if } x \in t \\ g(x) & \text{otherwise} \end{cases} = \left(\prod_{x \in s \cap t} f(x)\right) \cdot \left(\prod_{x \in s \setminus t} g(x)\right). \]
Finset.prod_inter_mul_prod_diff theorem
[DecidableEq α] (s t : Finset α) (f : α → β) : (∏ x ∈ s ∩ t, f x) * ∏ x ∈ s \ t, f x = ∏ x ∈ s, f x
Full source 
@[to_additive]
theorem prod_inter_mul_prod_diff [DecidableEq α] (s t : Finset α) (f : α → β) :
    (∏ x ∈ s ∩ t, f x) * ∏ x ∈ s \ t, f x = ∏ x ∈ s, f x := by
  convert (s.prod_piecewise t f f).symm
  simp +unfoldPartialApp [Finset.piecewise]
Product Decomposition over Intersection and Set Difference: $\prod_{s \cap t} f \cdot \prod_{s \setminus t} f = \prod_s f$
Informal description
Let $\alpha$ be a type with decidable equality, $s$ and $t$ be finite subsets of $\alpha$, and $f : \alpha \to \beta$ be a function where $\beta$ is a commutative monoid. Then the product of $f$ over the intersection $s \cap t$ multiplied by the product of $f$ over the set difference $s \setminus t$ equals the product of $f$ over the entire set $s$. That is, \[ \left(\prod_{x \in s \cap t} f(x)\right) \cdot \left(\prod_{x \in s \setminus t} f(x)\right) = \prod_{x \in s} f(x). \]
Finset.prod_eq_mul_prod_diff_singleton theorem
[DecidableEq α] {s : Finset α} {i : α} (h : i ∈ s) (f : α → β) : ∏ x ∈ s, f x = f i * ∏ x ∈ s \ { i }, f x
Full source 
@[to_additive]
theorem prod_eq_mul_prod_diff_singleton [DecidableEq α] {s : Finset α} {i : α} (h : i ∈ s)
    (f : α → β) : ∏ x ∈ s, f x = f i * ∏ x ∈ s \ {i}, f x := by
  convert (s.prod_inter_mul_prod_diff {i} f).symm
  simp [h]
Product Decomposition over Singleton Difference: $\prod_s f = f(i) \cdot \prod_{s \setminus \{i\}} f$
Informal description
Let $\alpha$ be a type with decidable equality, $s$ be a finite subset of $\alpha$, and $i \in s$ an element. For any function $f : \alpha \to \beta$ where $\beta$ is a commutative monoid, the product of $f$ over $s$ is equal to $f(i)$ multiplied by the product of $f$ over the set difference $s \setminus \{i\}$. That is, \[ \prod_{x \in s} f(x) = f(i) \cdot \prod_{x \in s \setminus \{i\}} f(x). \]
Finset.prod_eq_prod_diff_singleton_mul theorem
[DecidableEq α] {s : Finset α} {i : α} (h : i ∈ s) (f : α → β) : ∏ x ∈ s, f x = (∏ x ∈ s \ { i }, f x) * f i
Full source 
@[to_additive]
theorem prod_eq_prod_diff_singleton_mul [DecidableEq α] {s : Finset α} {i : α} (h : i ∈ s)
    (f : α → β) : ∏ x ∈ s, f x = (∏ x ∈ s \ {i}, f x) * f i := by
  rw [prod_eq_mul_prod_diff_singleton h, mul_comm]
Product Decomposition over Singleton Difference (Multiplicative Order Variant)
Informal description
Let $\alpha$ be a type with decidable equality, $s$ be a finite subset of $\alpha$, and $i \in s$ an element. For any function $f : \alpha \to \beta$ where $\beta$ is a commutative monoid, the product of $f$ over $s$ is equal to the product of $f$ over the set difference $s \setminus \{i\}$ multiplied by $f(i)$. That is, \[ \prod_{x \in s} f(x) = \left(\prod_{x \in s \setminus \{i\}} f(x)\right) \cdot f(i). \]
Fintype.prod_eq_mul_prod_compl theorem
[DecidableEq α] [Fintype α] (a : α) (f : α → β) : ∏ i, f i = f a * ∏ i ∈ { a }ᶜ, f i
Full source 
@[to_additive]
theorem _root_.Fintype.prod_eq_mul_prod_compl [DecidableEq α] [Fintype α] (a : α) (f : α → β) :
    ∏ i, f i = f a * ∏ i ∈ {a}ᶜ, f i :=
  prod_eq_mul_prod_diff_singleton (mem_univ a) f
Product Decomposition over Complement of Singleton: $\prod_\alpha f = f(a) \cdot \prod_{\alpha \setminus \{a\}} f$
Informal description
Let $\alpha$ be a finite type with decidable equality, and let $\beta$ be a commutative monoid. For any element $a \in \alpha$ and any function $f : \alpha \to \beta$, the product of $f$ over all elements of $\alpha$ equals $f(a)$ multiplied by the product of $f$ over the complement of $\{a\}$ in $\alpha$. That is, \[ \prod_{i \in \alpha} f(i) = f(a) \cdot \prod_{i \in \alpha \setminus \{a\}} f(i). \]
Fintype.prod_eq_prod_compl_mul theorem
[DecidableEq α] [Fintype α] (a : α) (f : α → β) : ∏ i, f i = (∏ i ∈ { a }ᶜ, f i) * f a
Full source 
@[to_additive]
theorem _root_.Fintype.prod_eq_prod_compl_mul [DecidableEq α] [Fintype α] (a : α) (f : α → β) :
    ∏ i, f i = (∏ i ∈ {a}ᶜ, f i) * f a :=
  prod_eq_prod_diff_singleton_mul (mem_univ a) f
Product Decomposition over Complement of Singleton (Multiplicative Order Variant)
Informal description
Let $\alpha$ be a finite type with decidable equality and $\beta$ be a commutative monoid. For any element $a \in \alpha$ and any function $f \colon \alpha \to \beta$, the product of $f$ over all elements of $\alpha$ equals the product of $f$ over the complement of $\{a\}$ in $\alpha$ multiplied by $f(a)$. That is, \[ \prod_{i \in \alpha} f(i) = \left(\prod_{i \in \alpha \setminus \{a\}} f(i)\right) \cdot f(a). \]
Finset.dvd_prod_of_mem theorem
(f : α → β) {a : α} {s : Finset α} (ha : a ∈ s) : f a ∣ ∏ i ∈ s, f i
Full source 
theorem dvd_prod_of_mem (f : α → β) {a : α} {s : Finset α} (ha : a ∈ s) : f a ∣ ∏ i ∈ s, f i := by
  classical
    rw [Finset.prod_eq_mul_prod_diff_singleton ha]
    exact dvd_mul_right _ _
Element Divides Product over Finite Set: $f(a) \mid \prod_{s} f$
Informal description
For any function $f \colon \alpha \to \beta$ where $\beta$ is a commutative monoid, and for any element $a \in \alpha$ in a finite subset $s \subseteq \alpha$, the value $f(a)$ divides the product $\prod_{i \in s} f(i)$.
Finset.prod_update_of_not_mem theorem
[DecidableEq α] {s : Finset α} {i : α} (h : i ∉ s) (f : α → β) (b : β) : ∏ x ∈ s, Function.update f i b x = ∏ x ∈ s, f x
Full source 
@[to_additive]
theorem prod_update_of_not_mem [DecidableEq α] {s : Finset α} {i : α} (h : i ∉ s) (f : α → β)
    (b : β) : ∏ x ∈ s, Function.update f i b x = ∏ x ∈ s, f x := by
  apply prod_congr rfl
  intros j hj
  have : j ≠ i := by
    rintro rfl
    exact h hj
  simp [this]
Product of Updated Function over Finite Set Excluding Updated Point
Informal description
Let $\alpha$ be a type with decidable equality, $s$ be a finite subset of $\alpha$, and $i \in \alpha$ such that $i \notin s$. For any function $f : \alpha \to \beta$ (where $\beta$ is a commutative monoid) and any element $b \in \beta$, the product of the updated function $\text{update } f \, i \, b$ over $s$ is equal to the product of $f$ over $s$, i.e., \[ \prod_{x \in s} \text{update } f \, i \, b \, x = \prod_{x \in s} f x. \]
Finset.prod_update_of_mem theorem
[DecidableEq α] {s : Finset α} {i : α} (h : i ∈ s) (f : α → β) (b : β) : ∏ x ∈ s, Function.update f i b x = b * ∏ x ∈ s \ singleton i, f x
Full source 
@[to_additive]
theorem prod_update_of_mem [DecidableEq α] {s : Finset α} {i : α} (h : i ∈ s) (f : α → β) (b : β) :
    ∏ x ∈ s, Function.update f i b x = b * ∏ x ∈ s \ singleton i, f x := by
  rw [update_eq_piecewise, prod_piecewise]
  simp [h]
Product of Updated Function over Finite Set Including Updated Point: $\prod_{x \in s} f[i \mapsto b](x) = b \cdot \prod_{x \in s \setminus \{i\}} f(x)$
Informal description
Let $\alpha$ be a type with decidable equality, $s$ be a finite subset of $\alpha$, and $i \in s$ an element. For any function $f : \alpha \to \beta$ (where $\beta$ is a commutative monoid) and any element $b \in \beta$, the product of the updated function $\text{update } f \, i \, b$ over $s$ is equal to $b$ multiplied by the product of $f$ over $s \setminus \{i\}$. That is, \[ \prod_{x \in s} \text{update } f \, i \, b \, x = b \cdot \prod_{x \in s \setminus \{i\}} f(x). \]
Finset.prod_ite_one theorem
(s : Finset α) (p : α → Prop) [DecidablePred p] (h : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j) (a : β) : ∏ i ∈ s, ite (p i) a 1 = ite (∃ i ∈ s, p i) a 1
Full source 
/-- See also `Finset.prod_ite_zero`. -/
@[to_additive "See also `Finset.sum_boole`."]
theorem prod_ite_one (s : Finset α) (p : α → Prop) [DecidablePred p]
    (h : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j) (a : β) :
    ∏ i ∈ s, ite (p i) a 1 = ite (∃ i ∈ s, p i) a 1 := by
  split_ifs with h
  · obtain ⟨i, hi, hpi⟩ := h
    rw [prod_eq_single_of_mem _ hi, if_pos hpi]
    exact fun j hj hji ↦ if_neg fun hpj ↦ hji <| h _ hj _ hi hpj hpi
  · push_neg at h
    rw [prod_eq_one]
    exact fun i hi => if_neg (h i hi)
Product of Indicator Function over Finite Set with Unique Condition
Informal description
Let $s$ be a finite set of type $\alpha$, $p : \alpha \to \mathrm{Prop}$ a decidable predicate, and $a$ an element of a commutative monoid $\beta$. Suppose that for any two elements $i, j \in s$, if both $p(i)$ and $p(j)$ hold, then $i = j$. Then the product over $s$ of the function that maps $i$ to $a$ if $p(i)$ holds and to $1$ otherwise is equal to $a$ if there exists an element $i \in s$ such that $p(i)$ holds, and to $1$ otherwise. In other words, \[ \prod_{i \in s} \begin{cases} a & \text{if } p(i) \\ 1 & \text{otherwise} \end{cases} = \begin{cases} a & \text{if } \exists i \in s, p(i) \\ 1 & \text{otherwise.} \end{cases} \]
Finset.prod_pow_boole theorem
[DecidableEq α] (s : Finset α) (f : α → β) (a : α) : (∏ x ∈ s, f x ^ ite (a = x) 1 0) = ite (a ∈ s) (f a) 1
Full source 
@[to_additive sum_boole_nsmul]
theorem prod_pow_boole [DecidableEq α] (s : Finset α) (f : α → β) (a : α) :
    (∏ x ∈ s, f x ^ ite (a = x) 1 0) = ite (a ∈ s) (f a) 1 := by simp
Product of Powers of Indicator Function over Finite Set: $\prod_{x \in s} f(x)^{\mathbb{1}_{a = x}} = f(a) \text{ if } a \in s \text{ else } 1$
Informal description
Let $\alpha$ be a type with decidable equality, $s$ a finite subset of $\alpha$, $f : \alpha \to \beta$ a function where $\beta$ is a commutative monoid, and $a \in \alpha$. Then the product over $s$ of $f(x)$ raised to the power of the indicator function $\mathbb{1}_{a = x}$ (which is $1$ if $a = x$ and $0$ otherwise) equals $f(a)$ if $a \in s$ and $1$ otherwise. That is, \[ \prod_{x \in s} f(x)^{\mathbb{1}_{a = x}} = \begin{cases} f(a) & \text{if } a \in s, \\ 1 & \text{otherwise}. \end{cases} \]
Finset.card_filter theorem
(p) [DecidablePred p] (s : Finset ι) : #({i ∈ s | p i}) = ∑ i ∈ s, ite (p i) 1 0
Full source 
lemma card_filter (p) [DecidablePred p] (s : Finset ι) :
    #{i ∈ s | p i} = ∑ i ∈ s, ite (p i) 1 0 := by simp [sum_ite]
Cardinality of Filtered Set as Sum of Indicators
Informal description
For any finite set $s$ of type $\iota$ and a decidable predicate $p$ on $\iota$, the cardinality of the subset $\{i \in s \mid p(i)\}$ is equal to the sum over $s$ of the indicator function $\mathbb{1}_p(i)$, where $\mathbb{1}_p(i) = 1$ if $p(i)$ holds and $0$ otherwise. In other words: $$ \#\{i \in s \mid p(i)\} = \sum_{i \in s} \begin{cases} 1 & \text{if } p(i) \\ 0 & \text{otherwise} \end{cases} $$
Fintype.prod_ite_eq_ite_exists theorem
(p : ι → Prop) [DecidablePred p] (h : ∀ i j, p i → p j → i = j) (a : α) : ∏ i, ite (p i) a 1 = ite (∃ i, p i) a 1
Full source 
@[to_additive]
lemma prod_ite_eq_ite_exists (p : ι → Prop) [DecidablePred p] (h : ∀ i j, p i → p j → i = j)
    (a : α) : ∏ i, ite (p i) a 1 = ite (∃ i, p i) a 1 := by
  simp [prod_ite_one univ p (by simpa using h)]
Product of Indicator Function over Finite Type with Unique Condition
Informal description
Let $\iota$ be a finite type, $p : \iota \to \mathrm{Prop}$ a decidable predicate, and $a$ an element of a commutative monoid $\alpha$. Suppose that for any two elements $i, j \in \iota$, if both $p(i)$ and $p(j)$ hold, then $i = j$. Then the product over $\iota$ of the function that maps $i$ to $a$ if $p(i)$ holds and to $1$ otherwise is equal to $a$ if there exists an element $i \in \iota$ such that $p(i)$ holds, and to $1$ otherwise. In other words, \[ \prod_{i \in \iota} \begin{cases} a & \text{if } p(i) \\ 1 & \text{otherwise} \end{cases} = \begin{cases} a & \text{if } \exists i \in \iota, p(i) \\ 1 & \text{otherwise.} \end{cases} \]
Fintype.prod_ite_mem theorem
(s : Finset ι) (f : ι → α) : ∏ i, (if i ∈ s then f i else 1) = ∏ i ∈ s, f i
Full source 
@[to_additive]
lemma prod_ite_mem (s : Finset ι) (f : ι → α) : ∏ i, (if i ∈ s then f i else 1) = ∏ i ∈ s, f i := by
  simp
Product of Piecewise Function over Finite Type Equals Product over Finite Subset
Informal description
Let $\alpha$ be a commutative monoid and $\iota$ a finite type. For any finite subset $s \subseteq \iota$ and any function $f : \iota \to \alpha$, the product over all elements of $\iota$ of the piecewise function that evaluates to $f(i)$ if $i \in s$ and to $1$ otherwise is equal to the product of $f$ over $s$. That is, \[ \prod_{i \in \iota} \begin{cases} f(i) & \text{if } i \in s, \\ 1 & \text{otherwise} \end{cases} = \prod_{i \in s} f(i). \]
Fintype.prod_dite_eq theorem
(i : ι) (f : ∀ j, i = j → α) : ∏ j, (if h : i = j then f j h else 1) = f i rfl
Full source 
/-- See also `Finset.prod_dite_eq`. -/
@[to_additive "See also `Finset.sum_dite_eq`."] lemma prod_dite_eq (i : ι) (f : ∀ j, i = j → α) :
    ∏ j, (if h : i = j then f j h else 1) = f i rfl := by
  rw [Finset.prod_dite_eq, if_pos (mem_univ _)]
Product of Conditional Function Equals Evaluation at Fixed Point
Informal description
Let $\iota$ be a finite type, $i \in \iota$, and $f : \forall j \in \iota, (i = j) \to \alpha$ a function where $\alpha$ is a commutative monoid. Then the product over all $j \in \iota$ of the piecewise function that evaluates to $f(j)$ if $i = j$ (with proof $h$) and to $1$ otherwise is equal to $f(i)$ (with the reflexivity proof $\text{rfl}$). That is, \[ \prod_{j \in \iota} \begin{cases} f(j) & \text{if } i = j, \\ 1 & \text{otherwise} \end{cases} = f(i). \]
Fintype.prod_dite_eq' theorem
(i : ι) (f : ∀ j, j = i → α) : ∏ j, (if h : j = i then f j h else 1) = f i rfl
Full source 
/-- See also `Finset.prod_dite_eq'`. -/
@[to_additive "See also `Finset.sum_dite_eq'`."] lemma prod_dite_eq' (i : ι) (f : ∀ j, j = i → α) :
    ∏ j, (if h : j = i then f j h else 1) = f i rfl := by
  rw [Finset.prod_dite_eq', if_pos (mem_univ _)]
Product of Piecewise Function over Finite Type Equals Value at Point
Informal description
Let $\alpha$ be a commutative monoid and $\iota$ a finite type. For any element $i \in \iota$ and any function $f : \iota \to \alpha$ defined only when its argument equals $i$, the product over all elements $j \in \iota$ of the piecewise function that evaluates to $f(j)$ when $j = i$ and to $1$ otherwise is equal to $f(i)$. That is, \[ \prod_{j \in \iota} \begin{cases} f(j) & \text{if } j = i, \\ 1 & \text{otherwise} \end{cases} = f(i). \]
Fintype.prod_ite_eq theorem
(i : ι) (f : ι → α) : ∏ j, (if i = j then f j else 1) = f i
Full source 
/-- See also `Finset.prod_ite_eq`. -/
@[to_additive "See also `Finset.sum_ite_eq`."]
lemma prod_ite_eq (i : ι) (f : ι → α) : ∏ j, (if i = j then f j else 1) = f i := by
  rw [Finset.prod_ite_eq, if_pos (mem_univ _)]
Product of Piecewise Function over Finite Type Equals Value at Point
Informal description
Let $\iota$ be a finite type, $i \in \iota$, and $f \colon \iota \to \alpha$ a function where $\alpha$ is a commutative monoid. Then the product over all $j \in \iota$ of the piecewise function that evaluates to $f(j)$ if $i = j$ and to $1$ otherwise is equal to $f(i)$. That is, \[ \prod_{j \in \iota} \begin{cases} f(j) & \text{if } i = j, \\ 1 & \text{otherwise} \end{cases} = f(i). \]
Fintype.prod_ite_eq' theorem
(i : ι) (f : ι → α) : ∏ j, (if j = i then f j else 1) = f i
Full source 
/-- See also `Finset.prod_ite_eq'`. -/
@[to_additive "See also `Finset.sum_ite_eq'`."]
lemma prod_ite_eq' (i : ι) (f : ι → α) : ∏ j, (if j = i then f j else 1) = f i := by
  rw [Finset.prod_ite_eq', if_pos (mem_univ _)]
Product of Piecewise Function over Finite Type Equals Value at Point (Swapped Equality)
Informal description
Let $\alpha$ be a commutative monoid and $\iota$ a finite type. For any element $i \in \iota$ and any function $f : \iota \to \alpha$, the product over all elements $j \in \iota$ of the piecewise function that evaluates to $f(j)$ when $j = i$ and to $1$ otherwise is equal to $f(i)$. That is, \[ \prod_{j \in \iota} \begin{cases} f(j) & \text{if } j = i, \\ 1 & \text{otherwise} \end{cases} = f(i). \]
Fintype.prod_pi_mulSingle theorem
{α : ι → Type*} [∀ i, CommMonoid (α i)] (i : ι) (f : ∀ i, α i) : ∏ j, Pi.mulSingle j (f j) i = f i
Full source 
/-- See also `Finset.prod_pi_mulSingle`. -/
@[to_additive "See also `Finset.sum_pi_single`."]
lemma prod_pi_mulSingle {α : ι → Type*} [∀ i, CommMonoid (α i)] (i : ι) (f : ∀ i, α i) :
    ∏ j, Pi.mulSingle j (f j) i = f i := prod_dite_eq _ _
Product of Multiplicative Single Functions Evaluates to Original Function
Informal description
Let $\iota$ be a finite type and $\alpha_i$ be a family of commutative monoids indexed by $\iota$. For any $i \in \iota$ and any function $f : \forall i, \alpha_i$, the product over all $j \in \iota$ of the multiplicative single function $\text{mulSingle}_j(f(j))$ evaluated at $i$ equals $f(i)$. That is, \[ \prod_{j \in \iota} \text{mulSingle}_j(f(j))(i) = f(i). \]
Fintype.prod_pi_mulSingle' theorem
(i : ι) (a : α) : ∏ j, Pi.mulSingle i a j = a
Full source 
/-- See also `Finset.prod_pi_mulSingle'`. -/
@[to_additive "See also `Finset.sum_pi_single'`."]
lemma prod_pi_mulSingle' (i : ι) (a : α) : ∏ j, Pi.mulSingle i a j = a := prod_dite_eq' _ _
Product of Multiplicative Single Function over Finite Type Equals Value at Point
Informal description
Let $\alpha$ be a commutative monoid and $\iota$ a finite type. For any element $i \in \iota$ and any element $a \in \alpha$, the product over all elements $j \in \iota$ of the multiplicative single function $\text{mulSingle}_i(a)$ evaluated at $j$ equals $a$. That is, \[ \prod_{j \in \iota} \text{mulSingle}_i(a)(j) = a, \] where $\text{mulSingle}_i(a)(j) = a$ if $j = i$ and $1$ otherwise.