Big operators and Fin

Some results about products and sums over the type Fin.

The most important results are the induction formulas Fin.prod_univ_castSucc and Fin.prod_univ_succ, and the formula Fin.prod_const for the product of a constant function. These results have variants for sums instead of products.

Main declarations

• finFunctionFinEquiv: An explicit equivalence between Fin n → Fin m and Fin (m ^ n).

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

theorem Finset.sum_range {M : Type u_2} [AddCommMonoid M] {n : ℕ} (f : ℕ → M) : ∑ i ∈ range n, f i = ∑ i : Fin n, f ↑i

theorem Fin.prod_ofFn {M : Type u_2} [CommMonoid M] {n : ℕ} (f : Fin n → M) : (List.ofFn f).prod = ∏ i : Fin n, f i

theorem Fin.sum_ofFn {M : Type u_2} [AddCommMonoid M] {n : ℕ} (f : Fin n → M) : (List.ofFn f).sum = ∑ i : Fin n, f i

theorem Fin.prod_univ_def {M : Type u_2} [CommMonoid M] {n : ℕ} (f : Fin n → M) : ∏ i : Fin n, f i = (List.map f (List.finRange n)).prod

theorem Fin.sum_univ_def {M : Type u_2} [AddCommMonoid M] {n : ℕ} (f : Fin n → M) : ∑ i : Fin n, f i = (List.map f (List.finRange n)).sum

theorem Fin.prod_univ_zero {M : Type u_2} [CommMonoid M] (f : Fin 0 → M) : ∏ i : Fin 0, f i = 1

A product of a function f : Fin 0 → M is 1 because Fin 0 is empty

theorem Fin.sum_univ_zero {M : Type u_2} [AddCommMonoid M] (f : Fin 0 → M) : ∑ i : Fin 0, f i = 0

A sum of a function f : Fin 0 → M is 0 because Fin 0 is empty

