# Documentation

Mathlib.Algebra.BigOperators.Fin

# 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.sum_range {β : Type u_2} [] {n : } (f : β) :
(Finset.sum () fun i => f i) = Finset.sum Finset.univ fun i => f i
theorem Finset.prod_range {β : Type u_2} [] {n : } (f : β) :
(Finset.prod () fun i => f i) = Finset.prod Finset.univ fun i => f i
theorem Fin.sum_univ_def {β : Type u_2} [] {n : } (f : Fin nβ) :
(Finset.sum Finset.univ fun i => f i) = List.sum ()
theorem Fin.prod_univ_def {β : Type u_2} [] {n : } (f : Fin nβ) :
(Finset.prod Finset.univ fun i => f i) = List.prod ()
theorem Fin.sum_ofFn {β : Type u_2} [] {n : } (f : Fin nβ) :
= Finset.sum Finset.univ fun i => f i
theorem Fin.prod_ofFn {β : Type u_2} [] {n : } (f : Fin nβ) :
= Finset.prod Finset.univ fun i => f i
theorem Fin.sum_univ_zero {β : Type u_2} [] (f : Fin 0β) :
(Finset.sum Finset.univ fun i => f i) = 0

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

theorem Fin.prod_univ_zero {β : Type u_2} [] (f : Fin 0β) :
(Finset.prod Finset.univ fun i => f i) = 1

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

theorem Fin.sum_univ_succAbove {β : Type u_2} [] {n : } (f : Fin (n + 1)β) (x : Fin (n + 1)) :
(Finset.sum Finset.univ fun i => f i) = f x + Finset.sum Finset.univ fun i => f ()

A sum of a function f : Fin (n + 1) → β over all Fin (n + 1) is the sum of f x, for some x : Fin (n + 1) plus the remaining product

theorem Fin.prod_univ_succAbove {β : Type u_2} [] {n : } (f : Fin (n + 1)β) (x : Fin (n + 1)) :
(Finset.prod Finset.univ fun i => f i) = f x * Finset.prod Finset.univ fun i => f ()

A product of a function f : Fin (n + 1) → β 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_succ {β : Type u_2} [] {n : } (f : Fin (n + 1)β) :
(Finset.sum Finset.univ fun i => f i) = f 0 + Finset.sum Finset.univ fun i => f ()

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

theorem Fin.prod_univ_succ {β : Type u_2} [] {n : } (f : Fin (n + 1)β) :
(Finset.prod Finset.univ fun i => f i) = f 0 * Finset.prod Finset.univ fun i => f ()

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

theorem Fin.sum_univ_castSucc {β : Type u_2} [] {n : } (f : Fin (n + 1)β) :
(Finset.sum Finset.univ fun i => f i) = (Finset.sum Finset.univ fun i => f ()) + f ()

A sum of a function f : Fin (n + 1) → β over all Fin (n + 1) is the sum of f (Fin.last n) plus the remaining sum

theorem Fin.prod_univ_castSucc {β : Type u_2} [] {n : } (f : Fin (n + 1)β) :
(Finset.prod Finset.univ fun i => f i) = (Finset.prod Finset.univ fun i => f ()) * f ()

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

