# mathlib3documentation

algebra.big_operators.fin

# Big operators and fin#

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Some results about products and sums over the type fin.

The most important results are the induction formulas fin.prod_univ_cast_succ 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 #

• fin_function_fin_equiv: An explicit equivalence between fin n → fin m and fin (m ^ n).
theorem finset.sum_range {β : Type u_2} {n : } (f : β) :
(finset.range n).sum (λ (i : ), f i) = finset.univ.sum (λ (i : fin n), f i)
theorem finset.prod_range {β : Type u_2} [comm_monoid β] {n : } (f : β) :
(finset.range n).prod (λ (i : ), f i) = finset.univ.prod (λ (i : fin n), f i)
theorem fin.prod_univ_def {β : Type u_2} [comm_monoid β] {n : } (f : fin n β) :
finset.univ.prod (λ (i : fin n), f i) = (list.map f (list.fin_range n)).prod
theorem fin.sum_univ_def {β : Type u_2} {n : } (f : fin n β) :
finset.univ.sum (λ (i : fin n), f i) = (list.map f (list.fin_range n)).sum
theorem fin.sum_of_fn {β : Type u_2} {n : } (f : fin n β) :
(list.of_fn f).sum = finset.univ.sum (λ (i : fin n), f i)
theorem fin.prod_of_fn {β : Type u_2} [comm_monoid β] {n : } (f : fin n β) :
(list.of_fn f).prod = finset.univ.prod (λ (i : fin n), f i)
theorem fin.sum_univ_zero {β : Type u_2} (f : fin 0 β) :
finset.univ.sum (λ (i : fin 0), 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} [comm_monoid β] (f : fin 0 β) :
finset.univ.prod (λ (i : fin 0), f i) = 1

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

