Sums and products from lists

This file provides further results about List.prod, List.sum, which calculate the product and sum of elements of a list and List.alternatingProd, List.alternatingSum, their alternating counterparts.

theorem List.prod_isUnit {M : Type u_4} [Monoid M] {L : List M} : (∀ (m : M), m ∈ L → IsUnit m) → IsUnit L.prod

theorem List.sum_isAddUnit {M : Type u_4} [AddMonoid M] {L : List M} : (∀ (m : M), m ∈ L → IsAddUnit m) → IsAddUnit L.sum

theorem List.prod_isUnit_iff {M : Type u_8} [CommMonoid M] {L : List M} : IsUnit L.prod ↔ ∀ (m : M), m ∈ L → IsUnit m

theorem List.sum_isAddUnit_iff {M : Type u_8} [AddCommMonoid M] {L : List M} : IsAddUnit L.sum ↔ ∀ (m : M), m ∈ L → IsAddUnit m

theorem List.Perm.prod_eq' {M : Type u_4} [Monoid M] {l₁ l₂ : List M} (h : l₁.Perm l₂) (hc : Pairwise Commute l₁) : l₁.prod = l₂.prod

If elements of a list commute with each other, then their product does not depend on the order of elements.

theorem List.Perm.sum_eq' {M : Type u_4} [AddMonoid M] {l₁ l₂ : List M} (h : l₁.Perm l₂) (hc : Pairwise AddCommute l₁) : l₁.sum = l₂.sum

If elements of a list additively commute with each other, then their sum does not depend on the order of elements.

theorem List.prod_rotate_eq_one_of_prod_eq_one {G : Type u_7} [Group G] {l : List G} : l.prod = 1 → ∀ (n : ℕ), (l.rotate n).prod = 1

theorem List.sum_map_count_dedup_filter_eq_countP {α : Type u_2} [DecidableEq α] (p : α → Bool) (l : List α) : (map (fun (x : α) => count x l) (filter p l.dedup)).sum = countP p l

Summing the count of x over a list filtered by some p is just countP applied to p

theorem List.sum_map_count_dedup_eq_length {α : Type u_2} [DecidableEq α] (l : List α) : (map (fun (x : α) => count x l) l.dedup).sum = l.length

theorem List.length_sigma {α : Type u_2} {σ : α → Type u_8} (l₁ : List α) (l₂ : (a : α) → List (σ a)) : (l₁.sigma l₂).length = (map (fun (a : α) => (l₂ a).length) l₁).sum

theorem List.ranges_flatten (l : List ℕ) : l.ranges.flatten = range l.sum

theorem List.ranges_nodup {l s : List ℕ} (hs : s ∈ l.ranges) : s.Nodup

The members of l.ranges have no duplicates

theorem List.mem_mem_ranges_iff_lt_sum (l : List ℕ) {n : ℕ} : (∃ (s : List ℕ), s ∈ l.ranges ∧ n ∈ s) ↔ n < l.sum

Any entry of any member of l.ranges is strictly smaller than l.sum.

theorem List.drop_take_succ_flatten_eq_getElem {α : Type u_2} (L : List (List α)) (i : ℕ) (h : i < L.length) : drop (take i (map length L)).sum (take (take (i + 1) (map length L)).sum L.flatten) = L[i]

In a flatten of sublists, taking the slice between the indices A and B - 1 gives back the original sublist of index i if A is the sum of the lengths of sublists of index < i, and B is the sum of the lengths of sublists of index ≤ i.

theorem List.neg_one_mem_of_prod_eq_neg_one {l : List ℤ} (h : l.prod = -1) : -1 ∈ l

If a product of integers is -1, then at least one factor must be -1.

theorem List.dvd_prod {M : Type u_4} [CommMonoid M] {a : M} {l : List M} (ha : a ∈ l) : a ∣ l.prod

theorem List.Sublist.prod_dvd_prod {M : Type u_4} [CommMonoid M] {l₁ l₂ : List M} (h : l₁.Sublist l₂) : l₁.prod ∣ l₂.prod

theorem List.alternatingProd_append {G : Type u_7} [CommGroup G] (l₁ l₂ : List G) : (l₁ ++ l₂).alternatingProd = l₁.alternatingProd * l₂.alternatingProd ^ (-1) ^ l₁.length

theorem List.alternatingSum_append {G : Type u_7} [AddCommGroup G] (l₁ l₂ : List G) : (l₁ ++ l₂).alternatingSum = l₁.alternatingSum + (-1) ^ l₁.length • l₂.alternatingSum

theorem List.alternatingProd_reverse {G : Type u_7} [CommGroup G] (l : List G) : l.reverse.alternatingProd = l.alternatingProd ^ (-1) ^ (l.length + 1)

theorem List.alternatingSum_reverse {G : Type u_7} [AddCommGroup G] (l : List G) : l.reverse.alternatingSum = (-1) ^ (l.length + 1) • l.alternatingSum

theorem MulOpposite.op_list_prod {M : Type u_4} [Monoid M] (l : List M) : op l.prod = (List.map op l).reverse.prod

theorem MulOpposite.unop_list_prod {M : Type u_4} [Monoid M] (l : List Mᵐᵒᵖ) : unop l.prod = (List.map unop l).reverse.prod

theorem unop_map_list_prod {M : Type u_4} {N : Type u_5} [Monoid M] [Monoid N] {F : Type u_8} [FunLike F M Nᵐᵒᵖ] [MonoidHomClass F M Nᵐᵒᵖ] (f : F) (l : List M) : MulOpposite.unop (f l.prod) = (List.map (MulOpposite.unop ∘ ⇑f) l).reverse.prod

A morphism into the opposite monoid acts on the product by acting on the reversed elements.