theorem Fin.sum_cons {β : Type u_2} [] {n : } (x : β) (f : Fin nβ) :
(Finset.sum Finset.univ fun i => Fin.cons x f i) = x + Finset.sum Finset.univ fun i => f i
theorem Fin.prod_cons {β : Type u_2} [] {n : } (x : β) (f : Fin nβ) :
(Finset.prod Finset.univ fun i => Fin.cons x f i) = x * Finset.prod Finset.univ fun i => f i
theorem Fin.sum_univ_one {β : Type u_2} [] (f : Fin 1β) :
(Finset.sum Finset.univ fun i => f i) = f 0
theorem Fin.prod_univ_one {β : Type u_2} [] (f : Fin 1β) :
(Finset.prod Finset.univ fun i => f i) = f 0
@[simp]
theorem Fin.sum_univ_two {β : Type u_2} [] (f : Fin 2β) :
(Finset.sum Finset.univ fun i => f i) = f 0 + f 1
@[simp]
theorem Fin.prod_univ_two {β : Type u_2} [] (f : Fin 2β) :
(Finset.prod Finset.univ fun i => f i) = f 0 * f 1
theorem Fin.sum_univ_three {β : Type u_2} [] (f : Fin 3β) :
(Finset.sum Finset.univ fun i => f i) = f 0 + f 1 + f 2
theorem Fin.prod_univ_three {β : Type u_2} [] (f : Fin 3β) :
(Finset.prod Finset.univ fun i => f i) = f 0 * f 1 * f 2
theorem Fin.sum_univ_four {β : Type u_2} [] (f : Fin 4β) :
(Finset.sum Finset.univ fun i => f i) = f 0 + f 1 + f 2 + f 3
theorem Fin.prod_univ_four {β : Type u_2} [] (f : Fin 4β) :
(Finset.prod Finset.univ fun i => f i) = f 0 * f 1 * f 2 * f 3
theorem Fin.sum_univ_five {β : Type u_2} [] (f : Fin 5β) :
(Finset.sum Finset.univ fun i => f i) = f 0 + f 1 + f 2 + f 3 + f 4
theorem Fin.prod_univ_five {β : Type u_2} [] (f : Fin 5β) :
(Finset.prod Finset.univ fun i => f i) = f 0 * f 1 * f 2 * f 3 * f 4
theorem Fin.sum_univ_six {β : Type u_2} [] (f : Fin 6β) :
(Finset.sum Finset.univ fun i => f i) = f 0 + f 1 + f 2 + f 3 + f 4 + f 5
theorem Fin.prod_univ_six {β : Type u_2} [] (f : Fin 6β) :
(Finset.prod Finset.univ fun i => f i) = f 0 * f 1 * f 2 * f 3 * f 4 * f 5
theorem Fin.sum_univ_seven {β : Type u_2} [] (f : Fin 7β) :
(Finset.sum Finset.univ fun i => f i) = f 0 + f 1 + f 2 + f 3 + f 4 + f 5 + f 6
theorem Fin.prod_univ_seven {β : Type u_2} [] (f : Fin 7β) :
(Finset.prod Finset.univ fun i => f i) = f 0 * f 1 * f 2 * f 3 * f 4 * f 5 * f 6
theorem Fin.sum_univ_eight {β : Type u_2} [] (f : Fin 8β) :
(Finset.sum Finset.univ fun i => f i) = f 0 + f 1 + f 2 + f 3 + f 4 + f 5 + f 6 + f 7
theorem Fin.prod_univ_eight {β : Type u_2} [] (f : Fin 8β) :
(Finset.prod Finset.univ fun i => f i) = f 0 * f 1 * f 2 * f 3 * f 4 * f 5 * f 6 * f 7
theorem Fin.sum_pow_mul_eq_add_pow {n : } {R : Type u_3} [] (a : R) (b : R) :
(Finset.sum Finset.univ fun s => a ^ * b ^ (n - )) = (a + b) ^ n
theorem Fin.prod_const {α : Type u_1} [] (n : ) (x : α) :
(Finset.prod Finset.univ fun _i => x) = x ^ n
theorem Fin.sum_const {α : Type u_1} [] (n : ) (x : α) :
(Finset.sum Finset.univ fun _i => x) = n x
theorem Fin.sum_Ioi_zero {M : Type u_3} [] {n : } {v : Fin ()M} :
(Finset.sum () fun i => v i) = Finset.sum Finset.univ fun j => v ()
theorem Fin.prod_Ioi_zero {M : Type u_3} [] {n : } {v : Fin ()M} :
(Finset.prod () fun i => v i) = Finset.prod Finset.univ fun j => v ()
theorem Fin.sum_Ioi_succ {M : Type u_3} [] {n : } (i : Fin n) (v : Fin ()M) :
(Finset.sum () fun j => v j) = Finset.sum () fun j => v ()
theorem Fin.prod_Ioi_succ {M : Type u_3} [] {n : } (i : Fin n) (v : Fin ()M) :
(Finset.prod () fun j => v j) = Finset.prod () fun j => v ()
theorem Fin.sum_congr' {M : Type u_3} [] {a : } {b : } (f : Fin bM) (h : a = b) :
(Finset.sum Finset.univ fun i => f (Fin.cast h i)) = Finset.sum Finset.univ fun i => f i
theorem Fin.prod_congr' {M : Type u_3} [] {a : } {b : } (f : Fin bM) (h : a = b) :
(Finset.prod Finset.univ fun i => f (Fin.cast h i)) = Finset.prod Finset.univ fun i => f i
theorem Fin.sum_univ_add {M : Type u_3} [] {a : } {b : } (f : Fin (a + b)M) :
(Finset.sum Finset.univ fun i => f i) = (Finset.sum Finset.univ fun i => f ()) + Finset.sum Finset.univ fun i => f ()
theorem Fin.prod_univ_add {M : Type u_3} [] {a : } {b : } (f : Fin (a + b)M) :
(Finset.prod Finset.univ fun i => f i) = (Finset.prod Finset.univ fun i => f ()) * Finset.prod Finset.univ fun i => f ()
theorem Fin.sum_trunc {M : Type u_3} [] {a : } {b : } (f : Fin (a + b)M) (hf : ∀ (j : Fin b), f () = 0) :
(Finset.sum Finset.univ fun i => f i) = Finset.sum Finset.univ fun i => f (Fin.castLE (_ : a a + b) i)
theorem Fin.prod_trunc {M : Type u_3} [] {a : } {b : } (f : Fin (a + b)M) (hf : ∀ (j : Fin b), f () = 1) :
(Finset.prod Finset.univ fun i => f i) = Finset.prod Finset.univ fun i => f (Fin.castLE (_ : a a + b) i)
def Fin.partialSum {α : Type u_1} [] {n : } (f : Fin nα) (i : Fin (n + 1)) :
α

