Mathlib.Algebra.BigOperators.Fin

Finset.prod_range theorem

[CommMonoid M] {n : ℕ} (f : ℕ → M) : ∏ i ∈ Finset.range n, f i = ∏ i : Fin n, f i

Full source

@[to_additive]
theorem prod_range [CommMonoid M] {n : ℕ} (f : ℕ → M) :
    ∏ i ∈ Finset.range n, f i = ∏ i : Fin n, f i :=
  (Fin.prod_univ_eq_prod_range _ _).symm

Equality of Products over $\{0, \dots, n-1\}$ and $\mathrm{Fin}(n)$

Informal description

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

Fin.prod_ofFn theorem

(f : Fin n → M) : (List.ofFn f).prod = ∏ i, f i

Full source

@[to_additive]
theorem prod_ofFn (f : Fin n → M) : (List.ofFn f).prod = ∏ i, f i := by
  simp [prod_eq_multiset_prod]

Product over $\mathrm{Fin}(n)$ via List Construction

Informal description

For any commutative monoid $M$ and any function $f \colon \mathrm{Fin}(n) \to M$, the product of the elements in the list obtained by applying $f$ to all elements of $\mathrm{Fin}(n)$ is equal to the product of $f$ over all elements of $\mathrm{Fin}(n)$. In symbols: $\prod (a \in \mathrm{List.ofFn}\, f) \, a = \prod_{i \in \mathrm{Fin}(n)} f(i)$.

Fin.prod_univ_def theorem

(f : Fin n → M) : ∏ i, f i = ((List.finRange n).map f).prod

Full source

@[to_additive]
theorem prod_univ_def (f : Fin n → M) : ∏ i, f i = ((List.finRange n).map f).prod := by
  rw [← List.ofFn_eq_map, prod_ofFn]

Product over $\mathrm{Fin}(n)$ as Product of Mapped List

Informal description

For any commutative monoid $M$ and any function $f \colon \mathrm{Fin}(n) \to M$, the product of $f$ over all elements of $\mathrm{Fin}(n)$ is equal to the product of the list obtained by mapping $f$ over the list $\mathrm{finRange}(n)$. In symbols: \[ \prod_{i \in \mathrm{Fin}(n)} f(i) = \prod (a \in \mathrm{map}\, f\, (\mathrm{finRange}\, n)) \, a. \]

Fin.prod_univ_zero theorem

(f : Fin 0 → M) : ∏ i, f i = 1

Full source

/-- A product of a function `f : Fin 0 → M` is `1` because `Fin 0` is empty -/
@[to_additive "A sum of a function `f : Fin 0 → M` is `0` because `Fin 0` is empty"]
theorem prod_univ_zero (f : Fin 0 → M) : ∏ i, f i = 1 :=
  rfl

Empty Product over $\mathrm{Fin}(0)$ is One

Informal description

For any commutative monoid $M$ and any function $f \colon \mathrm{Fin}(0) \to M$, the product of $f$ over all elements of $\mathrm{Fin}(0)$ is equal to the multiplicative identity $1$ of $M$, i.e., \[ \prod_{i \in \mathrm{Fin}(0)} f(i) = 1. \]

Fin.prod_univ_succAbove theorem

(f : Fin (n + 1) → M) (x : Fin (n + 1)) : ∏ i, f i = f x * ∏ i : Fin n, f (x.succAbove i)

Full source

