Mathlib.Data.Fintype.BigOperators

Fintype.prod_bool theorem

[CommMonoid α] (f : Bool → α) : ∏ b, f b = f true * f false

Full source

@[to_additive]
theorem prod_bool [CommMonoid α] (f : Bool → α) : ∏ b, f b = f true * f false := by simp

Product over Boolean Values in Commutative Monoid

Informal description

Let $\alpha$ be a commutative monoid and $f : \text{Bool} \to \alpha$ a function. The product of $f$ over all boolean values is equal to $f(\text{true})$ multiplied by $f(\text{false})$, i.e., \[ \prod_{b \in \text{Bool}} f(b) = f(\text{true}) \cdot f(\text{false}). \]

Fintype.card_eq_sum_ones theorem

{α} [Fintype α] : Fintype.card α = ∑ _a : α, 1

Full source

theorem card_eq_sum_ones {α} [Fintype α] : Fintype.card α = ∑ _a : α, 1 :=
  Finset.card_eq_sum_ones _

Cardinality as Sum of Ones over Finite Type

Informal description

For any finite type $\alpha$, the cardinality of $\alpha$ is equal to the sum of the constant function $1$ over all elements of $\alpha$, i.e., \[ |\alpha| = \sum_{a \in \alpha} 1. \]

Fintype.prod_extend_by_one theorem

[CommMonoid α] (s : Finset ι) (f : ι → α) : ∏ i, (if i ∈ s then f i else 1) = ∏ i ∈ s, f i

Full source

@[to_additive]
theorem prod_extend_by_one [CommMonoid α] (s : Finset ι) (f : ι → α) :
    ∏ i, (if i ∈ s then f i else 1) = ∏ i ∈ s, f i := by
  rw [← prod_filter, filter_mem_eq_inter, univ_inter]

Product of Extended Function Equals Product over Subset

Informal description

Let $\alpha$ be a commutative monoid and $s$ be a finite set of indices of type $\iota$. For any function $f \colon \iota \to \alpha$, the product over all indices $i \in \iota$ of the function that extends $f$ by setting it to $1$ outside $s$ is equal to the product of $f$ over the set $s$. In other words, \[ \prod_{i \in \iota} \left( \begin{cases} f(i) & \text{if } i \in s, \\ 1 & \text{otherwise} \end{cases} \right) = \prod_{i \in s} f(i). \]

Fintype.prod_eq_one theorem

(f : α → M) (h : ∀ a, f a = 1) : ∏ a, f a = 1

Full source

@[to_additive]
theorem prod_eq_one (f : α → M) (h : ∀ a, f a = 1) : ∏ a, f a = 1 :=
  Finset.prod_eq_one fun a _ha => h a

Product of Constant One Function Equals One

Informal description

For any function $f \colon \alpha \to M$ such that $f(a) = 1$ for all $a \in \alpha$, the product of $f$ over all elements of $\alpha$ is equal to $1$, i.e., $\prod_{a \in \alpha} f(a) = 1$.

Fintype.prod_congr theorem

(f g : α → M) (h : ∀ a, f a = g a) : ∏ a, f a = ∏ a, g a

Full source

@[to_additive]
theorem prod_congr (f g : α → M) (h : ∀ a, f a = g a) : ∏ a, f a = ∏ a, g a :=
  Finset.prod_congr rfl fun a _ha => h a

Product Equality for Pointwise Equal Functions on Finite Types

Informal description

Let $M$ be a commutative monoid and $\alpha$ a finite type. For any two functions $f, g : \alpha \to M$ such that $f(a) = g(a)$ for all $a \in \alpha$, the product of $f$ over $\alpha$ equals the product of $g$ over $\alpha$, i.e., \[ \prod_{a \in \alpha} f(a) = \prod_{a \in \alpha} g(a). \]

Fintype.prod_eq_single theorem

{f : α → M} (a : α) (h : ∀ x ≠ a, f x = 1) : ∏ x, f x = f a

Full source

@[to_additive]
theorem prod_eq_single {f : α → M} (a : α) (h : ∀ x ≠ a, f x = 1) : ∏ x, f x = f a :=
  Finset.prod_eq_single a (fun x _ hx => h x hx) fun ha => (ha (Finset.mem_univ a)).elim

Product over Finite Type Equals Single Non-Identity Term

Informal description

Let $\alpha$ be a finite type and $M$ a commutative monoid. For any function $f \colon \alpha \to M$ and element $a \in \alpha$, if $f(x) = 1$ for all $x \neq a$, then the product of $f$ over all elements of $\alpha$ equals $f(a)$, i.e., \[ \prod_{x \in \alpha} f(x) = f(a). \]

Fintype.prod_eq_mul theorem