For f = (a₁, ..., aₙ) in αⁿ, partialSum f is

(0, a₁, a₁ + a₂, ..., a₁ + ... + aₙ) in αⁿ⁺¹.

Instances For
def Fin.partialProd {α : Type u_1} [] {n : } (f : Fin nα) (i : Fin (n + 1)) :
α

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

Instances For
@[simp]
theorem Fin.partialSum_zero {α : Type u_1} [] {n : } (f : Fin nα) :
= 0
@[simp]
theorem Fin.partialProd_zero {α : Type u_1} [] {n : } (f : Fin nα) :
= 1
theorem Fin.partialSum_succ {α : Type u_1} [] {n : } (f : Fin nα) (j : Fin n) :
= + f j
theorem Fin.partialProd_succ {α : Type u_1} [] {n : } (f : Fin nα) (j : Fin n) :
= * f j
theorem Fin.partialSum_succ' {α : Type u_1} [] {n : } (f : Fin (n + 1)α) (j : Fin (n + 1)) :
= f 0 +
theorem Fin.partialProd_succ' {α : Type u_1} [] {n : } (f : Fin (n + 1)α) (j : Fin (n + 1)) :
= f 0 *
theorem Fin.partialSum_left_neg {n : } {G : Type u_3} [] (f : Fin (n + 1)G) :
(f 0 +ᵥ Fin.partialSum fun i => -f i + f ()) = f
theorem Fin.partialProd_left_inv {n : } {G : Type u_3} [] (f : Fin (n + 1)G) :
(f 0 Fin.partialProd fun i => (f i)⁻¹ * f ()) = f
theorem Fin.partialSum_right_neg {n : } {G : Type u_3} [] (f : Fin nG) (i : Fin n) :
- + = f i
theorem Fin.partialProd_right_inv {n : } {G : Type u_3} [] (f : Fin nG) (i : Fin n) :
()⁻¹ * = f i
theorem Fin.neg_partialSum_add_eq_contractNth {n : } {G : Type u_3} [] (g : Fin (n + 1)G) (j : Fin (n + 1)) (k : Fin n) :
-Fin.partialSum g (Fin.succAbove () ()) + Fin.partialSum g (Fin.succ ()) = Fin.contractNth j (fun x x_1 => x + x_1) 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.inv_partialProd_mul_eq_contractNth {n : } {G : Type u_3} [] (g : Fin (n + 1)G) (j : Fin (n + 1)) (k : Fin n) :
(Fin.partialProd g (Fin.succAbove () ()))⁻¹ * Fin.partialProd g (Fin.succ ()) = Fin.contractNth j (fun x x_1 => x * x_1) 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.

