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 ∈ L, IsUnit m) → IsUnit L.prod

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

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

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

theorem List.Perm.prod_eq' {M : Type u_4} [Monoid M] {l₁ l₂ : List M} (h : l₁.Perm l₂) (hc : List.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 : List.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 α) : (List.map (fun (x : α) => List.count x l) (List.filter p l.dedup)).sum = List.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 α) : (List.map (fun (x : α) => List.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 = (List.map (fun (a : α) => (l₂ a).length) l₁).sum

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

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

The members of l.ranges have no duplicate

@[deprecated List.ranges_flatten (since := "2024-10-15")]

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

Alias of List.ranges_flatten.

theorem List.mem_mem_ranges_iff_lt_sum (l : List ℕ) {n : ℕ} : (∃ 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) : List.drop (List.take i (List.map List.length L)).sum (List.take (List.take (i + 1) (List.map List.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.

@[deprecated List.drop_take_succ_flatten_eq_getElem (since := "2024-06-11")]

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

Alias of List.drop_take_succ_flatten_eq_getElem.

---

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.

@[deprecated List.drop_take_succ_flatten_eq_getElem (since := "2024-06-11")]

theorem List.drop_take_succ_join_eq_get {α : Type u_2} (L : List (List α)) (i : Fin L.length) : List.drop (List.take (↑i) (List.map List.length L)).sum (List.take (List.take (↑i + 1) (List.map List.length L)).sum L.flatten) = L.get 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 {α : Type u_2} [CommGroup α] (l₁ l₂ : List α) : (l₁ ++ l₂).alternatingProd = l₁.alternatingProd * l₂.alternatingProd ^ (-1) ^ l₁.length

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

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

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

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

theorem MulOpposite.unop_list_prod {M : Type u_4} [Monoid M] (l : List Mᵐᵒᵖ) : MulOpposite.unop l.prod = (List.map MulOpposite.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.