/-- A product of a function `f : Fin (n + 1) → M` over all `Fin (n + 1)`
is the product of `f x`, for some `x : Fin (n + 1)` times the remaining product -/
@[to_additive "A sum of a function `f : Fin (n + 1) → M` over all `Fin (n + 1)` is the sum of
`f x`, for some `x : Fin (n + 1)` plus the remaining sum"]
theorem prod_univ_succAbove (f : Fin (n + 1) → M) (x : Fin (n + 1)) :
    ∏ i, f i = f x * ∏ i : Fin n, f (x.succAbove i) := by
  rw [univ_succAbove n x, prod_cons, Finset.prod_map, coe_succAboveEmb]

Product Decomposition over $\mathrm{Fin}(n+1)$ via $\mathrm{succAbove}$ Embedding

Informal description

Let $M$ be a commutative monoid and $n$ a natural number. For any function $f \colon \mathrm{Fin}(n+1) \to M$ and any element $x \in \mathrm{Fin}(n+1)$, the product of $f$ over all elements of $\mathrm{Fin}(n+1)$ equals $f(x)$ multiplied by the product of $f$ over the image of $\mathrm{Fin}(n)$ under the embedding $\mathrm{succAbove}(x)$. In symbols: \[ \prod_{i \in \mathrm{Fin}(n+1)} f(i) = f(x) \cdot \prod_{i \in \mathrm{Fin}(n)} f(\mathrm{succAbove}(x, i)). \]

Fin.prod_univ_succ theorem

(f : Fin (n + 1) → M) : ∏ i, f i = f 0 * ∏ i : Fin n, f i.succ

Full source

/-- A product of a function `f : Fin (n + 1) → M` over all `Fin (n + 1)`
is the product of `f 0` plus the remaining product -/
@[to_additive "A sum of a function `f : Fin (n + 1) → M` over all `Fin (n + 1)` is the sum of
`f 0` plus the remaining sum"]
theorem prod_univ_succ (f : Fin (n + 1) → M) :
    ∏ i, f i = f 0 * ∏ i : Fin n, f i.succ :=
  prod_univ_succAbove f 0

Product Decomposition over $\mathrm{Fin}(n+1)$ via Successor Function

Informal description

Let $M$ be a commutative monoid and $n$ a natural number. For any function $f \colon \mathrm{Fin}(n+1) \to M$, the product of $f$ over all elements of $\mathrm{Fin}(n+1)$ equals $f(0)$ multiplied by the product of $f$ over the successors of all elements of $\mathrm{Fin}(n)$. In symbols: \[ \prod_{i \in \mathrm{Fin}(n+1)} f(i) = f(0) \cdot \prod_{i \in \mathrm{Fin}(n)} f(\mathrm{succ}(i)). \]

Fin.prod_univ_castSucc theorem

(f : Fin (n + 1) → M) : ∏ i, f i = (∏ i : Fin n, f (Fin.castSucc i)) * f (last n)

Full source

/-- A product of a function `f : Fin (n + 1) → M` over all `Fin (n + 1)`
is the product of `f (Fin.last n)` plus the remaining product -/
@[to_additive "A sum of a function `f : Fin (n + 1) → M` over all `Fin (n + 1)` is the sum of
`f (Fin.last n)` plus the remaining sum"]
theorem prod_univ_castSucc (f : Fin (n + 1) → M) :
    ∏ i, f i = (∏ i : Fin n, f (Fin.castSucc i)) * f (last n) := by
  simpa [mul_comm] using prod_univ_succAbove f (last n)

Product Decomposition over $\mathrm{Fin}(n+1)$ via $\mathrm{castSucc}$ Embedding

Informal description

Let $M$ be a commutative monoid and $n$ a natural number. For any function $f \colon \mathrm{Fin}(n+1) \to M$, the product of $f$ over all elements of $\mathrm{Fin}(n+1)$ equals the product of $f$ over the image of $\mathrm{Fin}(n)$ under the embedding $\mathrm{castSucc}$ multiplied by $f$ evaluated at the last element $\mathrm{last}\,n$. In symbols: \[ \prod_{i \in \mathrm{Fin}(n+1)} f(i) = \left(\prod_{i \in \mathrm{Fin}(n)} f(\mathrm{castSucc}\,i)\right) \cdot f(\mathrm{last}\,n). \]

Fin.prod_univ_getElem theorem

(l : List M) : ∏ i : Fin l.length, l[i.1] = l.prod

Full source

@[to_additive (attr := simp)]
theorem prod_univ_getElem (l : List M) : ∏ i : Fin l.length, l[i.1] = l.prod := by
  simp [Finset.prod_eq_multiset_prod]

Product over List Elements via Finite Ordinals Equals List Product

Informal description

For any list $l$ of elements in a commutative monoid $M$, the product of the elements of $l$ indexed by their positions in $\mathrm{Fin}(l.\mathrm{length})$ is equal to the product of the elements of $l$, i.e., \[ \prod_{i \in \mathrm{Fin}(l.\mathrm{length})} l[i] = \prod_{x \in l} x. \]

Fin.prod_univ_fun_getElem theorem

(l : List α) (f : α → M) : ∏ i : Fin l.length, f l[i.1] = (l.map f).prod

Full source

@[to_additive (attr := simp)]
theorem prod_univ_fun_getElem (l : List α) (f : α → M) :
    ∏ i : Fin l.length, f l[i.1] = (l.map f).prod := by
  simp [Finset.prod_eq_multiset_prod]

Product over List Elements via Finite Ordinals Equals Product of Mapped List

Informal description

For any list $l$ of elements of type $\alpha$ and any function $f \colon \alpha \to M$ where $M$ is a commutative monoid, the product of $f$ applied to each element of $l$ indexed by their positions in $\mathrm{Fin}(l.\mathrm{length})$ is equal to the product of the list obtained by mapping $f$ over $l$, i.e., \[ \prod_{i \in \mathrm{Fin}(l.\mathrm{length})} f(l[i]) = \prod_{x \in l.\mathrm{map}\, f} x. \]

Fin.prod_cons theorem

(x : M) (f : Fin n → M) : (∏ i : Fin n.succ, (cons x f : Fin n.succ → M) i) = x * ∏ i : Fin n, f i

Full source

@[to_additive (attr := simp)]
theorem prod_cons (x : M) (f : Fin n → M) :
    (∏ i : Fin n.succ, (cons x f : Fin n.succ → M) i) = x * ∏ i : Fin n, f i := by
  simp_rw [prod_univ_succ, cons_zero, cons_succ]

Product Decomposition via Prepended Function on $\mathrm{Fin}(n+1)$

Informal description

Let $M$ be a commutative monoid and $n$ a natural number. For any element $x \in M$ and any function $f \colon \mathrm{Fin}(n) \to M$, the product of the function $\mathrm{cons}(x, f) \colon \mathrm{Fin}(n+1) \to M$ over all elements of $\mathrm{Fin}(n+1)$ equals $x$ multiplied by the product of $f$ over all elements of $\mathrm{Fin}(n)$. In symbols: \[ \prod_{i \in \mathrm{Fin}(n+1)} \mathrm{cons}(x, f)(i) = x \cdot \prod_{i \in \mathrm{Fin}(n)} f(i). \]

Fin.prod_snoc theorem

(x : M) (f : Fin n → M) : (∏ i : Fin n.succ, (snoc f x : Fin n.succ → M) i) = (∏ i : Fin n, f i) * x

Full source

@[to_additive (attr := simp)]
theorem prod_snoc (x : M) (f : Fin n → M) :
    (∏ i : Fin n.succ, (snoc f x : Fin n.succ → M) i) = (∏ i : Fin n, f i) * x := by
  simp [prod_univ_castSucc]

Product Decomposition over $\mathrm{Fin}(n+1)$ via $\mathrm{snoc}$ Append

Informal description

Let $M$ be a commutative monoid and $n$ a natural number. For any function $f \colon \mathrm{Fin}(n) \to M$ and any element $x \in M$, the product of the function $\mathrm{snoc}(f, x) \colon \mathrm{Fin}(n+1) \to M$ over all elements of $\mathrm{Fin}(n+1)$ equals the product of $f$ over $\mathrm{Fin}(n)$ multiplied by $x$. In symbols: \[ \prod_{i \in \mathrm{Fin}(n+1)} \mathrm{snoc}(f, x)(i) = \left(\prod_{i \in \mathrm{Fin}(n)} f(i)\right) \cdot x. \]

Fin.prod_univ_one theorem

(f : Fin 1 → M) : ∏ i, f i = f 0

Full source

@[to_additive sum_univ_one]
theorem prod_univ_one (f : Fin 1 → M) : ∏ i, f i = f 0 := by simp

Product over $\mathrm{Fin}(1)$ equals $f(0)$

Informal description

For any commutative monoid $M$ and any function $f \colon \mathrm{Fin}(1) \to M$, the product of $f$ over all elements of $\mathrm{Fin}(1)$ is equal to $f(0)$. In other words, $\prod_{i \in \mathrm{Fin}(1)} f(i) = f(0)$.

Fin.prod_univ_two theorem

(f : Fin 2 → M) : ∏ i, f i = f 0 * f 1

Full source

@[to_additive (attr := simp)]
theorem prod_univ_two (f : Fin 2 → M) : ∏ i, f i = f 0 * f 1 := by
  simp [prod_univ_succ]

Product over $\mathrm{Fin}(2)$ decomposes into $f(0) \cdot f(1)$

Informal description

For any commutative monoid $M$ and any function $f \colon \mathrm{Fin}(2) \to M$, the product of $f$ over all elements of $\mathrm{Fin}(2)$ is equal to $f(0)$ multiplied by $f(1)$. In symbols: \[ \prod_{i \in \mathrm{Fin}(2)} f(i) = f(0) \cdot f(1). \]

Fin.prod_univ_two' theorem

(f : α → M) (a b : α) : ∏ i, f (![a, b] i) = f a * f b

Full source

@[to_additive]
theorem prod_univ_two' (f : α → M) (a b : α) : ∏ i, f (![a, b] i) = f a * f b :=
  prod_univ_two _

Product over Two-Element Vector Equals Product of Components

Informal description

For any commutative monoid $M$ and any function $f \colon \alpha \to M$, and for any two elements $a, b \in \alpha$, the product of $f$ over the vector $\begin{bmatrix}a & b\end{bmatrix}$ is equal to $f(a) \cdot f(b)$. In symbols: \[ \prod_{i \in \mathrm{Fin}(2)} f\!\left(\begin{bmatrix}a & b\end{bmatrix}_i\right) = f(a) \cdot f(b). \]

Fin.prod_univ_three theorem

(f : Fin 3 → M) : ∏ i, f i = f 0 * f 1 * f 2

Full source

@[to_additive]
theorem prod_univ_three (f : Fin 3 → M) : ∏ i, f i = f 0 * f 1 * f 2 := by
  rw [prod_univ_castSucc, prod_univ_two]
  rfl

Product over $\mathrm{Fin}(3)$ decomposes into $f(0) \cdot f(1) \cdot f(2)$

Informal description

Let $M$ be a commutative monoid. For any function $f \colon \mathrm{Fin}(3) \to M$, the product of $f$ over all elements of $\mathrm{Fin}(3)$ is equal to $f(0) \cdot f(1) \cdot f(2)$. In symbols: \[ \prod_{i \in \mathrm{Fin}(3)} f(i) = f(0) \cdot f(1) \cdot f(2). \]

Fin.prod_univ_four theorem

(f : Fin 4 → M) : ∏ i, f i = f 0 * f 1 * f 2 * f 3

Full source

@[to_additive]
theorem prod_univ_four (f : Fin 4 → M) : ∏ i, f i = f 0 * f 1 * f 2 * f 3 := by
  rw [prod_univ_castSucc, prod_univ_three]
  rfl

Product over $\mathrm{Fin}(4)$ decomposes into $f(0) \cdot f(1) \cdot f(2) \cdot f(3)$

Informal description

Let $M$ be a commutative monoid. For any function $f \colon \mathrm{Fin}(4) \to M$, the product of $f$ over all elements of $\mathrm{Fin}(4)$ is equal to $f(0) \cdot f(1) \cdot f(2) \cdot f(3)$. In symbols: \[ \prod_{i \in \mathrm{Fin}(4)} f(i) = f(0) \cdot f(1) \cdot f(2) \cdot f(3). \]

Fin.prod_univ_five theorem

(f : Fin 5 → M) : ∏ i, f i = f 0 * f 1 * f 2 * f 3 * f 4

Full source

@[to_additive]
theorem prod_univ_five (f : Fin 5 → M) : ∏ i, f i = f 0 * f 1 * f 2 * f 3 * f 4 := by
  rw [prod_univ_castSucc, prod_univ_four]
  rfl

Product over $\mathrm{Fin}(5)$ decomposes into $f(0) \cdot f(1) \cdot f(2) \cdot f(3) \cdot f(4)$

Informal description

Let $M$ be a commutative monoid. For any function $f \colon \mathrm{Fin}(5) \to M$, the product of $f$ over all elements of $\mathrm{Fin}(5)$ is equal to $f(0) \cdot f(1) \cdot f(2) \cdot f(3) \cdot f(4)$. In symbols: \[ \prod_{i \in \mathrm{Fin}(5)} f(i) = f(0) \cdot f(1) \cdot f(2) \cdot f(3) \cdot f(4). \]

Fin.prod_univ_six theorem

(f : Fin 6 → M) : ∏ i, f i = f 0 * f 1 * f 2 * f 3 * f 4 * f 5

Full source

@[to_additive]
theorem prod_univ_six (f : Fin 6 → M) : ∏ i, f i = f 0 * f 1 * f 2 * f 3 * f 4 * f 5 := by
  rw [prod_univ_castSucc, prod_univ_five]
  rfl

Product over $\mathrm{Fin}(6)$ decomposes into $f(0) \cdot f(1) \cdot f(2) \cdot f(3) \cdot f(4) \cdot f(5)$

Informal description

Let $M$ be a commutative monoid. For any function $f \colon \mathrm{Fin}(6) \to M$, the product of $f$ over all elements of $\mathrm{Fin}(6)$ is equal to $f(0) \cdot f(1) \cdot f(2) \cdot f(3) \cdot f(4) \cdot f(5)$. In symbols: \[ \prod_{i \in \mathrm{Fin}(6)} f(i) = f(0) \cdot f(1) \cdot f(2) \cdot f(3) \cdot f(4) \cdot f(5). \]

Fin.prod_univ_seven theorem

(f : Fin 7 → M) : ∏ i, f i = f 0 * f 1 * f 2 * f 3 * f 4 * f 5 * f 6

Full source

@[to_additive]
theorem prod_univ_seven (f : Fin 7 → M) : ∏ i, f i = f 0 * f 1 * f 2 * f 3 * f 4 * f 5 * f 6 := by
  rw [prod_univ_castSucc, prod_univ_six]
  rfl

Product over $\mathrm{Fin}(7)$ decomposes into $f(0) \cdot f(1) \cdot f(2) \cdot f(3) \cdot f(4) \cdot f(5) \cdot f(6)$

Informal description

Let $M$ be a commutative monoid. For any function $f \colon \mathrm{Fin}(7) \to M$, the product of $f$ over all elements of $\mathrm{Fin}(7)$ is equal to $f(0) \cdot f(1) \cdot f(2) \cdot f(3) \cdot f(4) \cdot f(5) \cdot f(6)$. In symbols: \[ \prod_{i \in \mathrm{Fin}(7)} f(i) = f(0) \cdot f(1) \cdot f(2) \cdot f(3) \cdot f(4) \cdot f(5) \cdot f(6). \]

Fin.prod_univ_eight theorem

(f : Fin 8 → M) : ∏ i, f i = f 0 * f 1 * f 2 * f 3 * f 4 * f 5 * f 6 * f 7

Full source

@[to_additive]
theorem prod_univ_eight (f : Fin 8 → M) :
    ∏ i, f i = f 0 * f 1 * f 2 * f 3 * f 4 * f 5 * f 6 * f 7 := by
  rw [prod_univ_castSucc, prod_univ_seven]
  rfl

Product over $\mathrm{Fin}(8)$ decomposes into $f(0) \cdot f(1) \cdot f(2) \cdot f(3) \cdot f(4) \cdot f(5) \cdot f(6) \cdot f(7)$

Informal description

Let $M$ be a commutative monoid. For any function $f \colon \mathrm{Fin}(8) \to M$, the product of $f$ over all elements of $\mathrm{Fin}(8)$ is equal to $f(0) \cdot f(1) \cdot f(2) \cdot f(3) \cdot f(4) \cdot f(5) \cdot f(6) \cdot f(7)$. In symbols: \[ \prod_{i \in \mathrm{Fin}(8)} f(i) = f(0) \cdot f(1) \cdot f(2) \cdot f(3) \cdot f(4) \cdot f(5) \cdot f(6) \cdot f(7). \]

Fin.prod_const theorem

(n : ℕ) (x : M) : ∏ _i : Fin n, x = x ^ n

Full source

@[to_additive]
theorem prod_const (n : ℕ) (x : M) : ∏ _i : Fin n, x = x ^ n := by simp

Product of a Constant Function over $\mathrm{Fin}(n)$ Equals $x^n$

Informal description

For any natural number $n$ and any element $x$ in a commutative monoid $M$, the product of $x$ over all elements of the finite type $\mathrm{Fin}(n)$ is equal to $x$ raised to the power $n$, i.e., \[ \prod_{i \in \mathrm{Fin}(n)} x = x^n. \]

Fin.prod_Ioi_zero theorem

{v : Fin n.succ → M} : ∏ i ∈ Ioi 0, v i = ∏ j : Fin n, v j.succ

Full source

@[to_additive]
theorem prod_Ioi_zero {v : Fin n.succ → M} :
    ∏ i ∈ Ioi 0, v i = ∏ j : Fin n, v j.succ := by
  rw [Ioi_zero_eq_map, Finset.prod_map, coe_succEmb]

Product over Open Upper Interval at Zero in $\mathrm{Fin}(n+1)$ Equals Product of Successors over $\mathrm{Fin}(n)$

Informal description

For any function $v : \mathrm{Fin}(n+1) \to M$ where $M$ is a commutative monoid, the product of $v$ over the open interval $(0, \infty)$ in $\mathrm{Fin}(n+1)$ is equal to the product of $v \circ \mathrm{succ}$ over all elements of $\mathrm{Fin}(n)$. In symbols: \[ \prod_{i \in (0, \infty)} v(i) = \prod_{j \in \mathrm{Fin}(n)} v(j.\mathrm{succ}). \]

Fin.prod_Ioi_succ theorem

(i : Fin n) (v : Fin n.succ → M) : ∏ j ∈ Ioi i.succ, v j = ∏ j ∈ Ioi i, v j.succ

Full source

@[to_additive (attr := simp)]
theorem prod_Ioi_succ (i : Fin n) (v : Fin n.succ → M) :
    ∏ j ∈ Ioi i.succ, v j = ∏ j ∈ Ioi i, v j.succ := by
  rw [← map_succEmb_Ioi, Finset.prod_map, coe_succEmb]

Product over Successor Interval in $\mathrm{Fin}(n+1)$ Equals Product over Predecessor Interval in $\mathrm{Fin}(n)$

Informal description

For any element $i \in \mathrm{Fin}(n)$ and any function $v : \mathrm{Fin}(n+1) \to M$ where $M$ is a commutative monoid, the product of $v$ over the open interval $(i.\mathrm{succ}, \infty)$ in $\mathrm{Fin}(n+1)$ is equal to the product of $v \circ \mathrm{succ}$ over the open interval $(i, \infty)$ in $\mathrm{Fin}(n)$. In symbols: \[ \prod_{j \in (i.\mathrm{succ}, \infty)} v(j) = \prod_{j \in (i, \infty)} v(j.\mathrm{succ}). \]

Fin.prod_congr' theorem

{a b : ℕ} (f : Fin b → M) (h : a = b) : (∏ i : Fin a, f (i.cast h)) = ∏ i : Fin b, f i

Full source

@[to_additive]
theorem prod_congr' {a b : ℕ} (f : Fin b → M) (h : a = b) :
    (∏ i : Fin a, f (i.cast h)) = ∏ i : Fin b, f i := by
  subst h
  congr

Product Equality under Casting of Finite Ordinals

Informal description

Let $a$ and $b$ be natural numbers, and let $f : \mathrm{Fin}(b) \to M$ be a function. If $a = b$, then the product of $f$ over all elements of $\mathrm{Fin}(a)$ (with elements cast via the equality $h : a = b$) is equal to the product of $f$ over all elements of $\mathrm{Fin}(b)$. In other words, for any equality $h : a = b$, we have: \[ \prod_{i \in \mathrm{Fin}(a)} f(i.\mathrm{cast}\, h) = \prod_{i \in \mathrm{Fin}(b)} f(i). \]

Fin.prod_univ_add theorem

 {a b : ℕ} (f : Fin (a + b) → M) :
  (∏ i : Fin (a + b), f i) = (∏ i : Fin a, f (castAdd b i)) * ∏ i : Fin b, f (natAdd a i)

Full source

@[to_additive]
theorem prod_univ_add {a b : ℕ} (f : Fin (a + b) → M) :
    (∏ i : Fin (a + b), f i) = (∏ i : Fin a, f (castAdd b i)) * ∏ i : Fin b, f (natAdd a i) := by
  rw [Fintype.prod_equiv finSumFinEquiv.symm f fun i => f (finSumFinEquiv.toFun i)]
  · apply Fintype.prod_sum_type
  · intro x
    simp only [Equiv.toFun_as_coe, Equiv.apply_symm_apply]

Product Decomposition over $\mathrm{Fin}(a + b)$ via Cast and Shift Embeddings

Informal description

Let $M$ be a commutative monoid, and let $a, b$ be natural numbers. For any function $f : \mathrm{Fin}(a + b) \to M$, the product of $f$ over all elements of $\mathrm{Fin}(a + b)$ equals the product of $f$ over the first $a$ elements (via the embedding $\mathrm{castAdd}\,b$) multiplied by the product of $f$ over the remaining $b$ elements (via the embedding $\mathrm{natAdd}\,a$). In other words: \[ \prod_{i \in \mathrm{Fin}(a + b)} f(i) = \left(\prod_{i \in \mathrm{Fin}(a)} f(\mathrm{castAdd}\,b\,i)\right) \times \left(\prod_{i \in \mathrm{Fin}(b)} f(\mathrm{natAdd}\,a\,i)\right). \]

Fin.prod_trunc theorem

 {a b : ℕ} (f : Fin (a + b) → M) (hf : ∀ j : Fin b, f (natAdd a j) = 1) :
  (∏ i : Fin (a + b), f i) = ∏ i : Fin a, f (castAdd b i)

Full source

@[to_additive]
theorem prod_trunc {a b : ℕ} (f : Fin (a + b) → M) (hf : ∀ j : Fin b, f (natAdd a j) = 1) :
    (∏ i : Fin (a + b), f i) = ∏ i : Fin a, f (castAdd b i) := by
  rw [prod_univ_add, Fintype.prod_eq_one _ hf, mul_one]

Truncated Product Equality for $\mathrm{Fin}(a + b)$ with Vanishing Tail

Informal description

Let $M$ be a commutative monoid, and let $a, b$ be natural numbers. Given a function $f \colon \mathrm{Fin}(a + b) \to M$ such that $f(j) = 1$ for all $j \in \mathrm{Fin}(b)$ (where $j$ is embedded into $\mathrm{Fin}(a + b)$ via $\mathrm{natAdd}\,a$), the product of $f$ over all elements of $\mathrm{Fin}(a + b)$ equals the product of $f$ over the first $a$ elements (embedded via $\mathrm{castAdd}\,b$). In other words: \[ \prod_{i \in \mathrm{Fin}(a + b)} f(i) = \prod_{i \in \mathrm{Fin}(a)} f(\mathrm{castAdd}\,b\,i). \]

Fin.sum_pow_mul_eq_add_pow theorem

 {n : ℕ} {R : Type*} [CommSemiring R] (a b : R) : (∑ s : Finset (Fin n), a ^ s.card * b ^ (n - s.card)) = (a + b) ^ n

Full source

theorem sum_pow_mul_eq_add_pow {n : ℕ} {R : Type*} [CommSemiring R] (a b : R) :
    (∑ s : Finset (Fin n), a ^ s.card * b ^ (n - s.card)) = (a + b) ^ n := by
  simpa using Fintype.sum_pow_mul_eq_add_pow (Fin n) a b

Binomial Expansion over Finite Ordinals: $\sum_{s \subseteq \mathrm{Fin}(n)} a^{|s|} b^{n - |s|} = (a + b)^n$

Informal description

Let $R$ be a commutative semiring, and let $a, b \in R$. For any natural number $n$, the sum over all subsets $s$ of $\mathrm{Fin}(n)$ of the product $a^{|s|} \cdot b^{n - |s|}$ equals $(a + b)^n$. In other words, \[ \sum_{s \subseteq \mathrm{Fin}(n)} a^{|s|} b^{n - |s|} = (a + b)^n. \]

Fin.sum_neg_one_pow theorem

(R : Type*) [Ring R] (m : ℕ) : (∑ n : Fin m, (-1) ^ n.1 : R) = if Even m then 0 else 1

Full source

lemma sum_neg_one_pow (R : Type*) [Ring R] (m : ℕ) :
    (∑ n : Fin m, (-1) ^ n.1 : R) = if Even m then 0 else 1 := by
  induction m with
  | zero => simp
  | succ n IH =>
    simp only [Fin.sum_univ_castSucc, Fin.coe_castSucc, IH, Fin.val_last,
      Nat.even_add_one, ← Nat.not_even_iff_odd, ite_not]
    split_ifs with h
    · simp [*]
    · simp [(Nat.not_even_iff_odd.mp h).neg_pow]

Alternating Sum over $\mathrm{Fin}(m)$: $\sum_{n \in \mathrm{Fin}(m)} (-1)^n = \begin{cases} 0 & \text{if } m \text{ is even} \\ 1 & \text{if } m \text{ is odd} \end{cases}$

Informal description

Let $R$ be a ring and $m$ be a natural number. The sum $\sum_{n \in \mathrm{Fin}(m)} (-1)^{n}$ over the finite ordinal $\mathrm{Fin}(m)$ equals $0$ if $m$ is even, and $1$ if $m$ is odd.

Fin.partialProd definition

(f : Fin n → α) (i : Fin (n + 1)) : α

Full source

/-- For `f = (a₁, ..., aₙ)` in `αⁿ`, `partialProd f` is `(1, a₁, a₁a₂, ..., a₁...aₙ)` in `αⁿ⁺¹`. -/
@[to_additive "For `f = (a₁, ..., aₙ)` in `αⁿ`, `partialSum f` is\n
`(0, a₁, a₁ + a₂, ..., a₁ + ... + aₙ)` in `αⁿ⁺¹`."]
def partialProd (f : Fin n → α) (i : Fin (n + 1)) : α :=
  ((List.ofFn f).take i).prod

Partial product of a sequence in a monoid

Informal description

For a function $ f = (a_1, \ldots, a_n) $ defined on the finite type $ \text{Fin} \, n $ with values in a monoid $ \alpha $, the partial product $ \text{partialProd} \, f $ is the sequence $ (1, a_1, a_1a_2, \ldots, a_1 \cdots a_n) $ in $ \alpha^{n+1} $. Specifically, for each $ i : \text{Fin} (n + 1) $, the $ i $-th element of the sequence is the product of the first $ i $ elements of $ f $.

Fin.partialProd_zero theorem

(f : Fin n → α) : partialProd f 0 = 1

Full source

@[to_additive (attr := simp)]
theorem partialProd_zero (f : Fin n → α) : partialProd f 0 = 1 := by simp [partialProd]

Initial Term of Partial Product Sequence is Identity

Informal description

For any function $ f $ defined on the finite type $ \text{Fin} \, n $ with values in a monoid $ \alpha $, the initial term of the partial product sequence is the multiplicative identity, i.e., $ \text{partialProd} \, f \, 0 = 1 $.

Fin.partialProd_succ theorem

(f : Fin n → α) (j : Fin n) : partialProd f j.succ = partialProd f (Fin.castSucc j) * f j

Full source

@[to_additive]
theorem partialProd_succ (f : Fin n → α) (j : Fin n) :
    partialProd f j.succ = partialProd f (Fin.castSucc j) * f j := by
  simp [partialProd, List.take_succ, List.ofFnNthVal, dif_pos j.is_lt]

Recursive formula for partial products in $\mathrm{Fin}\,n$

Informal description

Let $\alpha$ be a monoid and $f \colon \mathrm{Fin}\,n \to \alpha$ be a function. For any $j \in \mathrm{Fin}\,n$, the partial product up to $j+1$ equals the partial product up to $j$ multiplied by $f(j)$. That is, \[ \mathrm{partialProd}\,f\,(j+1) = (\mathrm{partialProd}\,f\,j) \cdot f(j). \]

Fin.partialProd_succ' theorem

(f : Fin (n + 1) → α) (j : Fin (n + 1)) : partialProd f j.succ = f 0 * partialProd (Fin.tail f) j

Full source

@[to_additive]
theorem partialProd_succ' (f : Fin (n + 1) → α) (j : Fin (n + 1)) :
    partialProd f j.succ = f 0 * partialProd (Fin.tail f) j := by
  simp [partialProd]
  rfl

Recursive formula for partial products in a monoid

Informal description

Let $\alpha$ be a monoid and $f : \text{Fin}(n+1) \to \alpha$ be a function. For any $j \in \text{Fin}(n+1)$, the partial product up to $j+1$ is equal to the product of $f(0)$ with the partial product up to $j$ of the tail of $f$. That is, \[ \text{partialProd}\, f\, (j+1) = f(0) \cdot \text{partialProd}\, (\text{tail}\, f)\, j. \]

Fin.partialProd_left_inv theorem

{G : Type*} [Group G] (f : Fin (n + 1) → G) : (f 0 • partialProd fun i : Fin n => (f i)⁻¹ * f i.succ) = f

Full source

@[to_additive]
theorem partialProd_left_inv {G : Type*} [Group G] (f : Fin (n + 1) → G) :
    (f 0 • partialProd fun i : Fin n => (f i)⁻¹ * f i.succ) = f :=
  funext fun x => Fin.inductionOn x (by simp) fun x hx => by
    simp only [coe_eq_castSucc, Pi.smul_apply, smul_eq_mul] at hx ⊢
    rw [partialProd_succ, ← mul_assoc, hx, mul_inv_cancel_left]

Left Inverse Property of Partial Products in Finite Groups: $f(0) \cdot \prod_{i} (f(i)^{-1} \cdot f(i+1)) = f$

Informal description

Let $G$ be a group and $f \colon \mathrm{Fin}(n+1) \to G$ be a function. Then the action of $f(0)$ on the partial product of the sequence $\left(f(i)^{-1} \cdot f(i+1)\right)_{i \in \mathrm{Fin}\,n}$ recovers the original function $f$. That is, \[ f(0) \cdot \prod_{i=0}^{n-1} \left(f(i)^{-1} \cdot f(i+1)\right) = f. \]

Fin.partialProd_right_inv theorem

 {G : Type*} [Group G] (f : Fin n → G) (i : Fin n) : (partialProd f (Fin.castSucc i))⁻¹ * partialProd f i.succ = f i

Full source

@[to_additive]
theorem partialProd_right_inv {G : Type*} [Group G] (f : Fin n → G) (i : Fin n) :
    (partialProd f (Fin.castSucc i))⁻¹ * partialProd f i.succ = f i := by
  rw [partialProd_succ, inv_mul_cancel_left]

Inverse Partial Product Recursion in $\mathrm{Fin}\,n$: $(\mathrm{partialProd}\,f\,i)^{-1} \cdot \mathrm{partialProd}\,f\,(i+1) = f(i)$

Informal description

Let $G$ be a group and $f \colon \mathrm{Fin}\,n \to G$ be a function. For any $i \in \mathrm{Fin}\,n$, the product of the inverse of the partial product up to $i$ with the partial product up to $i+1$ equals $f(i)$. That is, \[ \left(\mathrm{partialProd}\,f\,i\right)^{-1} \cdot \mathrm{partialProd}\,f\,(i+1) = f(i). \]

Fin.inv_partialProd_mul_eq_contractNth theorem

 {G : Type*} [Group G] (g : Fin (n + 1) → G) (j : Fin (n + 1)) (k : Fin n) :
  (partialProd g (j.succ.succAbove (Fin.castSucc k)))⁻¹ * partialProd g (j.succAbove k).succ = j.contractNth (· * ·) g k

Full source

/-- Let `(g₀, g₁, ..., gₙ)` be a tuple of elements in `Gⁿ⁺¹`.
Then if `k < j`, this says `(g₀g₁...gₖ₋₁)⁻¹ * g₀g₁...gₖ = gₖ`.
If `k = j`, it says `(g₀g₁...gₖ₋₁)⁻¹ * g₀g₁...gₖ₊₁ = gₖgₖ₊₁`.
If `k > j`, it says `(g₀g₁...gₖ)⁻¹ * g₀g₁...gₖ₊₁ = gₖ₊₁.`
Useful for defining group cohomology. -/
@[to_additive
      "Let `(g₀, g₁, ..., gₙ)` be a tuple of elements in `Gⁿ⁺¹`.
      Then if `k < j`, this says `-(g₀ + g₁ + ... + gₖ₋₁) + (g₀ + g₁ + ... + gₖ) = gₖ`.
      If `k = j`, it says `-(g₀ + g₁ + ... + gₖ₋₁) + (g₀ + g₁ + ... + gₖ₊₁) = gₖ + gₖ₊₁`.
      If `k > j`, it says `-(g₀ + g₁ + ... + gₖ) + (g₀ + g₁ + ... + gₖ₊₁) = gₖ₊₁.`
      Useful for defining group cohomology."]
theorem inv_partialProd_mul_eq_contractNth {G : Type*} [Group G] (g : Fin (n + 1) → G)
    (j : Fin (n + 1)) (k : Fin n) :
    (partialProd g (j.succ.succAbove (Fin.castSucc k)))⁻¹ * partialProd g (j.succAbove k).succ =
      j.contractNth (· * ·) g k := by
  rcases lt_trichotomy (k : ℕ) j with (h | h | h)
  · rwa [succAbove_of_castSucc_lt, succAbove_of_castSucc_lt, partialProd_right_inv,
    contractNth_apply_of_lt]
    · assumption
    · rw [castSucc_lt_iff_succ_le, succ_le_succ_iff, le_iff_val_le_val]
      exact le_of_lt h
  · rwa [succAbove_of_castSucc_lt, succAbove_of_le_castSucc, partialProd_succ,
    castSucc_fin_succ, ← mul_assoc,
      partialProd_right_inv, contractNth_apply_of_eq]
    · simp [le_iff_val_le_val, ← h]
    · rw [castSucc_lt_iff_succ_le, succ_le_succ_iff, le_iff_val_le_val]
      exact le_of_eq h
  · rwa [succAbove_of_le_castSucc, succAbove_of_le_castSucc, partialProd_succ, partialProd_succ,
      castSucc_fin_succ, partialProd_succ, inv_mul_cancel_left, contractNth_apply_of_gt]
    · exact le_iff_val_le_val.2 (le_of_lt h)
    · rw [le_iff_val_le_val, val_succ]
      exact Nat.succ_le_of_lt h

Inverse Partial Product Relation for Contracted Tuples in Groups

Informal description

Let $G$ be a group and $g = (g_0, g_1, \ldots, g_n)$ be a tuple of elements in $G^{n+1}$. For any position $j \in \mathrm{Fin}(n+1)$ and index $k \in \mathrm{Fin}(n)$, the following identity holds: \[ \left(\prod_{i=0}^{j.\mathrm{succAbove}(\mathrm{castSucc}\,k)} g_i\right)^{-1} \cdot \left(\prod_{i=0}^{(j.\mathrm{succAbove}\,k).\mathrm{succ}} g_i\right) = j.\mathrm{contractNth}\,(\cdot)\,g\,k \] where: - If $k < j$, the right side equals $g_k$. - If $k = j$, the right side equals $g_k \cdot g_{k+1}$. - If $k > j$, the right side equals $g_{k+1}$.

finFunctionFinEquiv definition

{m n : ℕ} : (Fin n → Fin m) ≃ Fin (m ^ n)

Full source

/-- Equivalence between `Fin n → Fin m` and `Fin (m ^ n)`. -/
@[simps!]
def finFunctionFinEquiv {m n : ℕ} : (Fin n → Fin m) ≃ Fin (m ^ n) :=
  Equiv.ofRightInverseOfCardLE (le_of_eq <| by simp_rw [Fintype.card_fun, Fintype.card_fin])
    (fun f => ⟨∑ i, f i * m ^ (i : ℕ), by
      induction n with
      | zero => simp
      | succ n ih =>
        cases m
        · exact isEmptyElim (f <| Fin.last _)
        simp_rw [Fin.sum_univ_castSucc, Fin.coe_castSucc, Fin.val_last]
        refine (Nat.add_lt_add_of_lt_of_le (ih _) <| Nat.mul_le_mul_right _
          (Fin.is_le _)).trans_eq ?_
        rw [← one_add_mul (_ : ℕ), add_comm, pow_succ']⟩)
    (fun a b => ⟨a / m ^ (b : ℕ) % m, by
      rcases n with - | n
      · exact b.elim0
      rcases m with - | m
      · rw [zero_pow n.succ_ne_zero] at a
        exact a.elim0
      · exact Nat.mod_lt _ m.succ_pos⟩)
    fun a => by
      dsimp
      induction n with
      | zero => subsingleton [(finCongr <| pow_zero _).subsingleton]
      | succ n ih =>
        simp_rw [Fin.forall_iff, Fin.ext_iff] at ih
        ext
        simp_rw [Fin.sum_univ_succ, Fin.val_zero, Fin.val_succ, pow_zero, Nat.div_one,
          mul_one, pow_succ', ← Nat.div_div_eq_div_mul, mul_left_comm _ m, ← mul_sum]
        rw [ih _ (Nat.div_lt_of_lt_mul (a.is_lt.trans_eq (pow_succ' _ _))), Nat.mod_add_div]

Equivalence between function space $\mathrm{Fin}\,n \to \mathrm{Fin}\,m$ and $\mathrm{Fin}(m^n)$

Informal description

The equivalence between the type of functions $\mathrm{Fin}\,n \to \mathrm{Fin}\,m$ and the finite ordinal $\mathrm{Fin}(m^n)$. Given a function $f \colon \mathrm{Fin}\,n \to \mathrm{Fin}\,m$, its corresponding element in $\mathrm{Fin}(m^n)$ is obtained by interpreting $f$ as an $m$-ary digit number with $n$ digits, where the $i$-th digit is $f(i)$ (for $i \in \mathrm{Fin}\,n$). Specifically, the equivalence maps $f$ to the natural number $\sum_{i=0}^{n-1} f(i) \cdot m^i$ modulo $m^n$. Conversely, given $k \in \mathrm{Fin}(m^n)$, the corresponding function is defined by $i \mapsto \left\lfloor \frac{k}{m^i} \right\rfloor \bmod m$ for each $i \in \mathrm{Fin}\,n$.

finFunctionFinEquiv_apply theorem

{m n : ℕ} (f : Fin n → Fin m) : (finFunctionFinEquiv f : ℕ) = ∑ i : Fin n, ↑(f i) * m ^ (i : ℕ)

Full source

theorem finFunctionFinEquiv_apply {m n : ℕ} (f : Fin n → Fin m) :
    (finFunctionFinEquiv f : ℕ) = ∑ i : Fin n, ↑(f i) * m ^ (i : ℕ) :=
  rfl

Explicit Formula for the Equivalence between $\mathrm{Fin}(n) \to \mathrm{Fin}(m)$ and $\mathrm{Fin}(m^n)$

Informal description

For any natural numbers $m$ and $n$, and any function $f \colon \mathrm{Fin}(n) \to \mathrm{Fin}(m)$, the natural number corresponding to $f$ under the equivalence $\mathrm{Fin}(n) \to \mathrm{Fin}(m) \simeq \mathrm{Fin}(m^n)$ is given by: \[ \sum_{i=0}^{n-1} f(i) \cdot m^i \] where $f(i)$ is treated as a natural number via the canonical embedding $\mathrm{Fin}(m) \hookrightarrow \mathbb{N}$.

finFunctionFinEquiv_single theorem

{m n : ℕ} [NeZero m] (i : Fin n) (j : Fin m) : (finFunctionFinEquiv (Pi.single i j) : ℕ) = j * m ^ (i : ℕ)

Full source

theorem finFunctionFinEquiv_single {m n : ℕ} [NeZero m] (i : Fin n) (j : Fin m) :
    (finFunctionFinEquiv (Pi.single i j) : ℕ) = j * m ^ (i : ℕ) := by
  rw [finFunctionFinEquiv_apply, Fintype.sum_eq_single i, Pi.single_eq_same]
  rintro x hx
  rw [Pi.single_eq_of_ne hx, Fin.val_zero, zero_mul]

Image of Point Function under $\mathrm{Fin}(n) \to \mathrm{Fin}(m) \simeq \mathrm{Fin}(m^n)$ Equivalence: $j \cdot m^i$

Informal description

For any natural numbers $m$ and $n$ with $m \neq 0$, and for any indices $i \in \mathrm{Fin}(n)$ and $j \in \mathrm{Fin}(m)$, the equivalence `finFunctionFinEquiv` maps the function $\mathrm{Pi.single}(i, j)$ (which is $j$ at $i$ and $0$ elsewhere) to the natural number $j \cdot m^i$.

finPiFinEquiv definition

{m : ℕ} {n : Fin m → ℕ} : (∀ i : Fin m, Fin (n i)) ≃ Fin (∏ i : Fin m, n i)

Full source

/-- Equivalence between `∀ i : Fin m, Fin (n i)` and `Fin (∏ i : Fin m, n i)`. -/
def finPiFinEquiv {m : ℕ} {n : Fin m → ℕ} : (∀ i : Fin m, Fin (n i)) ≃ Fin (∏ i : Fin m, n i) :=
  Equiv.ofRightInverseOfCardLE (le_of_eq <| by simp_rw [Fintype.card_pi, Fintype.card_fin])
    (fun f => ⟨∑ i, f i * ∏ j, n (Fin.castLE i.is_lt.le j), by
      induction m with
      | zero => simp
      | succ m ih =>
      rw [Fin.prod_univ_castSucc, Fin.sum_univ_castSucc]
      suffices
        ∀ (n : Fin m → ℕ) (nn : ℕ) (f : ∀ i : Fin m, Fin (n i)) (fn : Fin nn),
          ((∑ i : Fin m, ↑(f i) * ∏ j : Fin i, n (Fin.castLE i.prop.le j)) + ↑fn * ∏ j, n j) <
            (∏ i : Fin m, n i) * nn by
        replace := this (Fin.init n) (n (Fin.last _)) (Fin.init f) (f (Fin.last _))
        rw [← Fin.snoc_init_self f]
        simp +singlePass only [← Fin.snoc_init_self n]
        simp_rw [Fin.snoc_castSucc, Fin.snoc_last, Fin.snoc_init_self n]
        exact this
      intro n nn f fn
      cases nn
      · exact isEmptyElim fn
      refine (Nat.add_lt_add_of_lt_of_le (ih _) <| Nat.mul_le_mul_right _ (Fin.is_le _)).trans_eq ?_
      rw [← one_add_mul (_ : ℕ), mul_comm, add_comm]⟩)
    (fun a b => ⟨(a / ∏ j : Fin b, n (Fin.castLE b.is_lt.le j)) % n b, by
      cases m
      · exact b.elim0
      rcases h : n b with nb | nb
      · rw [prod_eq_zero (Finset.mem_univ _) h] at a
        exact isEmptyElim a
      exact Nat.mod_lt _ nb.succ_pos⟩)
    (by
      intro a; revert a; dsimp only [Fin.val_mk]
      refine Fin.consInduction ?_ ?_ n
      · intro a
        have : Subsingleton (Fin (∏ i : Fin 0, i.elim0)) :=
          (finCongr <| prod_empty).subsingleton
        subsingleton
      · intro n x xs ih a
        simp_rw [Fin.forall_iff, Fin.ext_iff] at ih
        ext
        simp_rw [Fin.sum_univ_succ, Fin.cons_succ]
        have := fun i : Fin n =>
          Fintype.prod_equiv (finCongr <| Fin.val_succ i)
            (fun j => (Fin.cons x xs : _ → ℕ) (Fin.castLE (Fin.is_lt _).le j))
            (fun j => (Fin.cons x xs : _ → ℕ) (Fin.castLE (Nat.succ_le_succ (Fin.is_lt _).le) j))
            fun j => rfl
        simp_rw [this]
        clear this
        simp_rw [Fin.val_zero, Fintype.prod_empty, Nat.div_one, mul_one, Fin.cons_zero,
          Fin.prod_univ_succ, Fin.castLE_zero, Fin.cons_zero, ← Nat.div_div_eq_div_mul,
          mul_left_comm (_ % _ : ℕ), ← mul_sum]
        convert Nat.mod_add_div _ _
        exact ih (a / x) (Nat.div_lt_of_lt_mul <| a.is_lt.trans_eq (Fin.prod_univ_succ _)))

Equivalence between dependent functions on finite ordinals and finite product ordinals

Informal description

Given a natural number $m$ and a family of natural numbers $(n_i)_{i \in \mathrm{Fin}(m)}$, there is an explicit equivalence (bijection) between the type of functions $\forall i : \mathrm{Fin}(m), \mathrm{Fin}(n_i)$ and the finite ordinal $\mathrm{Fin}(\prod_{i \in \mathrm{Fin}(m)} n_i)$. The forward map sends a function $f$ to the natural number $\sum_{i} f(i) \cdot \prod_{j} n_j$ where the product is taken over indices $j$ with $i < j < m$. The inverse map reconstructs the function from this natural number using division and modulo operations.

finPiFinEquiv_apply theorem

 {m : ℕ} {n : Fin m → ℕ} (f : ∀ i : Fin m, Fin (n i)) :
  (finPiFinEquiv f : ℕ) = ∑ i, f i * ∏ j, n (Fin.castLE i.is_lt.le j)

Full source

theorem finPiFinEquiv_apply {m : ℕ} {n : Fin m → ℕ} (f : ∀ i : Fin m, Fin (n i)) :
    (finPiFinEquiv f : ℕ) = ∑ i, f i * ∏ j, n (Fin.castLE i.is_lt.le j) := rfl

Explicit Formula for `finPiFinEquiv` Application

Informal description

For any natural number $m$ and a family of natural numbers $(n_i)_{i \in \mathrm{Fin}(m)}$, given a function $f : \forall i : \mathrm{Fin}(m), \mathrm{Fin}(n_i)$, the equivalence `finPiFinEquiv` maps $f$ to the natural number $\sum_{i} f(i) \cdot \prod_{j} n_j$, where the product is taken over indices $j$ with $i < j < m$.

finPiFinEquiv_single theorem

 {m : ℕ} {n : Fin m → ℕ} [∀ i, NeZero (n i)] (i : Fin m) (j : Fin (n i)) :
  (finPiFinEquiv (Pi.single i j : ∀ i : Fin m, Fin (n i)) : ℕ) = j * ∏ j, n (Fin.castLE i.is_lt.le j)

Full source

theorem finPiFinEquiv_single {m : ℕ} {n : Fin m → ℕ} [∀ i, NeZero (n i)] (i : Fin m)
    (j : Fin (n i)) :
    (finPiFinEquiv (Pi.single i j : ∀ i : Fin m, Fin (n i)) : ℕ) =
      j * ∏ j, n (Fin.castLE i.is_lt.le j) := by
  rw [finPiFinEquiv_apply, Fintype.sum_eq_single i, Pi.single_eq_same]
  rintro x hx
  rw [Pi.single_eq_of_ne hx, Fin.val_zero, zero_mul]

Image of Single Function under `finPiFinEquiv`: $j \cdot \prod_{j} n_j$

Informal description

For any natural number $m$ and a family of natural numbers $(n_i)_{i \in \mathrm{Fin}(m)}$ where each $n_i$ is nonzero, given an index $i \in \mathrm{Fin}(m)$ and an element $j \in \mathrm{Fin}(n_i)$, the equivalence `finPiFinEquiv` maps the function $\mathrm{Pi.single}(i, j)$ (which is $j$ at $i$ and $0$ elsewhere) to the natural number $j \cdot \prod_{j} n_j$, where the product is taken over indices $j$ with $i < j < m$.

finSigmaFinEquiv definition

{m : ℕ} {n : Fin m → ℕ} : (i : Fin m) × Fin (n i) ≃ Fin (∑ i : Fin m, n i)

Full source

/-- Equivalence between the Sigma type `(i : Fin m) × Fin (n i)` and `Fin (∑ i : Fin m, n i)`. -/
def finSigmaFinEquiv {m : ℕ} {n : Fin m → ℕ} : (i : Fin m) × Fin (n i)(i : Fin m) × Fin (n i) ≃ Fin (∑ i : Fin m, n i) :=
  match m with
  | 0 => @Equiv.equivOfIsEmpty _ _ _ (by simp; exact Fin.isEmpty')
  | Nat.succ m =>
    calc _ ≃ _ := (@finSumFinEquiv m 1).sigmaCongrLeft.symm
      _ ≃ _calc _ ≃ _ := (@finSumFinEquiv m 1).sigmaCongrLeft.symm
      _ ≃ _ := Equiv.sumSigmaDistrib _
      _ ≃ _calc _ ≃ _ := (@finSumFinEquiv m 1).sigmaCongrLeft.symm
      _ ≃ _ := Equiv.sumSigmaDistrib _
      _ ≃ _ := finSigmaFinEquiv.sumCongr (Equiv.uniqueSigma _)
      _ ≃ _calc _ ≃ _ := (@finSumFinEquiv m 1).sigmaCongrLeft.symm
      _ ≃ _ := Equiv.sumSigmaDistrib _
      _ ≃ _ := finSigmaFinEquiv.sumCongr (Equiv.uniqueSigma _)
      _ ≃ _ := finSumFinEquiv
      _ ≃ _ := finCongr (Fin.sum_univ_castSucc n).symm

Equivalence between dependent sums over finite types and finite sums

Informal description

Given a natural number $m$ and a family of natural numbers $n : \text{Fin}(m) \to \mathbb{N}$, there is an equivalence between the dependent sum type $(i : \text{Fin}(m)) \times \text{Fin}(n i)$ and the finite type $\text{Fin}(\sum_{i : \text{Fin}(m)} n i)$. This equivalence maps a pair $(i, j)$ where $i \in \text{Fin}(m)$ and $j \in \text{Fin}(n i)$ to the corresponding element in $\text{Fin}(\sum_{i} n i)$, and its inverse reconstructs the pair from an element of $\text{Fin}(\sum_{i} n i)$.

finSigmaFinEquiv_apply theorem

 {m : ℕ} {n : Fin m → ℕ} (k : (i : Fin m) × Fin (n i)) :
  (finSigmaFinEquiv k : ℕ) = ∑ i : Fin k.1, n (Fin.castLE k.1.2.le i) + k.2

Full source

@[simp]
theorem finSigmaFinEquiv_apply {m : ℕ} {n : Fin m → ℕ} (k : (i : Fin m) × Fin (n i)) :
    (finSigmaFinEquiv k : ℕ) = ∑ i : Fin k.1, n (Fin.castLE k.1.2.le i) + k.2 := by
  induction m with
  | zero => exact k.fst.elim0
  | succ m ih =>
  rcases k with ⟨⟨iv, hi⟩, j⟩
  rw [finSigmaFinEquiv]
  unfold finSumFinEquiv
  simp only [Equiv.coe_fn_mk, Equiv.sigmaCongrLeft, Equiv.coe_fn_symm_mk, Equiv.instTrans_trans,
    Equiv.trans_apply, finCongr_apply, Fin.coe_cast]
  conv  =>
    enter [1,1,3]
    apply Equiv.sumCongr_apply
  by_cases him : iv < m
  · conv in Sigma.mk _ _ =>
      equals ⟨Sum.inl ⟨iv, him⟩, j⟩ => simp [Fin.addCases, him]
    simpa using ih _
  · replace him := Nat.eq_of_lt_succ_of_not_lt hi him
    subst him
    conv in Sigma.mk _ _ =>
      equals ⟨Sum.inr 0, j⟩ => simp [Fin.addCases, Fin.natAdd]
    simp
    rfl

Explicit Formula for $\mathrm{finSigmaFinEquiv}$ on Dependent Pairs

Informal description

For any natural number $m$ and any family of natural numbers $n : \mathrm{Fin}(m) \to \mathbb{N}$, the equivalence $\mathrm{finSigmaFinEquiv}$ maps a pair $(i, j) \in \Sigma_{i \in \mathrm{Fin}(m)} \mathrm{Fin}(n i)$ to the natural number $\sum_{i' \in \mathrm{Fin}(i)} n(i') + j$, where $i'$ ranges over the elements of $\mathrm{Fin}(i)$ via the cast $\mathrm{Fin.castLE}$ induced by the inequality $i < m$.

finSigmaFinEquiv_one theorem

{n : Fin 1 → ℕ} (ij : (i : Fin 1) × Fin (n i)) : (finSigmaFinEquiv ij : ℕ) = ij.2

Full source

/-- `finSigmaFinEquiv` on `Fin 1 × f` is just `f` -/
theorem finSigmaFinEquiv_one {n : Fin 1 → ℕ} (ij : (i : Fin 1) × Fin (n i)) :
    (finSigmaFinEquiv ij : ℕ) = ij.2 := by
  rw [finSigmaFinEquiv_apply, add_eq_right]
  apply @Finset.sum_of_isEmpty _ _ _ _ (by simpa using Fin.isEmpty')

Simplification of $\mathrm{finSigmaFinEquiv}$ for $\mathrm{Fin}(1)$

Informal description

For any family of natural numbers $n : \mathrm{Fin}(1) \to \mathbb{N}$ and any pair $(i, j) \in \Sigma_{i \in \mathrm{Fin}(1)} \mathrm{Fin}(n i)$, the equivalence $\mathrm{finSigmaFinEquiv}$ maps $(i, j)$ to the natural number $j$. In other words, $\mathrm{finSigmaFinEquiv}(i, j) = j$.

List.prod_take_ofFn theorem

{n : ℕ} (f : Fin n → α) (i : ℕ) : ((ofFn f).take i).prod = ∏ j with j.val < i, f j

Full source

@[to_additive]
theorem prod_take_ofFn {n : ℕ} (f : Fin n → α) (i : ℕ) :
    ((ofFn f).take i).prod = ∏ j with j.val < i, f j := by
  induction i with
  | zero =>
    simp
  | succ i IH =>
    by_cases h : i < n
    · have : i < length (ofFn f) := by rwa [length_ofFn]
      rw [prod_take_succ _ _ this]
      have A : ({j | j.val < i + 1} : Finset (Fin n)) =
          insert ⟨i, h⟩ ({j | Fin.val j < i} : Finset (Fin n)) := by
        ext ⟨_, _⟩
        simp [Nat.lt_succ_iff_lt_or_eq, or_comm]
      rw [A, prod_insert (by simp), IH, mul_comm]
      simp
    · have A : (ofFn f).take i = (ofFn f).take i.succ := by
        rw [← length_ofFn (f := f)] at h
        have : length (ofFn f) ≤ i := not_lt.mp h
        rw [take_of_length_le this, take_of_length_le (le_trans this (Nat.le_succ _))]
      have B : ∀ j : Fin n, ((j : ℕ) < i.succ) = ((j : ℕ) < i) := by
        intro j
        have : (j : ℕ) < i := lt_of_lt_of_le j.2 (not_lt.mp h)
        simp [this, lt_trans this (Nat.lt_succ_self _)]
      simp [← A, B, IH]

Product of Initial Segment Equals Finite Product over $\mathrm{Fin}(n)$ with $j < i$

Informal description

For any commutative monoid $\alpha$, natural number $n$, function $f \colon \mathrm{Fin}(n) \to \alpha$, and natural number $i$, the product of the first $i$ elements in the list obtained from $f$ equals the product of $f$ over all elements $j \in \mathrm{Fin}(n)$ with $j < i$. In symbols: $\prod_{a \in \mathrm{List.ofFn}\, f \text{.take } i} a = \prod_{\substack{j \in \mathrm{Fin}(n) \\ j < i}} f(j)$.

List.prod_ofFn theorem

{n : ℕ} {f : Fin n → α} : (ofFn f).prod = ∏ i, f i

Full source

@[to_additive]
theorem prod_ofFn {n : ℕ} {f : Fin n → α} : (ofFn f).prod = ∏ i, f i :=
  Fin.prod_ofFn f

Equality of List Product and Finite Product over $\mathrm{Fin}(n)$

Informal description

For any commutative monoid $\alpha$ and any function $f \colon \mathrm{Fin}(n) \to \alpha$, the product of the elements in the list obtained by applying $f$ to all elements of $\mathrm{Fin}(n)$ is equal to the product of $f$ over all elements of $\mathrm{Fin}(n)$. In symbols: $\prod (a \in \mathrm{List.ofFn}\, f) \, a = \prod_{i \in \mathrm{Fin}(n)} f(i)$.

List.alternatingProd_eq_finset_prod theorem

 {G : Type*} [DivisionCommMonoid G] : ∀ (L : List G), alternatingProd L = ∏ i : Fin L.length, L[i] ^ (-1 : ℤ) ^ (i : ℕ)

Full source

@[to_additive]
theorem alternatingProd_eq_finset_prod {G : Type*} [DivisionCommMonoid G] :
    ∀ (L : List G), alternatingProd L = ∏ i : Fin L.length, L[i] ^ (-1 : ℤ) ^ (i : ℕ)
  | [] => by
    rw [alternatingProd, Finset.prod_eq_one]
    rintro ⟨i, ⟨⟩⟩
  | g::[] => by
    show g = ∏ i : Fin 1, [g][i] ^ (-1 : ℤ) ^ (i : ℕ)
    rw [Fin.prod_univ_succ]; simp
  | g::h::L =>
    calc g * h⁻¹ * L.alternatingProd
      = g * h⁻¹ * ∏ i : Fin L.length, L[i] ^ (-1 : ℤ) ^ (i : ℕ) :=
        congr_arg _ (alternatingProd_eq_finset_prod _)
    _ = ∏ i : Fin (L.length + 2), (g::h::L)[i] ^ (-1 : ℤ) ^ (i : ℕ) := by
        { rw [Fin.prod_univ_succ, Fin.prod_univ_succ, mul_assoc]
          simp [pow_add]}

Alternating Product as Signed Power Product in Commutative Division Monoids

Informal description

Let $G$ be a commutative division monoid. For any list $L$ of elements in $G$, the alternating product of $L$ equals the product over all indices $i$ in $\mathrm{Fin}(|L|)$ of $L[i]$ raised to the power $(-1)^i$. In symbols: \[ \text{alternatingProd}(L) = \prod_{i \in \mathrm{Fin}(|L|)} L[i]^{(-1)^i}. \]

Main declarations