{f : α → M} (a b : α) (h₁ : a ≠ b) (h₂ : ∀ x, x ≠ a ∧ x ≠ b → f x = 1) : ∏ x, f x = f a * f b

Full source

@[to_additive]
theorem prod_eq_mul {f : α → M} (a b : α) (h₁ : a ≠ b) (h₂ : ∀ x, x ≠ ax ≠ a ∧ x ≠ b → f x = 1) :
    ∏ x, f x = f a * f b := by
  apply Finset.prod_eq_mul a b h₁ fun x _ hx => h₂ x hx <;>
    exact fun hc => (hc (Finset.mem_univ _)).elim

Product over Finite Type with Two Non-Identity Elements

Informal description

Let $M$ be a commutative monoid and $\alpha$ a finite type. For any function $f : \alpha \to M$ and distinct elements $a, b \in \alpha$, if $f(x) = 1$ for all $x \neq a, b$, then the product of $f$ over $\alpha$ equals $f(a) \cdot f(b)$, i.e., \[ \prod_{x \in \alpha} f(x) = f(a) \cdot f(b). \]

Fintype.prod_option theorem

(f : Option α → M) : ∏ i, f i = f none * ∏ i, f (some i)

Full source

@[to_additive (attr := simp)]
theorem Fintype.prod_option (f : Option α → M) : ∏ i, f i = f none * ∏ i, f (some i) :=
  Finset.prod_insertNone f univ

Product over Option Type Decomposition

Informal description

For any function $f$ from the option type $\text{Option}\,\alpha$ to a multiplicative monoid $M$, the product of $f$ over all elements of $\text{Option}\,\alpha$ equals the product of $f(\text{none})$ and the product of $f$ over all elements of the form $\text{some}\,i$ where $i \in \alpha$. In symbols: \[ \prod_{i : \text{Option}\,\alpha} f(i) = f(\text{none}) \cdot \prod_{i : \alpha} f(\text{some}\,i) \]

Fintype.prod_eq_mul_prod_subtype_ne theorem