@[simp]
theorem finFunctionFinEquiv_apply_val {m : } {n : } (f : Fin nFin m) :
↑(finFunctionFinEquiv f) = Finset.sum Finset.univ fun i => ↑(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
def finFunctionFinEquiv {m : } {n : } :
(Fin nFin m) Fin (m ^ n)

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

Instances For
theorem finFunctionFinEquiv_apply {m : } {n : } (f : Fin nFin m) :
↑(finFunctionFinEquiv f) = Finset.sum Finset.univ fun i => ↑(f i) * m ^ i
theorem finFunctionFinEquiv_single {m : } {n : } [] (i : Fin n) (j : Fin m) :
↑(finFunctionFinEquiv ()) = j * m ^ i
def finPiFinEquiv {m : } {n : Fin m} :
((i : Fin m) → Fin (n i)) Fin (Finset.prod Finset.univ fun i => n i)

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

Instances For
theorem finPiFinEquiv_apply {m : } {n : Fin m} (f : (i : Fin m) → Fin (n i)) :
↑(finPiFinEquiv f) = Finset.sum Finset.univ fun i => ↑(f i) * Finset.prod Finset.univ fun j => n (Fin.castLE (_ : i m) j)
theorem finPiFinEquiv_single {m : } {n : Fin m} [∀ (i : Fin m), NeZero (n i)] (i : Fin m) (j : Fin (n i)) :
↑(finPiFinEquiv ()) = j * Finset.prod Finset.univ fun j => n (Fin.castLE (_ : i m) j)
theorem List.sum_take_ofFn {α : Type u_1} [] {n : } (f : Fin nα) (i : ) :
List.sum (List.take i ()) = Finset.sum (Finset.filter (fun j => j < i) Finset.univ) fun j => f j
theorem List.prod_take_ofFn {α : Type u_1} [] {n : } (f : Fin nα) (i : ) :
List.prod (List.take i ()) = Finset.prod (Finset.filter (fun j => j < i) Finset.univ) fun j => f j
theorem List.sum_ofFn {α : Type u_1} [] {n : } {f : Fin nα} :
= Finset.sum Finset.univ fun i => f i
theorem List.prod_ofFn {α : Type u_1} [] {n : } {f : Fin nα} :
= Finset.prod Finset.univ fun i => f i
abbrev List.alternatingSum_eq_finset_sum.match_1 {G : Type u_1} (motive : List GProp) :
(x : List G) → (Unitmotive []) → ((g : G) → motive [g]) → ((g h : G) → (L : List G) → motive (g :: h :: L)) → motive x
Instances For
theorem List.alternatingSum_eq_finset_sum {G : Type u_3} [] (L : List G) :
= Finset.sum Finset.univ fun i => (-1) ^ i List.get L i
theorem List.alternatingProd_eq_finset_prod {G : Type u_3} [] (L : List G) :
= Finset.prod Finset.univ fun i => List.get L i ^ (-1) ^ i