theorem fin.prod_univ_succ_above {β : Type u_2} [comm_monoid β] {n : } (f : fin (n + 1) β) (x : fin (n + 1)) :
finset.univ.prod (λ (i : fin (n + 1)), f i) = f x * finset.univ.prod (λ (i : fin n), f ((x.succ_above) i))

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_above {β : Type u_2} {n : } (f : fin (n + 1) β) (x : fin (n + 1)) :
finset.univ.sum (λ (i : fin (n + 1)), f i) = f x + finset.univ.sum (λ (i : fin n), f ((x.succ_above) i))

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_succ {β : Type u_2} [comm_monoid β] {n : } (f : fin (n + 1) β) :
finset.univ.prod (λ (i : fin (n + 1)), f i) = f 0 * finset.univ.prod (λ (i : fin n), f i.succ)

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_succ {β : Type u_2} {n : } (f : fin (n + 1) β) :
finset.univ.sum (λ (i : fin (n + 1)), f i) = f 0 + finset.univ.sum (λ (i : fin n), f i.succ)

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.sum_univ_cast_succ {β : Type u_2} {n : } (f : fin (n + 1) β) :
finset.univ.sum (λ (i : fin (n + 1)), f i) = finset.univ.sum (λ (i : fin n), f (fin.cast_succ i)) + f (fin.last n)

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_cast_succ {β : Type u_2} [comm_monoid β] {n : } (f : fin (n + 1) β) :
finset.univ.prod (λ (i : fin (n + 1)), f i) = finset.univ.prod (λ (i : fin n), f (fin.cast_succ i)) * f (fin.last n)

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.univ.sum (λ (i : fin n.succ), f i) = x + finset.univ.sum (λ (i : fin n), f i)
theorem fin.prod_cons {β : Type u_2} [comm_monoid β] {n : } (x : β) (f : fin n β) :
finset.univ.prod (λ (i : fin n.succ), f i) = x * finset.univ.prod (λ (i : fin n), f i)
theorem fin.prod_univ_one {β : Type u_2} [comm_monoid β] (f : fin 1 β) :
finset.univ.prod (λ (i : fin 1), f i) = f 0
theorem fin.sum_univ_one {β : Type u_2} (f : fin 1 β) :
finset.univ.sum (λ (i : fin 1), f i) = f 0
@[simp]
theorem fin.prod_univ_two {β : Type u_2} [comm_monoid β] (f : fin 2 β) :
finset.univ.prod (λ (i : fin 2), f i) = f 0 * f 1
@[simp]
theorem fin.sum_univ_two {β : Type u_2} (f : fin 2 β) :
finset.univ.sum (λ (i : fin 2), f i) = f 0 + f 1
theorem fin.sum_univ_three {β : Type u_2} (f : fin 3 β) :
finset.univ.sum (λ (i : fin 3), f i) = f 0 + f 1 + f 2
theorem fin.prod_univ_three {β : Type u_2} [comm_monoid β] (f : fin 3 β) :
finset.univ.prod (λ (i : fin 3), f i) = f 0 * f 1 * f 2
theorem fin.prod_univ_four {β : Type u_2} [comm_monoid β] (f : fin 4 β) :
finset.univ.prod (λ (i : fin 4), f i) = f 0 * f 1 * f 2 * f 3
theorem fin.sum_univ_four {β : Type u_2} (f : fin 4 β) :
finset.univ.sum (λ (i : fin 4), f i) = f 0 + f 1 + f 2 + f 3
theorem fin.sum_univ_five {β : Type u_2} (f : fin 5 β) :
finset.univ.sum (λ (i : fin 5), f i) = f 0 + f 1 + f 2 + f 3 + f 4
theorem fin.prod_univ_five {β : Type u_2} [comm_monoid β] (f : fin 5 β) :
finset.univ.prod (λ (i : fin 5), f i) = f 0 * f 1 * f 2 * f 3 * f 4
theorem fin.sum_univ_six {β : Type u_2} (f : fin 6 β) :
finset.univ.sum (λ (i : fin 6), f i) = f 0 + f 1 + f 2 + f 3 + f 4 + f 5
theorem fin.prod_univ_six {β : Type u_2} [comm_monoid β] (f : fin 6 β) :
finset.univ.prod (λ (i : fin 6), f i) = f 0 * f 1 * f 2 * f 3 * f 4 * f 5
theorem fin.prod_univ_seven {β : Type u_2} [comm_monoid β] (f : fin 7 β) :
finset.univ.prod (λ (i : fin 7), f i) = f 0 * f 1 * f 2 * f 3 * f 4 * f 5 * f 6
theorem fin.sum_univ_seven {β : Type u_2} (f : fin 7 β) :
finset.univ.sum (λ (i : fin 7), 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.univ.sum (λ (i : fin 8), 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} [comm_monoid β] (f : fin 8 β) :
finset.univ.prod (λ (i : fin 8), 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_1} (a b : R) :
finset.univ.sum (λ (s : finset (fin n)), a ^ s.card * b ^ (n - s.card)) = (a + b) ^ n
theorem fin.prod_const {α : Type u_1} [comm_monoid α] (n : ) (x : α) :
finset.univ.prod (λ (i : fin n), x) = x ^ n
theorem fin.sum_const {α : Type u_1} (n : ) (x : α) :
finset.univ.sum (λ (i : fin n), x) = n x
theorem fin.sum_Ioi_zero {M : Type u_1} {n : } {v : fin n.succ M} :
(finset.Ioi 0).sum (λ (i : fin n.succ), v i) = finset.univ.sum (λ (j : fin n), v j.succ)
theorem fin.prod_Ioi_zero {M : Type u_1} [comm_monoid M] {n : } {v : fin n.succ M} :
(finset.Ioi 0).prod (λ (i : fin n.succ), v i) = finset.univ.prod (λ (j : fin n), v j.succ)
theorem fin.sum_Ioi_succ {M : Type u_1} {n : } (i : fin n) (v : fin n.succ M) :
(finset.Ioi i.succ).sum (λ (j : fin n.succ), v j) = (finset.Ioi i).sum (λ (j : fin n), v j.succ)
theorem fin.prod_Ioi_succ {M : Type u_1} [comm_monoid M] {n : } (i : fin n) (v : fin n.succ M) :
(finset.Ioi i.succ).prod (λ (j : fin n.succ), v j) = (finset.Ioi i).prod (λ (j : fin n), v j.succ)
theorem fin.sum_congr' {M : Type u_1} {a b : } (f : fin b M) (h : a = b) :
finset.univ.sum (λ (i : fin a), f ((fin.cast h) i)) = finset.univ.sum (λ (i : fin b), f i)
theorem fin.prod_congr' {M : Type u_1} [comm_monoid M] {a b : } (f : fin b M) (h : a = b) :
finset.univ.prod (λ (i : fin a), f ((fin.cast h) i)) = finset.univ.prod (λ (i : fin b), f i)
theorem fin.prod_univ_add {M : Type u_1} [comm_monoid M] {a b : } (f : fin (a + b) M) :
finset.univ.prod (λ (i : fin (a + b)), f i) = finset.univ.prod (λ (i : fin a), f ((fin.cast_add b) i)) * finset.univ.prod (λ (i : fin b), f ((fin.nat_add a) i))
theorem fin.sum_univ_add {M : Type u_1} {a b : } (f : fin (a + b) M) :
finset.univ.sum (λ (i : fin (a + b)), f i) = finset.univ.sum (λ (i : fin a), f ((fin.cast_add b) i)) + finset.univ.sum (λ (i : fin b), f ((fin.nat_add a) i))
theorem fin.prod_trunc {M : Type u_1} [comm_monoid M] {a b : } (f : fin (a + b) M) (hf : (j : fin b), f ((fin.nat_add a) j) = 1) :
finset.univ.prod (λ (i : fin (a + b)), f i) = finset.univ.prod (λ (i : fin a), f ((fin.cast_le _) i))
theorem fin.sum_trunc {M : Type u_1} {a b : } (f : fin (a + b) M) (hf : (j : fin b), f ((fin.nat_add a) j) = 0) :
finset.univ.sum (λ (i : fin (a + b)), f i) = finset.univ.sum (λ (i : fin a), f ((fin.cast_le _) i))
def fin.partial_prod {α : Type u_1} [monoid α] {n : } (f : fin n α) (i : fin (n + 1)) :
α

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

Equations
def fin.partial_sum {α : Type u_1} [add_monoid α] {n : } (f : fin n α) (i : fin (n + 1)) :
α

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

Equations
@[simp]
theorem fin.partial_sum_zero {α : Type u_1} [add_monoid α] {n : } (f : fin n α) :
= 0
@[simp]
theorem fin.partial_prod_zero {α : Type u_1} [monoid α] {n : } (f : fin n α) :
= 1
theorem fin.partial_sum_succ {α : Type u_1} [add_monoid α] {n : } (f : fin n α) (j : fin n) :
= + f j
theorem fin.partial_prod_succ {α : Type u_1} [monoid α] {n : } (f : fin n α) (j : fin n) :
= * f j
theorem fin.partial_prod_succ' {α : Type u_1} [monoid α] {n : } (f : fin (n + 1) α) (j : fin (n + 1)) :
= f 0 * j
theorem fin.partial_sum_succ' {α : Type u_1} [add_monoid α] {n : } (f : fin (n + 1) α) (j : fin (n + 1)) :
= f 0 + j
theorem fin.partial_sum_left_neg {n : } {G : Type u_1} [add_group G] (f : fin (n + 1) G) :
f 0 +ᵥ fin.partial_sum (λ (i : fin n), -f i + f i.succ) = f
theorem fin.partial_prod_left_inv {n : } {G : Type u_1} [group G] (f : fin (n + 1) G) :
f 0 fin.partial_prod (λ (i : fin n), (f i)⁻¹ * f i.succ) = f
theorem fin.partial_prod_right_inv {n : } {G : Type u_1} [group G] (f : fin n G) (i : fin n) :
theorem fin.partial_sum_right_neg {n : } {G : Type u_1} [add_group G] (f : fin n G) (i : fin n) :
= f i
theorem fin.neg_partial_sum_add_eq_contract_nth {n : } {G : Type u_1} [add_group G] (g : fin (n + 1) G) (j : fin (n + 1)) (k : fin n) :

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_partial_prod_mul_eq_contract_nth {n : } {G : Type u_1} [group G] (g : fin (n + 1) G) (j : fin (n + 1)) (k : fin n) :

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 fin_function_fin_equiv_symm_apply_val {m n : } (a : fin (m ^ n)) (b : fin n) :
b).val = a / m ^ b % m
def fin_function_fin_equiv {m n : } :
(fin n fin m) fin (m ^ n)

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