[DecidableEq α] (f : α → M) (a : α) : ∏ i, f i = f a * ∏ i : { i // i ≠ a }, f i.1

Full source

@[to_additive]
theorem Fintype.prod_eq_mul_prod_subtype_ne [DecidableEq α] (f : α → M) (a : α) :
    ∏ i, f i = f a * ∏ i : {i // i ≠ a}, f i.1 := by
  simp_rw [← (Equiv.optionSubtypeNe a).prod_comp, prod_option, Equiv.optionSubtypeNe_none,
    Equiv.optionSubtypeNe_some]

Product Decomposition over Finite Type with Decidable Equality

Informal description

For a function $f \colon \alpha \to M$ where $\alpha$ is a finite type with decidable equality and $M$ is a multiplicative monoid, and for any element $a \in \alpha$, the product of $f$ over all elements of $\alpha$ equals $f(a)$ multiplied by the product of $f$ over all elements of $\alpha$ not equal to $a$. In symbols: \[ \prod_{i \in \alpha} f(i) = f(a) \cdot \prod_{\substack{i \in \alpha \\ i \neq a}} f(i). \]

Finset.card_pi theorem

(s : Finset ι) (t : ∀ i, Finset (α i)) : #(s.pi t) = ∏ i ∈ s, #(t i)

Full source

@[simp] lemma Finset.card_pi (s : Finset ι) (t : ∀ i, Finset (α i)) :
    #(s.pi t) = ∏ i ∈ s, #(t i) := Multiset.card_pi _ _

Cardinality of Cartesian Product of Finite Sets: $\left|\prod_{i \in s} t(i)\right| = \prod_{i \in s} |t(i)|$

Informal description

For any finite set $s$ indexed by $\iota$ and any family of finite sets $t(i)$ indexed by $i \in \iota$, the cardinality of the cartesian product $\prod_{i \in s} t(i)$ is equal to the product of the cardinalities of the sets $t(i)$ for all $i \in s$. That is, $$ \left|\prod_{i \in s} t(i)\right| = \prod_{i \in s} |t(i)|. $$

Fintype.card_piFinset theorem

(s : ∀ i, Finset (α i)) : #(piFinset s) = ∏ i, #(s i)

Full source

@[simp] lemma card_piFinset (s : ∀ i, Finset (α i)) :
    #(piFinset s) = ∏ i, #(s i) := by simp [piFinset, card_map]

Cardinality of Product of Finite Sets: $\left|\prod_{i} s_i\right| = \prod_{i} |s_i|$

Informal description

For any family of finite sets $(s_i)_{i \in I}$, the cardinality of the product set $\prod_{i \in I} s_i$ is equal to the product of the cardinalities of the sets $s_i$ for all $i \in I$. That is, $$ \left|\prod_{i \in I} s_i\right| = \prod_{i \in I} |s_i|. $$

Fintype.card_piFinset_const theorem

{α : Type*} (s : Finset α) (n : ℕ) : #(piFinset fun _ : Fin n ↦ s) = #s ^ n

Full source

/-- This lemma is specifically designed to be used backwards, whence the specialisation to `Fin n`
as the indexing type doesn't matter in practice. The more general forward direction lemma here is
`Fintype.card_piFinset`. -/
lemma card_piFinset_const {α : Type*} (s : Finset α) (n : ℕ) :
    #(piFinset fun _ : Fin n ↦ s) = #s ^ n := by simp

Cardinality of Constant Product Set: $|\prod_{i \in \text{Fin } n} s| = |s|^n$

Informal description

For any finite set $s$ of type $\alpha$ and any natural number $n$, the cardinality of the product set $\prod_{i \in \text{Fin } n} s$ is equal to the cardinality of $s$ raised to the power of $n$, i.e., $$ \left|\prod_{i \in \text{Fin } n} s\right| = |s|^n. $$

Fintype.card_pi theorem

[∀ i, Fintype (α i)] : card (∀ i, α i) = ∏ i, card (α i)

Full source

@[simp] lemma card_pi [∀ i, Fintype (α i)] : card (∀ i, α i) = ∏ i, card (α i) :=
  card_piFinset _

Cardinality of Dependent Function Type: $\left|\prod_{i} \alpha_i\right| = \prod_{i} |\alpha_i|$

Informal description

For any family of finite types $(\alpha_i)_{i \in I}$, the cardinality of the dependent function type $\forall i, \alpha_i$ (the type of functions that assign to each $i$ an element of $\alpha_i$) is equal to the product of the cardinalities of the types $\alpha_i$ for all $i \in I$. That is, $$ \left|\prod_{i \in I} \alpha_i\right| = \prod_{i \in I} |\alpha_i|. $$

Fintype.card_pi_const theorem

(α : Type*) [Fintype α] (n : ℕ) : card (Fin n → α) = card α ^ n

Full source

/-- This lemma is specifically designed to be used backwards, whence the specialisation to `Fin n`
as the indexing type doesn't matter in practice. The more general forward direction lemma here is
`Fintype.card_pi`. -/
lemma card_pi_const (α : Type*) [Fintype α] (n : ℕ) : card (Fin n → α) = card α ^ n :=
  card_piFinset_const _ _

Cardinality of Function Space: $|\text{Fin } n \to \alpha| = |\alpha|^n$

Informal description

For any finite type $\alpha$ and natural number $n$, the cardinality of the function space $\text{Fin } n \to \alpha$ (the set of all functions from $\text{Fin } n$ to $\alpha$) is equal to the cardinality of $\alpha$ raised to the power of $n$, i.e., $$ |\text{Fin } n \to \alpha| = |\alpha|^n. $$

Fintype.prod_sigma theorem

 {ι} {α : ι → Type*} {M : Type*} [Fintype ι] [∀ i, Fintype (α i)] [CommMonoid M] (f : Sigma α → M) :
  ∏ x, f x = ∏ x, ∏ y, f ⟨x, y⟩

Full source

/-- Product over a sigma type equals the repeated product.

This is a version of `Finset.prod_sigma` specialized to the case
of multiplication over `Finset.univ`. -/
@[to_additive "Sum over a sigma type equals the repeated sum.

This is a version of `Finset.sum_sigma` specialized to the case of summation over `Finset.univ`."]
theorem prod_sigma {ι} {α : ι → Type*} {M : Type*} [Fintype ι] [∀ i, Fintype (α i)] [CommMonoid M]
    (f : Sigma α → M) : ∏ x, f x = ∏ x, ∏ y, f ⟨x, y⟩ :=
  Finset.prod_sigma ..

Product over a Sigma Type Equals Iterated Product

Informal description

Let $\iota$ be a finite type, and for each $i \in \iota$, let $\alpha_i$ be a finite type. Let $M$ be a commutative monoid, and let $f : \Sigma_{i \in \iota} \alpha_i \to M$ be a function. Then the product of $f$ over all elements of $\Sigma_{i \in \iota} \alpha_i$ equals the iterated product over $i \in \iota$ and $y \in \alpha_i$ of $f(i, y)$. In symbols: \[ \prod_{x \in \Sigma_{i \in \iota} \alpha_i} f(x) = \prod_{i \in \iota} \prod_{y \in \alpha_i} f(i, y). \]

Fintype.prod_sigma' theorem

 {ι} {α : ι → Type*} {M : Type*} [Fintype ι] [∀ i, Fintype (α i)] [CommMonoid M] (f : (i : ι) → α i → M) :
  ∏ x : Sigma α, f x.1 x.2 = ∏ x, ∏ y, f x y

Full source

/-- Product over a sigma type equals the repeated product, curried version.
This version is useful to rewrite from right to left. -/
@[to_additive "Sum over a sigma type equals the repeated sum, curried version.
This version is useful to rewrite from right to left."]
theorem prod_sigma' {ι} {α : ι → Type*} {M : Type*} [Fintype ι] [∀ i, Fintype (α i)] [CommMonoid M]
    (f : (i : ι) → α i → M) : ∏ x : Sigma α, f x.1 x.2 = ∏ x, ∏ y, f x y :=
  prod_sigma ..

Curried Sigma Product Equals Iterated Product

Informal description

Let $\iota$ be a finite type, and for each $i \in \iota$, let $\alpha_i$ be a finite type. Let $M$ be a commutative monoid, and let $f : \Pi_{i \in \iota} \alpha_i \to M$ be a function. Then the product of $f$ over all elements $(x,y)$ of the sigma type $\Sigma_{i \in \iota} \alpha_i$ equals the iterated product over $i \in \iota$ and $y \in \alpha_i$ of $f(i, y)$. In symbols: \[ \prod_{(x,y) \in \Sigma_{i \in \iota} \alpha_i} f(x,y) = \prod_{i \in \iota} \prod_{y \in \alpha_i} f(i, y). \]

Fintype.card_sigma theorem

{ι} {α : ι → Type*} [Fintype ι] [∀ i, Fintype (α i)] : card (Sigma α) = ∑ i, card (α i)

Full source

@[simp] nonrec lemma card_sigma {ι} {α : ι → Type*} [Fintype ι] [∀ i, Fintype (α i)] :
    card (Sigma α) = ∑ i, card (α i) := card_sigma _ _

Cardinality of Sigma Type Equals Sum of Component Cardinalities

Informal description

Let $\iota$ be a finite type, and for each $i \in \iota$, let $\alpha_i$ be a finite type. Then the cardinality of the sigma type $\Sigma_{i \in \iota} \alpha_i$ is equal to the sum over $i \in \iota$ of the cardinalities of $\alpha_i$. In symbols: \[ |\Sigma_{i \in \iota} \alpha_i| = \sum_{i \in \iota} |\alpha_i|. \]

Fintype.card_filter_piFinset_eq_of_mem theorem

 [∀ i, DecidableEq (α i)] (s : ∀ i, Finset (α i)) (i : ι) {a : α i} (ha : a ∈ s i) :
  #({f ∈ piFinset s | f i = a}) = ∏ j ∈ univ.erase i, #(s j)

Full source

/-- The number of dependent maps `f : Π j, s j` for which the `i` component is `a` is the product
over all `j ≠ i` of `#(s j)`.

Note that this is just a composition of easier lemmas, but there's some glue missing to make that
smooth enough not to need this lemma. -/
lemma card_filter_piFinset_eq_of_mem [∀ i, DecidableEq (α i)]
    (s : ∀ i, Finset (α i)) (i : ι) {a : α i} (ha : a ∈ s i) :
    #{f ∈ piFinset s | f i = a} = ∏ j ∈ univ.erase i, #(s j) := by
  calc
    _ = ∏ j, #(Function.update s i {a} j) := by
      rw [← piFinset_update_singleton_eq_filter_piFinset_eq _ _ ha, Fintype.card_piFinset]
    _ = ∏ j, Function.update (fun j ↦ #(s j)) i 1 j :=
      Fintype.prod_congr _ _ fun j ↦ by obtain rfl | hji := eq_or_ne j i <;> simp [*]
    _ = _ := by simp [prod_update_of_mem, erase_eq]

Cardinality of Dependent Functions with Fixed Component: $\left|\{f \in \prod_j s_j \mid f(i) = a\}\right| = \prod_{j \neq i} |s_j|$

Informal description

Let $I$ be a finite index set and for each $i \in I$, let $s_i$ be a finite set with decidable equality. For any fixed index $i \in I$ and element $a \in s_i$, the number of functions $f \in \prod_{j \in I} s_j$ such that $f(i) = a$ is equal to the product of the cardinalities of $s_j$ for all $j \neq i$. That is, $$ \left|\left\{f \in \prod_{j \in I} s_j \mid f(i) = a\right\}\right| = \prod_{j \in I \setminus \{i\}} |s_j|. $$

Fintype.card_filter_piFinset_const_eq_of_mem theorem

(s : Finset κ) (i : ι) {x : κ} (hx : x ∈ s) : #({f ∈ piFinset fun _ ↦ s | f i = x}) = #s ^ (card ι - 1)

Full source

lemma card_filter_piFinset_const_eq_of_mem (s : Finset κ) (i : ι) {x : κ} (hx : x ∈ s) :
    #{f ∈ piFinset fun _ ↦ s | f i = x} = #s ^ (card ι - 1) :=
  (card_filter_piFinset_eq_of_mem _ _ hx).trans <| by
    rw [prod_const #s, card_erase_of_mem (mem_univ _), card_univ]

Cardinality of Constant-Dependent Functions with Fixed Component: $\left|\{f \in \prod_j s \mid f(i) = x\}\right| = |s|^{|\iota| - 1}$

Informal description

Let $s$ be a finite set of elements of type $\kappa$, and let $\iota$ be a finite index set. For any fixed index $i \in \iota$ and element $x \in s$, the number of functions $f \in \prod_{j \in \iota} s$ such that $f(i) = x$ is equal to $|s|^{|\iota| - 1}$. That is, $$ \left|\left\{f \in \prod_{j \in \iota} s \mid f(i) = x\right\}\right| = |s|^{|\iota| - 1}. $$

Fintype.card_filter_piFinset_eq theorem

 [∀ i, DecidableEq (α i)] (s : ∀ i, Finset (α i)) (i : ι) (a : α i) :
  #({f ∈ piFinset s | f i = a}) = if a ∈ s i then ∏ b ∈ univ.erase i, #(s b) else 0

Full source

lemma card_filter_piFinset_eq [∀ i, DecidableEq (α i)] (s : ∀ i, Finset (α i)) (i : ι) (a : α i) :
    #{f ∈ piFinset s | f i = a} = if a ∈ s i then ∏ b ∈ univ.erase i, #(s b) else 0 := by
  split_ifs with h
  · rw [card_filter_piFinset_eq_of_mem _ _ h]
  · rw [filter_piFinset_of_not_mem _ _ _ h, Finset.card_empty]

Cardinality of Dependent Functions with Fixed Component (General Case)

Informal description

Let $I$ be a finite index set and for each $i \in I$, let $s_i$ be a finite set with decidable equality. For any fixed index $i \in I$ and element $a \in \alpha_i$, the number of functions $f \in \prod_{j \in I} s_j$ such that $f(i) = a$ is equal to $\prod_{j \in I \setminus \{i\}} |s_j|$ if $a \in s_i$, and $0$ otherwise. That is, $$ \left|\left\{f \in \prod_{j \in I} s_j \mid f(i) = a\right\}\right| = \begin{cases} \prod_{j \in I \setminus \{i\}} |s_j| & \text{if } a \in s_i, \\ 0 & \text{otherwise.} \end{cases} $$

Fintype.card_filter_piFinset_const theorem

 (s : Finset κ) (i : ι) (j : κ) : #({f ∈ piFinset fun _ ↦ s | f i = j}) = if j ∈ s then #s ^ (card ι - 1) else 0

Full source

lemma card_filter_piFinset_const (s : Finset κ) (i : ι) (j : κ) :
    #{f ∈ piFinset fun _ ↦ s | f i = j} = if j ∈ s then #s ^ (card ι - 1) else 0 :=
  (card_filter_piFinset_eq _ _ _).trans <| by
    rw [prod_const #s, card_erase_of_mem (mem_univ _), card_univ]

Cardinality of Constant-Dependent Functions with Fixed Component: $\left|\{f \in \prod_k s \mid f(i) = j\}\right| = |s|^{|\iota| - 1}$ if $j \in s$

Informal description

Let $s$ be a finite set of elements of type $\kappa$, and let $\iota$ be a finite index set. For any fixed index $i \in \iota$ and element $j \in \kappa$, the number of functions $f \in \prod_{k \in \iota} s$ such that $f(i) = j$ is equal to $|s|^{|\iota| - 1}$ if $j \in s$, and $0$ otherwise. That is, $$ \left|\left\{f \in \prod_{k \in \iota} s \mid f(i) = j\right\}\right| = \begin{cases} |s|^{|\iota| - 1} & \text{if } j \in s, \\ 0 & \text{otherwise.} \end{cases} $$

Fintype.card_fun theorem

[DecidableEq α] [Fintype α] [Fintype β] : Fintype.card (α → β) = Fintype.card β ^ Fintype.card α

Full source

theorem Fintype.card_fun [DecidableEq α] [Fintype α] [Fintype β] :
    Fintype.card (α → β) = Fintype.card β ^ Fintype.card α := by
  simp

Cardinality of Function Space: $|\alpha \to \beta| = |\beta|^{|\alpha|}$

Informal description

For any finite types $\alpha$ and $\beta$, the cardinality of the function type $\alpha \to \beta$ is equal to the cardinality of $\beta$ raised to the power of the cardinality of $\alpha$, i.e., \[ |\alpha \to \beta| = |\beta|^{|\alpha|}. \]

card_vector theorem

[Fintype α] (n : ℕ) : Fintype.card (List.Vector α n) = Fintype.card α ^ n

Full source

@[simp]
theorem card_vector [Fintype α] (n : ℕ) :
    Fintype.card (List.Vector α n) = Fintype.card α ^ n := by
  rw [Fintype.ofEquiv_card]; simp

Cardinality of Vectors: $|\text{Vector}\,\alpha\,n| = |\alpha|^n$

Informal description

For any finite type $\alpha$ and natural number $n$, the cardinality of the type of vectors of length $n$ over $\alpha$ is equal to the cardinality of $\alpha$ raised to the power of $n$. That is, $$ |\text{Vector}\,\alpha\,n| = |\alpha|^n. $$

Fin.prod_univ_eq_prod_range theorem

[CommMonoid α] (f : ℕ → α) (n : ℕ) : ∏ i : Fin n, f i = ∏ i ∈ range n, f i

Full source

/-- It is equivalent to compute the product of a function over `Fin n` or `Finset.range n`. -/
@[to_additive "It is equivalent to sum a function over `fin n` or `finset.range n`."]
theorem Fin.prod_univ_eq_prod_range [CommMonoid α] (f : ℕ → α) (n : ℕ) :
    ∏ i : Fin n, f i = ∏ i ∈ range n, f i :=
  calc
    ∏ i : Fin n, f i = ∏ i : { x // x ∈ range n }, f i :=
      Fintype.prod_equiv (Fin.equivSubtype.trans (Equiv.subtypeEquivRight (by simp))) _ _ (by simp)
    _ = ∏ i ∈ range n, f i := by rw [← attach_eq_univ, prod_attach]

Product over $\text{Fin } n$ Equals Product over $\{0, \dots, n-1\}$

Informal description

Let $\alpha$ be a commutative monoid and $f : \mathbb{N} \to \alpha$ a function. For any natural number $n$, the product of $f$ over the finite type $\text{Fin } n$ is equal to the product of $f$ over the finite set $\{0, \dots, n-1\}$. In symbols: \[ \prod_{i : \text{Fin } n} f(i) = \prod_{i \in \{0, \dots, n-1\}} f(i). \]

Finset.prod_fin_eq_prod_range theorem

 [CommMonoid β] {n : ℕ} (c : Fin n → β) : ∏ i, c i = ∏ i ∈ Finset.range n, if h : i < n then c ⟨i, h⟩ else 1

Full source

@[to_additive]
theorem Finset.prod_fin_eq_prod_range [CommMonoid β] {n : ℕ} (c : Fin n → β) :
    ∏ i, c i = ∏ i ∈ Finset.range n, if h : i < n then c ⟨i, h⟩ else 1 := by
  rw [← Fin.prod_univ_eq_prod_range, Finset.prod_congr rfl]
  rintro ⟨i, hi⟩ _
  simp only [hi, dif_pos]

Product over $\text{Fin } n$ Equals Conditional Product over $\{0, \dots, n-1\}$

Informal description

Let $\beta$ be a commutative monoid and $n$ a natural number. For any function $c : \text{Fin } n \to \beta$, the product of $c$ over all elements of $\text{Fin } n$ is equal to the product over the finite set $\{0, \dots, n-1\}$, where for each $i$ in this set, the term in the product is $c(i)$ if $i < n$ and $1$ otherwise. In symbols: \[ \prod_{i : \text{Fin } n} c(i) = \prod_{i \in \{0, \dots, n-1\}} \begin{cases} c(i) & \text{if } i < n, \\ 1 & \text{otherwise.} \end{cases} \]

Finset.prod_toFinset_eq_subtype theorem

 {M : Type*} [CommMonoid M] [Fintype α] (p : α → Prop) [DecidablePred p] (f : α → M) :
  ∏ a ∈ {x | p x}.toFinset, f a = ∏ a : Subtype p, f a

Full source

@[to_additive]
theorem Finset.prod_toFinset_eq_subtype {M : Type*} [CommMonoid M] [Fintype α] (p : α → Prop)
    [DecidablePred p] (f : α → M) : ∏ a ∈ { x | p x }.toFinset, f a = ∏ a : Subtype p, f a := by
  rw [← Finset.prod_subtype]
  simp_rw [Set.mem_toFinset]; intro; rfl

Product over Predicate-Defined Set Equals Product over Subtype

Informal description

Let $M$ be a commutative monoid and $\alpha$ a finite type. For any predicate $p : \alpha \to \text{Prop}$ with decidable membership and any function $f : \alpha \to M$, the product of $f$ over the finite set $\{x \mid p x\}$ is equal to the product of $f$ over the subtype $\{a : \alpha \mid p a\}$. In symbols: \[ \prod_{a \in \{x \mid p x\}} f(a) = \prod_{a : \{a \mid p a\}} f(a). \]

Fintype.prod_dite theorem

 [Fintype α] {p : α → Prop} [DecidablePred p] [CommMonoid β] (f : ∀ a, p a → β) (g : ∀ a, ¬p a → β) :
  (∏ a, dite (p a) (f a) (g a)) = (∏ a : { a // p a }, f a a.2) * ∏ a : { a // ¬p a }, g a a.2

Full source

nonrec theorem Fintype.prod_dite [Fintype α] {p : α → Prop} [DecidablePred p] [CommMonoid β]
    (f : ∀ a, p a → β) (g : ∀ a, ¬p a → β) :
    (∏ a, dite (p a) (f a) (g a)) =
    (∏ a : { a // p a }, f a a.2) * ∏ a : { a // ¬p a }, g a a.2 := by
  simp only [prod_dite, attach_eq_univ]
  congr 1
  · exact (Equiv.subtypeEquivRight <| by simp).prod_comp fun x : { x // p x } => f x x.2
  · exact (Equiv.subtypeEquivRight <| by simp).prod_comp fun x : { x // ¬p x } => g x x.2

Product of Dependent If-Then-Else over Finite Type Decomposes into Products over Subtypes

Informal description

Let $\alpha$ be a finite type and $p : \alpha \to \text{Prop}$ a decidable predicate on $\alpha$. Let $\beta$ be a commutative monoid, and let $f : \forall a \in \alpha, p(a) \to \beta$ and $g : \forall a \in \alpha, \neg p(a) \to \beta$ be functions. Then the product over $\alpha$ of the dependent if-then-else term $\mathrm{dite}(p(a), f(a), g(a))$ is equal to the product of $f$ over the subtype $\{a \in \alpha \mid p(a)\}$ multiplied by the product of $g$ over the subtype $\{a \in \alpha \mid \neg p(a)\}$. In symbols: \[ \prod_{a \in \alpha} \mathrm{dite}(p(a), f(a), g(a)) = \left(\prod_{a \in \{a \mid p(a)\}} f(a)\right) \cdot \left(\prod_{a \in \{a \mid \neg p(a)\}} g(a)\right). \]

Fintype.prod_sumElim theorem

(f : α₁ → M) (g : α₂ → M) : ∏ x, Sum.elim f g x = (∏ a₁, f a₁) * ∏ a₂, g a₂

Full source

@[to_additive]
theorem Fintype.prod_sumElim (f : α₁ → M) (g : α₂ → M) :
    ∏ x, Sum.elim f g x = (∏ a₁, f a₁) * ∏ a₂, g a₂ :=
  prod_disj_sum _ _ _

Product over Sum Type via Elimination

Informal description

Let $M$ be a commutative monoid and let $\alpha_1$ and $\alpha_2$ be finite types. For any functions $f : \alpha_1 \to M$ and $g : \alpha_2 \to M$, the product of the function $\mathrm{Sum.elim}\,f\,g$ over $\alpha_1 \oplus \alpha_2$ equals the product of $f$ over $\alpha_1$ multiplied by the product of $g$ over $\alpha_2$. In symbols: \[ \prod_{x \in \alpha_1 \oplus \alpha_2} \mathrm{Sum.elim}\,f\,g\,x = \left(\prod_{a_1 \in \alpha_1} f(a_1)\right) \cdot \left(\prod_{a_2 \in \alpha_2} g(a_2)\right). \]

Fintype.prod_sum_type theorem

(f : α₁ ⊕ α₂ → M) : ∏ x, f x = (∏ a₁, f (Sum.inl a₁)) * ∏ a₂, f (Sum.inr a₂)

Full source

@[to_additive (attr := simp)]
theorem Fintype.prod_sum_type (f : α₁ ⊕ α₂ → M) :
    ∏ x, f x = (∏ a₁, f (Sum.inl a₁)) * ∏ a₂, f (Sum.inr a₂) :=
  prod_disj_sum _ _ _

Product over Sum Type Decomposes into Products over Components

Informal description

Let $M$ be a commutative monoid and let $\alpha_1$ and $\alpha_2$ be finite types. For any function $f : \alpha_1 \oplus \alpha_2 \to M$, the product of $f$ over all elements of $\alpha_1 \oplus \alpha_2$ equals the product of $f$ over all left injections (elements of $\alpha_1$) multiplied by the product of $f$ over all right injections (elements of $\alpha_2$). In other words: \[ \prod_{x \in \alpha_1 \oplus \alpha_2} f(x) = \left(\prod_{a_1 \in \alpha_1} f(\text{inl}(a_1))\right) \times \left(\prod_{a_2 \in \alpha_2} f(\text{inr}(a_2))\right) \]

Fintype.prod_prod_type theorem

[CommMonoid γ] (f : α₁ × α₂ → γ) : ∏ x, f x = ∏ x, ∏ y, f (x, y)

Full source

/-- The product over a product type equals the product of the fiberwise products. For rewriting
in the reverse direction, use `Fintype.prod_prod_type'`. -/
@[to_additive Fintype.sum_prod_type "The sum over a product type equals the sum of fiberwise sums.
For rewriting in the reverse direction, use `Fintype.sum_prod_type'`."]
theorem Fintype.prod_prod_type [CommMonoid γ] (f : α₁ × α₂ → γ) :
    ∏ x, f x = ∏ x, ∏ y, f (x, y) :=
  Finset.prod_product ..

Product over a product type equals iterated product

Informal description

Let $γ$ be a commutative monoid and let $f : α₁ × α₂ → γ$ be a function. The product of $f$ over all pairs $(x, y) ∈ α₁ × α₂$ equals the product over $x ∈ α₁$ of the products over $y ∈ α₂$ of $f(x, y)$. In other words, \[ \prod_{(x,y) ∈ α₁ × α₂} f(x,y) = \prod_{x ∈ α₁} \prod_{y ∈ α₂} f(x,y). \]

Fintype.prod_prod_type' theorem

[CommMonoid γ] (f : α₁ → α₂ → γ) : ∏ x : α₁ × α₂, f x.1 x.2 = ∏ x, ∏ y, f x y

Full source

/-- The product over a product type equals the product of the fiberwise products. For rewriting
in the reverse direction, use `Fintype.prod_prod_type`. -/
@[to_additive Fintype.sum_prod_type' "The sum over a product type equals the sum of fiberwise sums.
For rewriting in the reverse direction, use `Fintype.sum_prod_type`."]
theorem Fintype.prod_prod_type' [CommMonoid γ] (f : α₁ → α₂ → γ) :
    ∏ x : α₁ × α₂, f x.1 x.2 = ∏ x, ∏ y, f x y :=
  Finset.prod_product' ..

Product over a product type equals iterated product

Informal description

Let $γ$ be a commutative monoid and $f : α₁ → α₂ → γ$ be a function. The product of $f$ over all pairs $(x, y) ∈ α₁ × α₂$ equals the product over $x ∈ α₁$ of the products over $y ∈ α₂$ of $f(x, y)$. In symbols: \[ \prod_{(x, y) ∈ α₁ × α₂} f(x, y) = \prod_{x ∈ α₁} \prod_{y ∈ α₂} f(x, y) \]

Fintype.prod_prod_type_right theorem

[CommMonoid γ] (f : α₁ × α₂ → γ) : ∏ x, f x = ∏ y, ∏ x, f (x, y)

Full source

@[to_additive Fintype.sum_prod_type_right]
theorem Fintype.prod_prod_type_right [CommMonoid γ] (f : α₁ × α₂ → γ) :
    ∏ x, f x = ∏ y, ∏ x, f (x, y) :=
  Finset.prod_product_right ..

Double Product Equality for Cartesian Product Types (Right Version)

Informal description

Let $γ$ be a commutative monoid and $f : α₁ × α₂ → γ$ be a function. The product of $f$ over all pairs $(x, y) ∈ α₁ × α₂$ equals the product over $y ∈ α₂$ of the products over $x ∈ α₁$ of $f(x, y)$. In symbols: \[ \prod_{(x,y) ∈ α₁ × α₂} f(x,y) = \prod_{y ∈ α₂} \prod_{x ∈ α₁} f(x,y) \]

Fintype.prod_prod_type_right' theorem

[CommMonoid γ] (f : α₁ → α₂ → γ) : ∏ x : α₁ × α₂, f x.1 x.2 = ∏ y, ∏ x, f x y

Full source

/-- An uncurried version of `Finset.prod_prod_type_right`. -/
@[to_additive Fintype.sum_prod_type_right' "An uncurried version of `Finset.sum_prod_type_right`"]
theorem Fintype.prod_prod_type_right' [CommMonoid γ] (f : α₁ → α₂ → γ) :
    ∏ x : α₁ × α₂, f x.1 x.2 = ∏ y, ∏ x, f x y :=
  Finset.prod_product_right' ..

Double Product Equality for Commutative Monoids

Informal description

Let $\gamma$ be a commutative monoid and $f : \alpha_1 \to \alpha_2 \to \gamma$ be a function. Then the product over all pairs $(x,y) \in \alpha_1 \times \alpha_2$ of $f(x)(y)$ is equal to the product over $y \in \alpha_2$ of the product over $x \in \alpha_1$ of $f(x)(y)$. In symbols: \[ \prod_{(x,y) \in \alpha_1 \times \alpha_2} f(x)(y) = \prod_{y \in \alpha_2} \prod_{x \in \alpha_1} f(x)(y) \]

Implementation note