theorem Fin.prod_univ_succAbove {M : Type u_2} [CommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (x : Fin (n + 1)) : ∏ i : Fin (n + 1), f i = f x * ∏ i : Fin n, f (x.succAbove i)

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

theorem Fin.sum_univ_succAbove {M : Type u_2} [AddCommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (x : Fin (n + 1)) : ∑ i : Fin (n + 1), f i = f x + ∑ i : Fin n, f (x.succAbove i)

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 Fin.prod_univ_succ {M : Type u_2} [CommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) : ∏ i : Fin (n + 1), f i = f 0 * ∏ i : Fin n, f i.succ

A product of a function f : Fin (n + 1) → M over all Fin (n + 1) is the product of f 0 times the remaining product

theorem Fin.sum_univ_succ {M : Type u_2} [AddCommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) : ∑ i : Fin (n + 1), f i = f 0 + ∑ i : Fin n, f i.succ

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 Fin.prod_univ_castSucc {M : Type u_2} [CommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) : ∏ i : Fin (n + 1), f i = (∏ i : Fin n, f i.castSucc) * f (last n)

A product of a function f : Fin (n + 1) → M over all Fin (n + 1) is the product of f (Fin.last n) times the remaining product

theorem Fin.sum_univ_castSucc {M : Type u_2} [AddCommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) : ∑ i : Fin (n + 1), f i = ∑ i : Fin n, f i.castSucc + f (last n)

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

@[simp]

theorem Fin.prod_univ_getElem {M : Type u_2} [CommMonoid M] (l : List M) : ∏ i : Fin l.length, l[↑i] = l.prod

@[simp]

theorem Fin.sum_univ_getElem {M : Type u_2} [AddCommMonoid M] (l : List M) : ∑ i : Fin l.length, l[↑i] = l.sum

@[simp]

theorem Fin.prod_univ_fun_getElem {ι : Type u_1} {M : Type u_2} [CommMonoid M] (l : List ι) (f : ι → M) : ∏ i : Fin l.length, f l[↑i] = (List.map f l).prod

@[simp]

theorem Fin.sum_univ_fun_getElem {ι : Type u_1} {M : Type u_2} [AddCommMonoid M] (l : List ι) (f : ι → M) : ∑ i : Fin l.length, f l[↑i] = (List.map f l).sum

@[simp]

theorem Fin.prod_cons {M : Type u_2} [CommMonoid M] {n : ℕ} (x : M) (f : Fin n → M) : ∏ i : Fin n.succ, cons x f i = x * ∏ i : Fin n, f i

@[simp]

theorem Fin.sum_cons {M : Type u_2} [AddCommMonoid M] {n : ℕ} (x : M) (f : Fin n → M) : ∑ i : Fin n.succ, cons x f i = x + ∑ i : Fin n, f i

@[simp]

theorem Fin.prod_snoc {M : Type u_2} [CommMonoid M] {n : ℕ} (x : M) (f : Fin n → M) : ∏ i : Fin n.succ, snoc f x i = (∏ i : Fin n, f i) * x

@[simp]

theorem Fin.sum_snoc {M : Type u_2} [AddCommMonoid M] {n : ℕ} (x : M) (f : Fin n → M) : ∑ i : Fin n.succ, snoc f x i = ∑ i : Fin n, f i + x

theorem Fin.prod_univ_one {M : Type u_2} [CommMonoid M] (f : Fin 1 → M) : ∏ i : Fin 1, f i = f 0

theorem Fin.sum_univ_one {M : Type u_2} [AddCommMonoid M] (f : Fin 1 → M) : ∑ i : Fin 1, f i = f 0

@[simp]

theorem Fin.prod_univ_two {M : Type u_2} [CommMonoid M] (f : Fin 2 → M) : ∏ i : Fin 2, f i = f 0 * f 1

@[simp]

theorem Fin.sum_univ_two {M : Type u_2} [AddCommMonoid M] (f : Fin 2 → M) : ∑ i : Fin 2, f i = f 0 + f 1

theorem Fin.prod_univ_two' {ι : Type u_1} {M : Type u_2} [CommMonoid M] (f : ι → M) (a b : ι) : ∏ i : Fin (Nat.succ 0).succ, f (![a, b] i) = f a * f b

theorem Fin.sum_univ_two' {ι : Type u_1} {M : Type u_2} [AddCommMonoid M] (f : ι → M) (a b : ι) : ∑ i : Fin (Nat.succ 0).succ, f (![a, b] i) = f a + f b

theorem Fin.prod_univ_three {M : Type u_2} [CommMonoid M] (f : Fin 3 → M) : ∏ i : Fin 3, f i = f 0 * f 1 * f 2

theorem Fin.sum_univ_three {M : Type u_2} [AddCommMonoid M] (f : Fin 3 → M) : ∑ i : Fin 3, f i = f 0 + f 1 + f 2

theorem Fin.prod_univ_four {M : Type u_2} [CommMonoid M] (f : Fin 4 → M) : ∏ i : Fin 4, f i = f 0 * f 1 * f 2 * f 3

theorem Fin.sum_univ_four {M : Type u_2} [AddCommMonoid M] (f : Fin 4 → M) : ∑ i : Fin 4, f i = f 0 + f 1 + f 2 + f 3

theorem Fin.prod_univ_five {M : Type u_2} [CommMonoid M] (f : Fin 5 → M) : ∏ i : Fin 5, f i = f 0 * f 1 * f 2 * f 3 * f 4

theorem Fin.sum_univ_five {M : Type u_2} [AddCommMonoid M] (f : Fin 5 → M) : ∑ i : Fin 5, f i = f 0 + f 1 + f 2 + f 3 + f 4

theorem Fin.prod_univ_six {M : Type u_2} [CommMonoid M] (f : Fin 6 → M) : ∏ i : Fin 6, f i = f 0 * f 1 * f 2 * f 3 * f 4 * f 5

theorem Fin.sum_univ_six {M : Type u_2} [AddCommMonoid M] (f : Fin 6 → M) : ∑ i : Fin 6, f i = f 0 + f 1 + f 2 + f 3 + f 4 + f 5

theorem Fin.prod_univ_seven {M : Type u_2} [CommMonoid M] (f : Fin 7 → M) : ∏ i : Fin 7, f i = f 0 * f 1 * f 2 * f 3 * f 4 * f 5 * f 6

theorem Fin.sum_univ_seven {M : Type u_2} [AddCommMonoid M] (f : Fin 7 → M) : ∑ i : Fin 7, f i = f 0 + f 1 + f 2 + f 3 + f 4 + f 5 + f 6

theorem Fin.prod_univ_eight {M : Type u_2} [CommMonoid M] (f : Fin 8 → M) : ∏ i : Fin 8, f i = f 0 * f 1 * f 2 * f 3 * f 4 * f 5 * f 6 * f 7

theorem Fin.sum_univ_eight {M : Type u_2} [AddCommMonoid M] (f : Fin 8 → M) : ∑ i : Fin 8, f i = f 0 + f 1 + f 2 + f 3 + f 4 + f 5 + f 6 + f 7

theorem Fin.prod_const {M : Type u_2} [CommMonoid M] (n : ℕ) (x : M) : ∏ _i : Fin n, x = x ^ n

theorem Fin.sum_const {M : Type u_2} [AddCommMonoid M] (n : ℕ) (x : M) : ∑ _i : Fin n, x = n • x

theorem Fin.prod_congr' {M : Type u_2} [CommMonoid M] {a b : ℕ} (f : Fin b → M) (h : a = b) : ∏ i : Fin a, f (Fin.cast h i) = ∏ i : Fin b, f i

theorem Fin.sum_congr' {M : Type u_2} [AddCommMonoid M] {a b : ℕ} (f : Fin b → M) (h : a = b) : ∑ i : Fin a, f (Fin.cast h i) = ∑ i : Fin b, f i

theorem Fin.prod_univ_add {M : Type u_2} [CommMonoid M] {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)

theorem Fin.sum_univ_add {M : Type u_2} [AddCommMonoid M] {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)

theorem Fin.prod_trunc {M : Type u_2} [CommMonoid M] {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)

theorem Fin.sum_trunc {M : Type u_2} [AddCommMonoid M] {a b : ℕ} (f : Fin (a + b) → M) (hf : ∀ (j : Fin b), f (natAdd a j) = 0) : ∑ i : Fin (a + b), f i = ∑ i : Fin a, f (castAdd b i)

@[simp]

theorem Fin.prod_insertNth {M : Type u_2} [CommMonoid M] {n : ℕ} (i : Fin (n + 1)) (x : M) (p : Fin n → M) : ∏ j : Fin (n + 1), i.insertNth x p j = x * ∏ j : Fin n, p j

@[simp]

theorem Fin.sum_insertNth {M : Type u_2} [AddCommMonoid M] {n : ℕ} (i : Fin (n + 1)) (x : M) (p : Fin n → M) : ∑ j : Fin (n + 1), i.insertNth x p j = x + ∑ j : Fin n, p j

@[simp]

theorem Fin.mul_prod_removeNth {M : Type u_2} [CommMonoid M] {n : ℕ} (i : Fin (n + 1)) (f : Fin (n + 1) → M) : f i * ∏ j : Fin n, i.removeNth f j = ∏ j : Fin (n + 1), f j

@[simp]

theorem Fin.add_sum_removeNth {M : Type u_2} [AddCommMonoid M] {n : ℕ} (i : Fin (n + 1)) (f : Fin (n + 1) → M) : f i + ∑ j : Fin n, i.removeNth f j = ∑ j : Fin (n + 1), f j

Products over intervals: Fin.cast

theorem Fin.prod_Icc_cast {M : Type u_2} [CommMonoid M] {n m : ℕ} (h : n = m) (f : Fin m → M) (a b : Fin n) : ∏ i ∈ Finset.Icc (Fin.cast h a) (Fin.cast h b), f i = ∏ i ∈ Finset.Icc a b, f (Fin.cast h i)

theorem Fin.sum_Icc_cast {M : Type u_2} [AddCommMonoid M] {n m : ℕ} (h : n = m) (f : Fin m → M) (a b : Fin n) : ∑ i ∈ Finset.Icc (Fin.cast h a) (Fin.cast h b), f i = ∑ i ∈ Finset.Icc a b, f (Fin.cast h i)

theorem Fin.prod_Ico_cast {M : Type u_2} [CommMonoid M] {n m : ℕ} (h : n = m) (f : Fin m → M) (a b : Fin n) : ∏ i ∈ Finset.Ico (Fin.cast h a) (Fin.cast h b), f i = ∏ i ∈ Finset.Ico a b, f (Fin.cast h i)

theorem Fin.sum_Ico_cast {M : Type u_2} [AddCommMonoid M] {n m : ℕ} (h : n = m) (f : Fin m → M) (a b : Fin n) : ∑ i ∈ Finset.Ico (Fin.cast h a) (Fin.cast h b), f i = ∑ i ∈ Finset.Ico a b, f (Fin.cast h i)

theorem Fin.prod_Ioc_cast {M : Type u_2} [CommMonoid M] {n m : ℕ} (h : n = m) (f : Fin m → M) (a b : Fin n) : ∏ i ∈ Finset.Ioc (Fin.cast h a) (Fin.cast h b), f i = ∏ i ∈ Finset.Ioc a b, f (Fin.cast h i)

theorem Fin.sum_Ioc_cast {M : Type u_2} [AddCommMonoid M] {n m : ℕ} (h : n = m) (f : Fin m → M) (a b : Fin n) : ∑ i ∈ Finset.Ioc (Fin.cast h a) (Fin.cast h b), f i = ∑ i ∈ Finset.Ioc a b, f (Fin.cast h i)

theorem Fin.prod_Ioo_cast {M : Type u_2} [CommMonoid M] {n m : ℕ} (h : n = m) (f : Fin m → M) (a b : Fin n) : ∏ i ∈ Finset.Ioo (Fin.cast h a) (Fin.cast h b), f i = ∏ i ∈ Finset.Ioo a b, f (Fin.cast h i)

theorem Fin.sum_Ioo_cast {M : Type u_2} [AddCommMonoid M] {n m : ℕ} (h : n = m) (f : Fin m → M) (a b : Fin n) : ∑ i ∈ Finset.Ioo (Fin.cast h a) (Fin.cast h b), f i = ∑ i ∈ Finset.Ioo a b, f (Fin.cast h i)

theorem Fin.prod_uIcc_cast {M : Type u_2} [CommMonoid M] {n m : ℕ} (h : n = m) (f : Fin m → M) (a b : Fin n) : ∏ i ∈ Finset.uIcc (Fin.cast h a) (Fin.cast h b), f i = ∏ i ∈ Finset.uIcc a b, f (Fin.cast h i)

theorem Fin.sum_uIcc_cast {M : Type u_2} [AddCommMonoid M] {n m : ℕ} (h : n = m) (f : Fin m → M) (a b : Fin n) : ∑ i ∈ Finset.uIcc (Fin.cast h a) (Fin.cast h b), f i = ∑ i ∈ Finset.uIcc a b, f (Fin.cast h i)

theorem Fin.prod_Ici_cast {M : Type u_2} [CommMonoid M] {n m : ℕ} (h : n = m) (f : Fin m → M) (a : Fin n) : ∏ i ∈ Finset.Ici (Fin.cast h a), f i = ∏ i ∈ Finset.Ici a, f (Fin.cast h i)

theorem Fin.sum_Ici_cast {M : Type u_2} [AddCommMonoid M] {n m : ℕ} (h : n = m) (f : Fin m → M) (a : Fin n) : ∑ i ∈ Finset.Ici (Fin.cast h a), f i = ∑ i ∈ Finset.Ici a, f (Fin.cast h i)

theorem Fin.prod_Ioi_cast {M : Type u_2} [CommMonoid M] {n m : ℕ} (h : n = m) (f : Fin m → M) (a : Fin n) : ∏ i ∈ Finset.Ioi (Fin.cast h a), f i = ∏ i ∈ Finset.Ioi a, f (Fin.cast h i)

theorem Fin.sum_Ioi_cast {M : Type u_2} [AddCommMonoid M] {n m : ℕ} (h : n = m) (f : Fin m → M) (a : Fin n) : ∑ i ∈ Finset.Ioi (Fin.cast h a), f i = ∑ i ∈ Finset.Ioi a, f (Fin.cast h i)

theorem Fin.prod_Iic_cast {M : Type u_2} [CommMonoid M] {n m : ℕ} (h : n = m) (f : Fin m → M) (a : Fin n) : ∏ i ∈ Finset.Iic (Fin.cast h a), f i = ∏ i ∈ Finset.Iic a, f (Fin.cast h i)

theorem Fin.sum_Iic_cast {M : Type u_2} [AddCommMonoid M] {n m : ℕ} (h : n = m) (f : Fin m → M) (a : Fin n) : ∑ i ∈ Finset.Iic (Fin.cast h a), f i = ∑ i ∈ Finset.Iic a, f (Fin.cast h i)

theorem Fin.prod_Iio_cast {M : Type u_2} [CommMonoid M] {n m : ℕ} (h : n = m) (f : Fin m → M) (a : Fin n) : ∏ i ∈ Finset.Iio (Fin.cast h a), f i = ∏ i ∈ Finset.Iio a, f (Fin.cast h i)

theorem Fin.sum_Iio_cast {M : Type u_2} [AddCommMonoid M] {n m : ℕ} (h : n = m) (f : Fin m → M) (a : Fin n) : ∑ i ∈ Finset.Iio (Fin.cast h a), f i = ∑ i ∈ Finset.Iio a, f (Fin.cast h i)

Products over intervals: Fin.castLE

theorem Fin.prod_Icc_castLE {M : Type u_2} [CommMonoid M] {n m : ℕ} (h : n ≤ m) (f : Fin m → M) (a b : Fin n) : ∏ i ∈ Finset.Icc (castLE h a) (castLE h b), f i = ∏ i ∈ Finset.Icc a b, f (castLE h i)

theorem Fin.sum_Icc_castLE {M : Type u_2} [AddCommMonoid M] {n m : ℕ} (h : n ≤ m) (f : Fin m → M) (a b : Fin n) : ∑ i ∈ Finset.Icc (castLE h a) (castLE h b), f i = ∑ i ∈ Finset.Icc a b, f (castLE h i)

theorem Fin.prod_Ico_castLE {M : Type u_2} [CommMonoid M] {n m : ℕ} (h : n ≤ m) (f : Fin m → M) (a b : Fin n) : ∏ i ∈ Finset.Ico (castLE h a) (castLE h b), f i = ∏ i ∈ Finset.Ico a b, f (castLE h i)

theorem Fin.sum_Ico_castLE {M : Type u_2} [AddCommMonoid M] {n m : ℕ} (h : n ≤ m) (f : Fin m → M) (a b : Fin n) : ∑ i ∈ Finset.Ico (castLE h a) (castLE h b), f i = ∑ i ∈ Finset.Ico a b, f (castLE h i)

theorem Fin.prod_Ioc_castLE {M : Type u_2} [CommMonoid M] {n m : ℕ} (h : n ≤ m) (f : Fin m → M) (a b : Fin n) : ∏ i ∈ Finset.Ioc (castLE h a) (castLE h b), f i = ∏ i ∈ Finset.Ioc a b, f (castLE h i)

theorem Fin.sum_Ioc_castLE {M : Type u_2} [AddCommMonoid M] {n m : ℕ} (h : n ≤ m) (f : Fin m → M) (a b : Fin n) : ∑ i ∈ Finset.Ioc (castLE h a) (castLE h b), f i = ∑ i ∈ Finset.Ioc a b, f (castLE h i)

theorem Fin.prod_Ioo_castLE {M : Type u_2} [CommMonoid M] {n m : ℕ} (h : n ≤ m) (f : Fin m → M) (a b : Fin n) : ∏ i ∈ Finset.Ioo (castLE h a) (castLE h b), f i = ∏ i ∈ Finset.Ioo a b, f (castLE h i)

theorem Fin.sum_Ioo_castLE {M : Type u_2} [AddCommMonoid M] {n m : ℕ} (h : n ≤ m) (f : Fin m → M) (a b : Fin n) : ∑ i ∈ Finset.Ioo (castLE h a) (castLE h b), f i = ∑ i ∈ Finset.Ioo a b, f (castLE h i)

theorem Fin.prod_uIcc_castLE {M : Type u_2} [CommMonoid M] {n m : ℕ} (h : n ≤ m) (f : Fin m → M) (a b : Fin n) : ∏ i ∈ Finset.uIcc (castLE h a) (castLE h b), f i = ∏ i ∈ Finset.uIcc a b, f (castLE h i)

theorem Fin.sum_uIcc_castLE {M : Type u_2} [AddCommMonoid M] {n m : ℕ} (h : n ≤ m) (f : Fin m → M) (a b : Fin n) : ∑ i ∈ Finset.uIcc (castLE h a) (castLE h b), f i = ∑ i ∈ Finset.uIcc a b, f (castLE h i)

theorem Fin.prod_Iic_castLE {M : Type u_2} [CommMonoid M] {n m : ℕ} (h : n ≤ m) (f : Fin m → M) (a : Fin n) : ∏ i ∈ Finset.Iic (castLE h a), f i = ∏ i ∈ Finset.Iic a, f (castLE h i)

theorem Fin.sum_Iic_castLE {M : Type u_2} [AddCommMonoid M] {n m : ℕ} (h : n ≤ m) (f : Fin m → M) (a : Fin n) : ∑ i ∈ Finset.Iic (castLE h a), f i = ∑ i ∈ Finset.Iic a, f (castLE h i)

theorem Fin.prod_Iio_castLE {M : Type u_2} [CommMonoid M] {n m : ℕ} (h : n ≤ m) (f : Fin m → M) (a : Fin n) : ∏ i ∈ Finset.Iio (castLE h a), f i = ∏ i ∈ Finset.Iio a, f (castLE h i)

theorem Fin.sum_Iio_castLE {M : Type u_2} [AddCommMonoid M] {n m : ℕ} (h : n ≤ m) (f : Fin m → M) (a : Fin n) : ∑ i ∈ Finset.Iio (castLE h a), f i = ∑ i ∈ Finset.Iio a, f (castLE h i)

Products over intervals: Fin.castAdd

theorem Fin.prod_Icc_castAdd {M : Type u_2} [CommMonoid M] {n : ℕ} (m : ℕ) (f : Fin (n + m) → M) (a b : Fin n) : ∏ i ∈ Finset.Icc (castAdd m a) (castAdd m b), f i = ∏ i ∈ Finset.Icc a b, f (castAdd m i)

theorem Fin.sum_Icc_castAdd {M : Type u_2} [AddCommMonoid M] {n : ℕ} (m : ℕ) (f : Fin (n + m) → M) (a b : Fin n) : ∑ i ∈ Finset.Icc (castAdd m a) (castAdd m b), f i = ∑ i ∈ Finset.Icc a b, f (castAdd m i)

theorem Fin.prod_Ico_castAdd {M : Type u_2} [CommMonoid M] {n : ℕ} (m : ℕ) (f : Fin (n + m) → M) (a b : Fin n) : ∏ i ∈ Finset.Ico (castAdd m a) (castAdd m b), f i = ∏ i ∈ Finset.Ico a b, f (castAdd m i)

theorem Fin.sum_Ico_castAdd {M : Type u_2} [AddCommMonoid M] {n : ℕ} (m : ℕ) (f : Fin (n + m) → M) (a b : Fin n) : ∑ i ∈ Finset.Ico (castAdd m a) (castAdd m b), f i = ∑ i ∈ Finset.Ico a b, f (castAdd m i)

theorem Fin.prod_Ioc_castAdd {M : Type u_2} [CommMonoid M] {n : ℕ} (m : ℕ) (f : Fin (n + m) → M) (a b : Fin n) : ∏ i ∈ Finset.Ioc (castAdd m a) (castAdd m b), f i = ∏ i ∈ Finset.Ioc a b, f (castAdd m i)

theorem Fin.sum_Ioc_castAdd {M : Type u_2} [AddCommMonoid M] {n : ℕ} (m : ℕ) (f : Fin (n + m) → M) (a b : Fin n) : ∑ i ∈ Finset.Ioc (castAdd m a) (castAdd m b), f i = ∑ i ∈ Finset.Ioc a b, f (castAdd m i)

theorem Fin.prod_Ioo_castAdd {M : Type u_2} [CommMonoid M] {n : ℕ} (m : ℕ) (f : Fin (n + m) → M) (a b : Fin n) : ∏ i ∈ Finset.Ioo (castAdd m a) (castAdd m b), f i = ∏ i ∈ Finset.Ioo a b, f (castAdd m i)

theorem Fin.sum_Ioo_castAdd {M : Type u_2} [AddCommMonoid M] {n : ℕ} (m : ℕ) (f : Fin (n + m) → M) (a b : Fin n) : ∑ i ∈ Finset.Ioo (castAdd m a) (castAdd m b), f i = ∑ i ∈ Finset.Ioo a b, f (castAdd m i)

theorem Fin.prod_uIcc_castAdd {M : Type u_2} [CommMonoid M] {n : ℕ} (m : ℕ) (f : Fin (n + m) → M) (a b : Fin n) : ∏ i ∈ Finset.uIcc (castAdd m a) (castAdd m b), f i = ∏ i ∈ Finset.uIcc a b, f (castAdd m i)

theorem Fin.sum_uIcc_castAdd {M : Type u_2} [AddCommMonoid M] {n : ℕ} (m : ℕ) (f : Fin (n + m) → M) (a b : Fin n) : ∑ i ∈ Finset.uIcc (castAdd m a) (castAdd m b), f i = ∑ i ∈ Finset.uIcc a b, f (castAdd m i)

theorem Fin.prod_Iic_castAdd {M : Type u_2} [CommMonoid M] {n : ℕ} (m : ℕ) (f : Fin (n + m) → M) (a : Fin n) : ∏ i ∈ Finset.Iic (castAdd m a), f i = ∏ i ∈ Finset.Iic a, f (castAdd m i)

theorem Fin.sum_Iic_castAdd {M : Type u_2} [AddCommMonoid M] {n : ℕ} (m : ℕ) (f : Fin (n + m) → M) (a : Fin n) : ∑ i ∈ Finset.Iic (castAdd m a), f i = ∑ i ∈ Finset.Iic a, f (castAdd m i)

theorem Fin.prod_Iio_castAdd {M : Type u_2} [CommMonoid M] {n : ℕ} (m : ℕ) (f : Fin (n + m) → M) (a : Fin n) : ∏ i ∈ Finset.Iio (castAdd m a), f i = ∏ i ∈ Finset.Iio a, f (castAdd m i)

theorem Fin.sum_Iio_castAdd {M : Type u_2} [AddCommMonoid M] {n : ℕ} (m : ℕ) (f : Fin (n + m) → M) (a : Fin n) : ∑ i ∈ Finset.Iio (castAdd m a), f i = ∑ i ∈ Finset.Iio a, f (castAdd m i)

Products over intervals: Fin.castSucc

theorem Fin.prod_Icc_castSucc {M : Type u_2} [CommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (a b : Fin n) : ∏ i ∈ Finset.Icc a.castSucc b.castSucc, f i = ∏ i ∈ Finset.Icc a b, f i.castSucc

theorem Fin.sum_Icc_castSucc {M : Type u_2} [AddCommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (a b : Fin n) : ∑ i ∈ Finset.Icc a.castSucc b.castSucc, f i = ∑ i ∈ Finset.Icc a b, f i.castSucc

theorem Fin.prod_Ico_castSucc {M : Type u_2} [CommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (a b : Fin n) : ∏ i ∈ Finset.Ico a.castSucc b.castSucc, f i = ∏ i ∈ Finset.Ico a b, f i.castSucc

theorem Fin.sum_Ico_castSucc {M : Type u_2} [AddCommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (a b : Fin n) : ∑ i ∈ Finset.Ico a.castSucc b.castSucc, f i = ∑ i ∈ Finset.Ico a b, f i.castSucc

theorem Fin.prod_Ioc_castSucc {M : Type u_2} [CommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (a b : Fin n) : ∏ i ∈ Finset.Ioc a.castSucc b.castSucc, f i = ∏ i ∈ Finset.Ioc a b, f i.castSucc

theorem Fin.sum_Ioc_castSucc {M : Type u_2} [AddCommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (a b : Fin n) : ∑ i ∈ Finset.Ioc a.castSucc b.castSucc, f i = ∑ i ∈ Finset.Ioc a b, f i.castSucc

theorem Fin.prod_Ioo_castSucc {M : Type u_2} [CommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (a b : Fin n) : ∏ i ∈ Finset.Ioo a.castSucc b.castSucc, f i = ∏ i ∈ Finset.Ioo a b, f i.castSucc

theorem Fin.sum_Ioo_castSucc {M : Type u_2} [AddCommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (a b : Fin n) : ∑ i ∈ Finset.Ioo a.castSucc b.castSucc, f i = ∑ i ∈ Finset.Ioo a b, f i.castSucc

theorem Fin.prod_uIcc_castSucc {M : Type u_2} [CommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (a b : Fin n) : ∏ i ∈ Finset.uIcc a.castSucc b.castSucc, f i = ∏ i ∈ Finset.uIcc a b, f i.castSucc

theorem Fin.sum_uIcc_castSucc {M : Type u_2} [AddCommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (a b : Fin n) : ∑ i ∈ Finset.uIcc a.castSucc b.castSucc, f i = ∑ i ∈ Finset.uIcc a b, f i.castSucc

theorem Fin.prod_Iic_castSucc {M : Type u_2} [CommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (a : Fin n) : ∏ i ∈ Finset.Iic a.castSucc, f i = ∏ i ∈ Finset.Iic a, f i.castSucc

theorem Fin.sum_Iic_castSucc {M : Type u_2} [AddCommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (a : Fin n) : ∑ i ∈ Finset.Iic a.castSucc, f i = ∑ i ∈ Finset.Iic a, f i.castSucc

theorem Fin.prod_Iio_castSucc {M : Type u_2} [CommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (a : Fin n) : ∏ i ∈ Finset.Iio a.castSucc, f i = ∏ i ∈ Finset.Iio a, f i.castSucc

theorem Fin.sum_Iio_castSucc {M : Type u_2} [AddCommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (a : Fin n) : ∑ i ∈ Finset.Iio a.castSucc, f i = ∑ i ∈ Finset.Iio a, f i.castSucc

Products over intervals: Fin.succ

theorem Fin.prod_Icc_succ {M : Type u_2} [CommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (a b : Fin n) : ∏ i ∈ Finset.Icc a.succ b.succ, f i = ∏ i ∈ Finset.Icc a b, f i.succ

theorem Fin.sum_Icc_succ {M : Type u_2} [AddCommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (a b : Fin n) : ∑ i ∈ Finset.Icc a.succ b.succ, f i = ∑ i ∈ Finset.Icc a b, f i.succ

theorem Fin.prod_Ico_succ {M : Type u_2} [CommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (a b : Fin n) : ∏ i ∈ Finset.Ico a.succ b.succ, f i = ∏ i ∈ Finset.Ico a b, f i.succ

theorem Fin.sum_Ico_succ {M : Type u_2} [AddCommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (a b : Fin n) : ∑ i ∈ Finset.Ico a.succ b.succ, f i = ∑ i ∈ Finset.Ico a b, f i.succ

theorem Fin.prod_Ioc_succ {M : Type u_2} [CommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (a b : Fin n) : ∏ i ∈ Finset.Ioc a.succ b.succ, f i = ∏ i ∈ Finset.Ioc a b, f i.succ

theorem Fin.sum_Ioc_succ {M : Type u_2} [AddCommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (a b : Fin n) : ∑ i ∈ Finset.Ioc a.succ b.succ, f i = ∑ i ∈ Finset.Ioc a b, f i.succ

theorem Fin.prod_Ioo_succ {M : Type u_2} [CommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (a b : Fin n) : ∏ i ∈ Finset.Ioo a.succ b.succ, f i = ∏ i ∈ Finset.Ioo a b, f i.succ

theorem Fin.sum_Ioo_succ {M : Type u_2} [AddCommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (a b : Fin n) : ∑ i ∈ Finset.Ioo a.succ b.succ, f i = ∑ i ∈ Finset.Ioo a b, f i.succ

theorem Fin.prod_uIcc_succ {M : Type u_2} [CommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (a b : Fin n) : ∏ i ∈ Finset.uIcc a.succ b.succ, f i = ∏ i ∈ Finset.uIcc a b, f i.succ

theorem Fin.sum_uIcc_succ {M : Type u_2} [AddCommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (a b : Fin n) : ∑ i ∈ Finset.uIcc a.succ b.succ, f i = ∑ i ∈ Finset.uIcc a b, f i.succ

theorem Fin.prod_Ici_succ {M : Type u_2} [CommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (a : Fin n) : ∏ i ∈ Finset.Ici a.succ, f i = ∏ i ∈ Finset.Ici a, f i.succ

theorem Fin.sum_Ici_succ {M : Type u_2} [AddCommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (a : Fin n) : ∑ i ∈ Finset.Ici a.succ, f i = ∑ i ∈ Finset.Ici a, f i.succ

@[simp]

theorem Fin.prod_Ioi_succ {M : Type u_2} [CommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (a : Fin n) : ∏ i ∈ Finset.Ioi a.succ, f i = ∏ i ∈ Finset.Ioi a, f i.succ

@[simp]

theorem Fin.sum_Ioi_succ {M : Type u_2} [AddCommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (a : Fin n) : ∑ i ∈ Finset.Ioi a.succ, f i = ∑ i ∈ Finset.Ioi a, f i.succ

theorem Fin.prod_Ioi_zero {M : Type u_2} [CommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) : ∏ i ∈ Finset.Ioi 0, f i = ∏ j : Fin n, f j.succ

theorem Fin.sum_Ioi_zero {M : Type u_2} [AddCommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) : ∑ i ∈ Finset.Ioi 0, f i = ∑ j : Fin n, f j.succ

theorem Fin.prod_prod_eq_prod_triangle_mul {M : Type u_2} [CommMonoid M] {n : ℕ} (f : Fin (n + 1) → Fin n → M) : ∏ i : Fin (n + 1), ∏ j : Fin n, f i j = ∏ i : Fin n, ∏ j ∈ Finset.Ici i, f i.castSucc j * f j.succ i

The product of g i j over i j : Fin (n + 1), i ≠ j, is equal to the product of g i j * g j i over i < j.

The additive version of this lemma is useful for some proofs about differential forms. In this application, the function has the signature f : Fin (n + 1) → Fin n → M, where f i j means g i (Fin.succAbove i j) in the informal statements.

Similarly, the product of g i j * g j i over i < j is written as f (Fin.castSucc i) j * f (Fin.succ j) i over i j : Fin n, j ≥ i.

theorem Fin.sum_sum_eq_sum_triangle_add {M : Type u_2} [AddCommMonoid M] {n : ℕ} (f : Fin (n + 1) → Fin n → M) : ∑ i : Fin (n + 1), ∑ j : Fin n, f i j = ∑ i : Fin n, ∑ j ∈ Finset.Ici i, (f i.castSucc j + f j.succ i)

The sum of g i j over i j : Fin (n + 1), i ≠ j, is equal to the sum of g i j + g j i over i < j.

This lemma is useful for some proofs about differential forms. In this application, the function has the signature f : Fin (n + 1) → Fin n → M, where f i j means g i (Fin.succAbove i j) in the informal statements.

Similarly, the sum of g i j + g j i over i < j is written as f (Fin.castSucc i) j + f (Fin.succ j) i over i j : Fin n, j ≥ i.

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

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

def Fin.partialProd {M : Type u_2} [Monoid M] {n : ℕ} (f : Fin n → M) (i : Fin (n + 1)) : M

For f = (a₁, ..., aₙ) in αⁿ, partialProd f is (1, a₁, a₁a₂, ..., a₁...aₙ) in αⁿ⁺¹.

def Fin.partialSum {M : Type u_2} [AddMonoid M] {n : ℕ} (f : Fin n → M) (i : Fin (n + 1)) : M

For f = (a₁, ..., aₙ) in αⁿ, partialSum f is (0, a₁, a₁ + a₂, ..., a₁ + ... + aₙ) in αⁿ⁺¹.

@[simp]

theorem Fin.partialProd_zero {M : Type u_2} [Monoid M] {n : ℕ} (f : Fin n → M) : partialProd f 0 = 1

@[simp]

theorem Fin.partialSum_zero {M : Type u_2} [AddMonoid M] {n : ℕ} (f : Fin n → M) : partialSum f 0 = 0

theorem Fin.partialProd_succ {M : Type u_2} [Monoid M] {n : ℕ} (f : Fin n → M) (j : Fin n) : partialProd f j.succ = partialProd f j.castSucc * f j

theorem Fin.partialSum_succ {M : Type u_2} [AddMonoid M] {n : ℕ} (f : Fin n → M) (j : Fin n) : partialSum f j.succ = partialSum f j.castSucc + f j

theorem Fin.partialProd_succ' {M : Type u_2} [Monoid M] {n : ℕ} (f : Fin (n + 1) → M) (j : Fin (n + 1)) : partialProd f j.succ = f 0 * partialProd (tail f) j

theorem Fin.partialSum_succ' {M : Type u_2} [AddMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (j : Fin (n + 1)) : partialSum f j.succ = f 0 + partialSum (tail f) j

theorem Fin.partialProd_init {M : Type u_2} [Monoid M] {n : ℕ} {f : Fin (n + 1) → M} (i : Fin (n + 1)) : partialProd (init f) i = partialProd f i.castSucc

theorem Fin.partialSum_init {M : Type u_2} [AddMonoid M] {n : ℕ} {f : Fin (n + 1) → M} (i : Fin (n + 1)) : partialSum (init f) i = partialSum f i.castSucc

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

theorem Fin.partialSum_left_neg {n : ℕ} {G : Type u_3} [AddGroup G] (f : Fin (n + 1) → G) : (f 0 +ᵥ partialSum fun (i : Fin n) => -f i.castSucc + f i.succ) = f

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

theorem Fin.partialSum_right_neg {n : ℕ} {G : Type u_3} [AddGroup G] (f : Fin n → G) (i : Fin n) : -partialSum f i.castSucc + partialSum f i.succ = f i

theorem Fin.partialProd_contractNth {G : Type u_3} [Monoid G] {n : ℕ} (g : Fin (n + 1) → G) (a : Fin (n + 1)) : partialProd (a.contractNth (fun (x1 x2 : G) => x1 * x2) g) = partialProd g ∘ a.succ.succAbove

theorem Fin.partialSum_contractNth {G : Type u_3} [AddMonoid G] {n : ℕ} (g : Fin (n + 1) → G) (a : Fin (n + 1)) : partialSum (a.contractNth (fun (x1 x2 : G) => x1 + x2) g) = partialSum g ∘ a.succ.succAbove

theorem Fin.inv_partialProd_mul_eq_contractNth {n : ℕ} {G : Type u_3} [Group G] (g : Fin (n + 1) → G) (j : Fin (n + 1)) (k : Fin n) : (partialProd g (j.succ.succAbove k.castSucc))⁻¹ * partialProd g (j.succAbove k).succ = j.contractNth (fun (x1 x2 : G) => x1 * x2) g k

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 Fin.neg_partialSum_add_eq_contractNth {n : ℕ} {G : Type u_3} [AddGroup G] (g : Fin (n + 1) → G) (j : Fin (n + 1)) (k : Fin n) : -partialSum g (j.succ.succAbove k.castSucc) + partialSum g (j.succAbove k).succ = j.contractNth (fun (x1 x2 : G) => x1 + x2) g k

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.

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

Equivalence between Fin n → Fin m and Fin (m ^ n).

@[simp]

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

@[simp]

theorem finFunctionFinEquiv_symm_apply_val {m n : ℕ} (a : Fin (m ^ n)) (b : Fin n) : ↑(finFunctionFinEquiv.symm a b) = ↑a / m ^ ↑b % m

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

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

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

Equivalence between ∀ i : Fin m, Fin (n i) and Fin (∏ i : Fin m, n i).

theorem finPiFinEquiv_apply {m : ℕ} {n : Fin m → ℕ} (f : (i : Fin m) → Fin (n i)) : ↑(finPiFinEquiv f) = ∑ i : Fin m, ↑(f i) * ∏ j : Fin ↑i, n (Fin.castLE ⋯ j)

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

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

Equivalence between the Sigma type (i : Fin m) × Fin (n i) and Fin (∑ i : Fin m, n i).

@[simp]

theorem finSigmaFinEquiv_apply {m : ℕ} {n : Fin m → ℕ} (k : (i : Fin m) × Fin (n i)) : ↑(finSigmaFinEquiv k) = ∑ i : Fin ↑k.fst, n (Fin.castLE ⋯ i) + ↑k.snd

theorem finSigmaFinEquiv_one {n : Fin 1 → ℕ} (ij : (i : Fin 1) × Fin (n i)) : ↑(finSigmaFinEquiv ij) = ↑ij.snd

finSigmaFinEquiv on Fin 1 × f is just f

theorem List.prod_take_ofFn {M : Type u_2} [CommMonoid M] {n : ℕ} (f : Fin n → M) (i : ℕ) : (take i (ofFn f)).prod = ∏ j : Fin n with ↑j < i, f j

theorem List.sum_take_ofFn {M : Type u_2} [AddCommMonoid M] {n : ℕ} (f : Fin n → M) (i : ℕ) : (take i (ofFn f)).sum = ∑ j : Fin n with ↑j < i, f j

theorem List.prod_ofFn {M : Type u_2} [CommMonoid M] {n : ℕ} {f : Fin n → M} : (ofFn f).prod = ∏ i : Fin n, f i

theorem List.sum_ofFn {M : Type u_2} [AddCommMonoid M] {n : ℕ} {f : Fin n → M} : (ofFn f).sum = ∑ i : Fin n, f i

theorem List.alternatingProd_eq_finset_prod {G : Type u_3} [DivisionCommMonoid G] (L : List G) : L.alternatingProd = ∏ i : Fin L.length, L[i] ^ (-1) ^ ↑i

theorem List.alternatingSum_eq_finset_sum {G : Type u_3} [SubtractionCommMonoid G] (L : List G) : L.alternatingSum = ∑ i : Fin L.length, (-1) ^ ↑i • L[i]