Equations
@[simp]
theorem fin_function_fin_equiv_apply_val {m n : } (f : fin n fin m) :
= finset.univ.sum (λ (i : fin n), (f i) * m ^ i)
theorem fin_function_fin_equiv_apply {m n : } (f : fin n fin m) :
= finset.univ.sum (λ (i : fin n), (f i) * m ^ i)
theorem fin_function_fin_equiv_single {m n : } [ne_zero m] (i : fin n) (j : fin m) :
def fin_pi_fin_equiv {m : } {n : fin m } :
(Π (i : fin m), fin (n i)) fin (finset.univ.prod (λ (i : fin m), n i))

Equivalence between Π i : fin m, fin (n i) and fin (∏ i : fin m, n i).

Equations
theorem fin_pi_fin_equiv_apply {m : } {n : fin m } (f : Π (i : fin m), fin (n i)) :
= finset.univ.sum (λ (i : fin m), (f i) * finset.univ.prod (λ (j : fin i), n ((fin.cast_le _) j)))
theorem fin_pi_fin_equiv_single {m : } {n : fin m } [ (i : fin m), ne_zero (n i)] (i : fin m) (j : fin (n i)) :
theorem list.sum_take_of_fn {α : Type u_1} {n : } (f : fin n α) (i : ) :
(list.of_fn f)).sum = (finset.filter (λ (j : fin n), j.val < i) finset.univ).sum (λ (j : fin n), f j)
theorem list.prod_take_of_fn {α : Type u_1} [comm_monoid α] {n : } (f : fin n α) (i : ) :
(list.of_fn f)).prod = (finset.filter (λ (j : fin n), j.val < i) finset.univ).prod (λ (j : fin n), f j)
theorem list.sum_of_fn {α : Type u_1} {n : } {f : fin n α} :
(list.of_fn f).sum = finset.univ.sum (λ (i : fin n), f i)
theorem list.prod_of_fn {α : Type u_1} [comm_monoid α] {n : } {f : fin n α} :
(list.of_fn f).prod = finset.univ.prod (λ (i : fin n), f i)
theorem list.alternating_sum_eq_finset_sum {G : Type u_1} (L : list G) :
L.alternating_sum = finset.univ.sum (λ (i : fin L.length), (-1) ^ i L.nth_le i _)
theorem list.alternating_prod_eq_finset_prod {G : Type u_1} [comm_group G] (L : list G) :
L.alternating_prod = finset.univ.prod (λ (i : fin L.length), L.nth_le i _ ^ (-1) ^ i)