Sums and products from lists

This file provides basic 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_eq_foldl {M : Type u_4} [Monoid M] {l : List M} : l.prod = foldl (fun (x1 x2 : M) => x1 * x2) 1 l

theorem List.sum_eq_foldl {M : Type u_4} [AddMonoid M] {l : List M} : l.sum = foldl (fun (x1 x2 : M) => x1 + x2) 0 l

@[simp]

theorem List.prod_append {M : Type u_4} [Monoid M] {l₁ l₂ : List M} : (l₁ ++ l₂).prod = l₁.prod * l₂.prod

@[simp]

theorem List.sum_append {M : Type u_4} [AddMonoid M] {l₁ l₂ : List M} : (l₁ ++ l₂).sum = l₁.sum + l₂.sum

theorem List.prod_concat {M : Type u_4} [Monoid M] {l : List M} {a : M} : (l.concat a).prod = l.prod * a

theorem List.sum_concat {M : Type u_4} [AddMonoid M] {l : List M} {a : M} : (l.concat a).sum = l.sum + a

@[simp]

theorem List.prod_flatten {M : Type u_4} [Monoid M] {l : List (List M)} : l.flatten.prod = (map prod l).prod

@[simp]

theorem List.sum_flatten {M : Type u_4} [AddMonoid M] {l : List (List M)} : l.flatten.sum = (map sum l).sum

theorem List.rel_prod {M : Type u_4} {N : Type u_5} [Monoid M] [Monoid N] {R : M → N → Prop} (h : R 1 1) (hf : Relator.LiftFun R (Relator.LiftFun R R) (fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : N) => x1 * x2) : Relator.LiftFun (Forall₂ R) R prod prod

theorem List.rel_sum {M : Type u_4} {N : Type u_5} [AddMonoid M] [AddMonoid N] {R : M → N → Prop} (h : R 0 0) (hf : Relator.LiftFun R (Relator.LiftFun R R) (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : N) => x1 + x2) : Relator.LiftFun (Forall₂ R) R sum sum

theorem List.prod_hom_nonempty {M : Type u_4} {N : Type u_5} [Monoid M] [Monoid N] {l : List M} {F : Type u_8} [FunLike F M N] [MulHomClass F M N] (f : F) (hl : l ≠ []) : (map (⇑f) l).prod = f l.prod

theorem List.sum_hom_nonempty {M : Type u_4} {N : Type u_5} [AddMonoid M] [AddMonoid N] {l : List M} {F : Type u_8} [FunLike F M N] [AddHomClass F M N] (f : F) (hl : l ≠ []) : (map (⇑f) l).sum = f l.sum

theorem List.prod_hom {M : Type u_4} {N : Type u_5} [Monoid M] [Monoid N] (l : List M) {F : Type u_8} [FunLike F M N] [MonoidHomClass F M N] (f : F) : (map (⇑f) l).prod = f l.prod

theorem List.sum_hom {M : Type u_4} {N : Type u_5} [AddMonoid M] [AddMonoid N] (l : List M) {F : Type u_8} [FunLike F M N] [AddMonoidHomClass F M N] (f : F) : (map (⇑f) l).sum = f l.sum

theorem List.prod_hom₂_nonempty {ι : Type u_1} {M : Type u_4} {N : Type u_5} {P : Type u_6} [Monoid M] [Monoid N] [Monoid P] {l : List ι} (f : M → N → P) (hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d) (f₁ : ι → M) (f₂ : ι → N) (hl : l ≠ []) : (map (fun (i : ι) => f (f₁ i) (f₂ i)) l).prod = f (map f₁ l).prod (map f₂ l).prod

theorem List.sum_hom₂_nonempty {ι : Type u_1} {M : Type u_4} {N : Type u_5} {P : Type u_6} [AddMonoid M] [AddMonoid N] [AddMonoid P] {l : List ι} (f : M → N → P) (hf : ∀ (a b : M) (c d : N), f (a + b) (c + d) = f a c + f b d) (f₁ : ι → M) (f₂ : ι → N) (hl : l ≠ []) : (map (fun (i : ι) => f (f₁ i) (f₂ i)) l).sum = f (map f₁ l).sum (map f₂ l).sum

theorem List.prod_hom₂ {ι : Type u_1} {M : Type u_4} {N : Type u_5} {P : Type u_6} [Monoid M] [Monoid N] [Monoid P] (l : List ι) (f : M → N → P) (hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d) (hf' : f 1 1 = 1) (f₁ : ι → M) (f₂ : ι → N) : (map (fun (i : ι) => f (f₁ i) (f₂ i)) l).prod = f (map f₁ l).prod (map f₂ l).prod

theorem List.sum_hom₂ {ι : Type u_1} {M : Type u_4} {N : Type u_5} {P : Type u_6} [AddMonoid M] [AddMonoid N] [AddMonoid P] (l : List ι) (f : M → N → P) (hf : ∀ (a b : M) (c d : N), f (a + b) (c + d) = f a c + f b d) (hf' : f 0 0 = 0) (f₁ : ι → M) (f₂ : ι → N) : (map (fun (i : ι) => f (f₁ i) (f₂ i)) l).sum = f (map f₁ l).sum (map f₂ l).sum

@[simp]

theorem List.prod_map_mul {ι : Type u_1} {M : Type u_8} [CommMonoid M] {l : List ι} {f g : ι → M} : (map (fun (i : ι) => f i * g i) l).prod = (map f l).prod * (map g l).prod

@[simp]

theorem List.sum_map_add {ι : Type u_1} {M : Type u_8} [AddCommMonoid M] {l : List ι} {f g : ι → M} : (map (fun (i : ι) => f i + g i) l).sum = (map f l).sum + (map g l).sum

theorem List.prod_map_hom {ι : Type u_1} {M : Type u_4} {N : Type u_5} [Monoid M] [Monoid N] (L : List ι) (f : ι → M) {G : Type u_8} [FunLike G M N] [MonoidHomClass G M N] (g : G) : (map (⇑g ∘ f) L).prod = g (map f L).prod

theorem List.sum_map_hom {ι : Type u_1} {M : Type u_4} {N : Type u_5} [AddMonoid M] [AddMonoid N] (L : List ι) (f : ι → M) {G : Type u_8} [FunLike G M N] [AddMonoidHomClass G M N] (g : G) : (map (⇑g ∘ f) L).sum = g (map f L).sum

@[simp]

theorem List.prod_take_mul_prod_drop {M : Type u_4} [Monoid M] (L : List M) (i : ℕ) : (take i L).prod * (drop i L).prod = L.prod

@[simp]

theorem List.sum_take_add_sum_drop {M : Type u_4} [AddMonoid M] (L : List M) (i : ℕ) : (take i L).sum + (drop i L).sum = L.sum

@[simp]

theorem List.prod_take_succ {M : Type u_4} [Monoid M] (L : List M) (i : ℕ) (p : i < L.length) : (take (i + 1) L).prod = (take i L).prod * L[i]

@[simp]

theorem List.sum_take_succ {M : Type u_4} [AddMonoid M] (L : List M) (i : ℕ) (p : i < L.length) : (take (i + 1) L).sum = (take i L).sum + L[i]

theorem List.length_pos_of_prod_ne_one {M : Type u_4} [Monoid M] (L : List M) (h : L.prod ≠ 1) : 0 < L.length

A list with product not one must have positive length.

theorem List.length_pos_of_sum_ne_zero {M : Type u_4} [AddMonoid M] (L : List M) (h : L.sum ≠ 0) : 0 < L.length

A list with sum not zero must have positive length.

theorem List.length_pos_of_one_lt_prod {M : Type u_4} [Monoid M] [Preorder M] (L : List M) (h : 1 < L.prod) : 0 < L.length

A list with product greater than one must have positive length.

theorem List.length_pos_of_sum_pos {M : Type u_4} [AddMonoid M] [Preorder M] (L : List M) (h : 0 < L.sum) : 0 < L.length

A list with positive sum must have positive length.

theorem List.length_pos_of_prod_lt_one {M : Type u_4} [Monoid M] [Preorder M] (L : List M) (h : L.prod < 1) : 0 < L.length

A list with product less than one must have positive length.

theorem List.length_pos_of_sum_neg {M : Type u_4} [AddMonoid M] [Preorder M] (L : List M) (h : L.sum < 0) : 0 < L.length

A list with negative sum must have positive length.

theorem List.prod_set {M : Type u_4} [Monoid M] (L : List M) (n : ℕ) (a : M) : (L.set n a).prod = ((take n L).prod * if n < L.length then a else 1) * (drop (n + 1) L).prod

theorem List.sum_set {M : Type u_4} [AddMonoid M] (L : List M) (n : ℕ) (a : M) : (L.set n a).sum = ((take n L).sum + if n < L.length then a else 0) + (drop (n + 1) L).sum

theorem List.getElem?_zero_mul_tail_prod {M : Type u_4} [Monoid M] (l : List M) : l[0]?.getD 1 * l.tail.prod = l.prod

We'd like to state this as L.headI * L.tail.prod = L.prod, but because L.headI relies on an inhabited instance to return a garbage value on the empty list, this is not possible. Instead, we write the statement in terms of L[0]?.getD 1.

theorem List.getElem?_zero_add_tail_sum {M : Type u_4} [AddMonoid M] (l : List M) : l[0]?.getD 0 + l.tail.sum = l.sum

We'd like to state this as L.headI + L.tail.sum = L.sum, but because L.headI relies on an inhabited instance to return a garbage value on the empty list, this is not possible. Instead, we write the statement in terms of L[0]?.getD 0.

theorem List.headI_mul_tail_prod_of_ne_nil {M : Type u_4} [Monoid M] [Inhabited M] (l : List M) (h : l ≠ []) : l.headI * l.tail.prod = l.prod

Same as get?_zero_mul_tail_prod, but avoiding the List.headI garbage complication by requiring the list to be nonempty.

theorem List.headI_add_tail_sum_of_ne_nil {M : Type u_4} [AddMonoid M] [Inhabited M] (l : List M) (h : l ≠ []) : l.headI + l.tail.sum = l.sum

Same as get?_zero_add_tail_sum, but avoiding the List.headI garbage complication by requiring the list to be nonempty.

theorem Commute.list_prod_right {M : Type u_4} [Monoid M] (l : List M) (y : M) (h : ∀ (x : M), x ∈ l → Commute y x) : Commute y l.prod

theorem AddCommute.list_sum_right {M : Type u_4} [AddMonoid M] (l : List M) (y : M) (h : ∀ (x : M), x ∈ l → AddCommute y x) : AddCommute y l.sum

theorem Commute.list_prod_left {M : Type u_4} [Monoid M] (l : List M) (y : M) (h : ∀ (x : M), x ∈ l → Commute x y) : Commute l.prod y

theorem AddCommute.list_sum_left {M : Type u_4} [AddMonoid M] (l : List M) (y : M) (h : ∀ (x : M), x ∈ l → AddCommute x y) : AddCommute l.sum y

theorem List.prod_range_succ {M : Type u_4} [Monoid M] (f : ℕ → M) (n : ℕ) : (map f (range n.succ)).prod = (map f (range n)).prod * f n

theorem List.sum_range_succ {M : Type u_4} [AddMonoid M] (f : ℕ → M) (n : ℕ) : (map f (range n.succ)).sum = (map f (range n)).sum + f n

theorem List.prod_range_succ' {M : Type u_4} [Monoid M] (f : ℕ → M) (n : ℕ) : (map f (range n.succ)).prod = f 0 * (map (fun (i : ℕ) => f i.succ) (range n)).prod

A variant of prod_range_succ which pulls off the first term in the product rather than the last.

theorem List.sum_range_succ' {M : Type u_4} [AddMonoid M] (f : ℕ → M) (n : ℕ) : (map f (range n.succ)).sum = f 0 + (map (fun (i : ℕ) => f i.succ) (range n)).sum

A variant of sum_range_succ which pulls off the first term in the sum rather than the last.

theorem List.prod_eq_one {M : Type u_4} [Monoid M] {l : List M} (hl : ∀ (x : M), x ∈ l → x = 1) : l.prod = 1

theorem List.sum_eq_zero {M : Type u_4} [AddMonoid M] {l : List M} (hl : ∀ (x : M), x ∈ l → x = 0) : l.sum = 0

theorem List.exists_mem_ne_one_of_prod_ne_one {M : Type u_4} [Monoid M] {l : List M} (h : l.prod ≠ 1) : ∃ (x : M), x ∈ l ∧ x ≠ 1

theorem List.exists_mem_ne_zero_of_sum_ne_zero {M : Type u_4} [AddMonoid M] {l : List M} (h : l.sum ≠ 0) : ∃ (x : M), x ∈ l ∧ x ≠ 0

theorem List.prod_erase_of_comm {M : Type u_4} [Monoid M] {l : List M} {a : M} [DecidableEq M] (ha : a ∈ l) (comm : ∀ (x : M), x ∈ l → ∀ (y : M), y ∈ l → x * y = y * x) : a * (l.erase a).prod = l.prod

theorem List.sum_erase_of_comm {M : Type u_4} [AddMonoid M] {l : List M} {a : M} [DecidableEq M] (ha : a ∈ l) (comm : ∀ (x : M), x ∈ l → ∀ (y : M), y ∈ l → x + y = y + x) : a + (l.erase a).sum = l.sum

theorem List.prod_map_eq_pow_single {α : Type u_2} {M : Type u_4} [Monoid M] [DecidableEq α] {l : List α} (a : α) (f : α → M) (hf : ∀ (a' : α), a' ≠ a → a' ∈ l → f a' = 1) : (map f l).prod = f a ^ count a l

theorem List.sum_map_eq_nsmul_single {α : Type u_2} {M : Type u_4} [AddMonoid M] [DecidableEq α] {l : List α} (a : α) (f : α → M) (hf : ∀ (a' : α), a' ≠ a → a' ∈ l → f a' = 0) : (map f l).sum = count a l • f a

theorem List.prod_eq_pow_single {M : Type u_4} [Monoid M] {l : List M} [DecidableEq M] (a : M) (h : ∀ (a' : M), a' ≠ a → a' ∈ l → a' = 1) : l.prod = a ^ count a l

theorem List.sum_eq_nsmul_single {M : Type u_4} [AddMonoid M] {l : List M} [DecidableEq M] (a : M) (h : ∀ (a' : M), a' ≠ a → a' ∈ l → a' = 0) : l.sum = count a l • a

@[simp]

theorem List.prod_erase {M : Type u_4} [CommMonoid M] {a : M} {l : List M} [DecidableEq M] (ha : a ∈ l) : a * (l.erase a).prod = l.prod

@[simp]

theorem List.sum_erase {M : Type u_4} [AddCommMonoid M] {a : M} {l : List M} [DecidableEq M] (ha : a ∈ l) : a + (l.erase a).sum = l.sum

@[simp]

theorem List.prod_map_erase {α : Type u_2} {M : Type u_4} [CommMonoid M] [DecidableEq α] (f : α → M) {a : α} {l : List α} : a ∈ l → f a * (map f (l.erase a)).prod = (map f l).prod

@[simp]

theorem List.sum_map_erase {α : Type u_2} {M : Type u_4} [AddCommMonoid M] [DecidableEq α] (f : α → M) {a : α} {l : List α} : a ∈ l → f a + (map f (l.erase a)).sum = (map f l).sum

theorem List.Perm.prod_eq {M : Type u_4} [CommMonoid M] {l₁ l₂ : List M} (h : l₁.Perm l₂) : l₁.prod = l₂.prod

theorem List.Perm.sum_eq {M : Type u_4} [AddCommMonoid M] {l₁ l₂ : List M} (h : l₁.Perm l₂) : l₁.sum = l₂.sum

@[simp]

theorem List.prod_reverse {M : Type u_4} [CommMonoid M] (l : List M) : l.reverse.prod = l.prod

@[simp]

theorem List.sum_reverse {M : Type u_4} [AddCommMonoid M] (l : List M) : l.reverse.sum = l.sum

theorem List.prod_mul_prod_eq_prod_zipWith_mul_prod_drop {M : Type u_4} [CommMonoid M] (l l' : List M) : l.prod * l'.prod = (zipWith (fun (x1 x2 : M) => x1 * x2) l l').prod * (drop l'.length l).prod * (drop l.length l').prod

theorem List.sum_add_sum_eq_sum_zipWith_add_sum_drop {M : Type u_4} [AddCommMonoid M] (l l' : List M) : l.sum + l'.sum = (zipWith (fun (x1 x2 : M) => x1 + x2) l l').sum + (drop l'.length l).sum + (drop l.length l').sum

theorem List.prod_mul_prod_eq_prod_zipWith_of_length_eq {M : Type u_4} [CommMonoid M] (l l' : List M) (h : l.length = l'.length) : l.prod * l'.prod = (zipWith (fun (x1 x2 : M) => x1 * x2) l l').prod

theorem List.sum_add_sum_eq_sum_zipWith_of_length_eq {M : Type u_4} [AddCommMonoid M] (l l' : List M) (h : l.length = l'.length) : l.sum + l'.sum = (zipWith (fun (x1 x2 : M) => x1 + x2) l l').sum

theorem List.prod_map_ite {α : Type u_2} {M : Type u_4} [CommMonoid M] (p : α → Prop) [DecidablePred p] (f g : α → M) (l : List α) : (map (fun (a : α) => if p a then f a else g a) l).prod = (map f (filter (fun (b : α) => decide (p b)) l)).prod * (map g (filter (fun (a : α) => decide ¬p a) l)).prod

theorem List.sum_map_ite {α : Type u_2} {M : Type u_4} [AddCommMonoid M] (p : α → Prop) [DecidablePred p] (f g : α → M) (l : List α) : (map (fun (a : α) => if p a then f a else g a) l).sum = (map f (filter (fun (b : α) => decide (p b)) l)).sum + (map g (filter (fun (a : α) => decide ¬p a) l)).sum

theorem List.prod_map_filter_mul_prod_map_filter_not {α : Type u_2} {M : Type u_4} [CommMonoid M] (p : α → Prop) [DecidablePred p] (f : α → M) (l : List α) : (map f (filter (fun (b : α) => decide (p b)) l)).prod * (map f (filter (fun (x : α) => decide ¬p x) l)).prod = (map f l).prod

theorem List.sum_map_filter_add_sum_map_filter_not {α : Type u_2} {M : Type u_4} [AddCommMonoid M] (p : α → Prop) [DecidablePred p] (f : α → M) (l : List α) : (map f (filter (fun (b : α) => decide (p b)) l)).sum + (map f (filter (fun (x : α) => decide ¬p x) l)).sum = (map f l).sum

theorem List.eq_of_prod_take_eq {M : Type u_4} [LeftCancelMonoid M] {L L' : List M} (h : L.length = L'.length) (h' : ∀ (i : ℕ), i ≤ L.length → (take i L).prod = (take i L').prod) : L = L'

theorem List.eq_of_sum_take_eq {M : Type u_4} [AddLeftCancelMonoid M] {L L' : List M} (h : L.length = L'.length) (h' : ∀ (i : ℕ), i ≤ L.length → (take i L).sum = (take i L').sum) : L = L'

theorem List.prod_inv_reverse {G : Type u_7} [Group G] (L : List G) : L.prod⁻¹ = (map (fun (x : G) => x⁻¹) L).reverse.prod

This is the List.prod version of mul_inv_rev

theorem List.sum_neg_reverse {G : Type u_7} [AddGroup G] (L : List G) : -L.sum = (map (fun (x : G) => -x) L).reverse.sum

This is the List.sum version of add_neg_rev

theorem List.prod_reverse_noncomm {G : Type u_7} [Group G] (L : List G) : L.reverse.prod = (map (fun (x : G) => x⁻¹) L).prod⁻¹

A non-commutative variant of List.prod_reverse

theorem List.sum_reverse_noncomm {G : Type u_7} [AddGroup G] (L : List G) : L.reverse.sum = -(map (fun (x : G) => -x) L).sum

A non-commutative variant of List.sum_reverse

@[simp]

theorem List.prod_drop_succ {G : Type u_7} [Group G] (L : List G) (i : ℕ) (p : i < L.length) : (drop (i + 1) L).prod = L[i]⁻¹ * (drop i L).prod

Counterpart to List.prod_take_succ when we have an inverse operation

@[simp]

theorem List.sum_drop_succ {G : Type u_7} [AddGroup G] (L : List G) (i : ℕ) (p : i < L.length) : (drop (i + 1) L).sum = -L[i] + (drop i L).sum

Counterpart to List.sum_take_succ when we have a negation operation

theorem List.prod_range_div' {G : Type u_7} [Group G] (n : ℕ) (f : ℕ → G) : (map (fun (k : ℕ) => f k / f (k + 1)) (range n)).prod = f 0 / f n

Cancellation of a telescoping product.

theorem List.sum_range_sub' {G : Type u_7} [AddGroup G] (n : ℕ) (f : ℕ → G) : (map (fun (k : ℕ) => f k - f (k + 1)) (range n)).sum = f 0 - f n

Cancellation of a telescoping sum.

theorem List.prod_inv {K : Type u_8} [DivisionCommMonoid K] (L : List K) : L.prod⁻¹ = (map (fun (x : K) => x⁻¹) L).prod

This is the List.prod version of mul_inv

theorem List.sum_neg {K : Type u_8} [SubtractionCommMonoid K] (L : List K) : -L.sum = (map (fun (x : K) => -x) L).sum

This is the List.sum version of add_neg

theorem List.prod_range_div {G : Type u_7} [CommGroup G] (n : ℕ) (f : ℕ → G) : (map (fun (k : ℕ) => f (k + 1) / f k) (range n)).prod = f n / f 0

Cancellation of a telescoping product.

theorem List.sum_range_sub {G : Type u_7} [AddCommGroup G] (n : ℕ) (f : ℕ → G) : (map (fun (k : ℕ) => f (k + 1) - f k) (range n)).sum = f n - f 0

Cancellation of a telescoping sum.

theorem List.prod_set' {G : Type u_7} [CommGroup G] (L : List G) (n : ℕ) (a : G) : (L.set n a).prod = L.prod * if hn : n < L.length then L[n]⁻¹ * a else 1

Alternative version of List.prod_set when the list is over a group

theorem List.sum_set' {G : Type u_7} [AddCommGroup G] (L : List G) (n : ℕ) (a : G) : (L.set n a).sum = L.sum + if hn : n < L.length then -L[n] + a else 0

Alternative version of List.sum_set when the list is over a group

theorem List.prod_map_ite_eq {G : Type u_7} [CommGroup G] {A : Type u_8} [DecidableEq A] (l : List A) (f g : A → G) (a : A) : (map (fun (x : A) => if x = a then f x else g x) l).prod = (f a / g a) ^ count a l * (map g l).prod

theorem List.sum_map_ite_eq {G : Type u_7} [AddCommGroup G] {A : Type u_8} [DecidableEq A] (l : List A) (f g : A → G) (a : A) : (map (fun (x : A) => if x = a then f x else g x) l).sum = count a l • (f a - g a) + (map g l).sum

theorem List.sum_const_nat (m n : ℕ) : (replicate m n).sum = m * n

Several lemmas about sum/head/tail for List ℕ. These are hard to generalize well, as they rely on the fact that default ℕ = 0. If desired, we could add a class stating that default = 0.

theorem List.headI_add_tail_sum (L : List ℕ) : L.headI + L.tail.sum = L.sum

This relies on default ℕ = 0.

theorem List.headI_le_sum (L : List ℕ) : L.headI ≤ L.sum

This relies on default ℕ = 0.

theorem List.tail_sum (L : List ℕ) : L.tail.sum = L.sum - L.headI

This relies on default ℕ = 0.

@[simp]

theorem List.alternatingProd_nil {G : Type u_7} [One G] [Mul G] [Inv G] : [].alternatingProd = 1

@[simp]

theorem List.alternatingSum_nil {G : Type u_7} [Zero G] [Add G] [Neg G] : [].alternatingSum = 0

@[simp]

theorem List.alternatingProd_singleton {G : Type u_7} [One G] [Mul G] [Inv G] (a : G) : [a].alternatingProd = a

@[simp]

theorem List.alternatingSum_singleton {G : Type u_7} [Zero G] [Add G] [Neg G] (a : G) : [a].alternatingSum = a

theorem List.alternatingProd_cons_cons' {G : Type u_7} [One G] [Mul G] [Inv G] (a b : G) (l : List G) : (a :: b :: l).alternatingProd = a * b⁻¹ * l.alternatingProd

theorem List.alternatingSum_cons_cons' {G : Type u_7} [Zero G] [Add G] [Neg G] (a b : G) (l : List G) : (a :: b :: l).alternatingSum = a + -b + l.alternatingSum

theorem List.alternatingProd_cons_cons {G : Type u_7} [DivInvMonoid G] (a b : G) (l : List G) : (a :: b :: l).alternatingProd = a / b * l.alternatingProd

theorem List.alternatingSum_cons_cons {G : Type u_7} [SubNegMonoid G] (a b : G) (l : List G) : (a :: b :: l).alternatingSum = a - b + l.alternatingSum

theorem List.alternatingProd_cons' {G : Type u_7} [CommGroup G] (a : G) (l : List G) : (a :: l).alternatingProd = a * l.alternatingProd⁻¹

theorem List.alternatingSum_cons' {G : Type u_7} [AddCommGroup G] (a : G) (l : List G) : (a :: l).alternatingSum = a + -l.alternatingSum

@[simp]

theorem List.alternatingProd_cons {G : Type u_7} [CommGroup G] (a : G) (l : List G) : (a :: l).alternatingProd = a / l.alternatingProd

@[simp]

theorem List.alternatingSum_cons {G : Type u_7} [AddCommGroup G] (a : G) (l : List G) : (a :: l).alternatingSum = a - l.alternatingSum

theorem List.sum_nat_mod (l : List ℕ) (n : ℕ) : l.sum % n = (map (fun (x : ℕ) => x % n) l).sum % n

theorem List.prod_nat_mod (l : List ℕ) (n : ℕ) : l.prod % n = (map (fun (x : ℕ) => x % n) l).prod % n

theorem List.sum_int_mod (l : List ℤ) (n : ℤ) : l.sum % n = (map (fun (x : ℤ) => x % n) l).sum % n

theorem List.prod_int_mod (l : List ℤ) (n : ℤ) : l.prod % n = (map (fun (x : ℤ) => x % n) l).prod % n

theorem 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) : f l.prod = (List.map (⇑f) l).prod

theorem map_list_sum {M : Type u_4} {N : Type u_5} [AddMonoid M] [AddMonoid N] {F : Type u_8} [FunLike F M N] [AddMonoidHomClass F M N] (f : F) (l : List M) : f l.sum = (List.map (⇑f) l).sum

theorem MonoidHom.map_list_prod {M : Type u_4} {N : Type u_5} [Monoid M] [Monoid N] (f : M →* N) (l : List M) : f l.prod = (List.map (⇑f) l).prod

theorem AddMonoidHom.map_list_sum {M : Type u_4} {N : Type u_5} [AddMonoid M] [AddMonoid N] (f : M →+ N) (l : List M) : f l.sum = (List.map (⇑f) l).sum

theorem List.prod_zpow {β : Type u_8} [DivisionCommMonoid β] {r : ℤ} {l : List β} : l.prod ^ r = (map (fun (x : β) => x ^ r) l).prod

theorem List.take_sum_flatten {α : Type u_2} (L : List (List α)) (i : ℕ) : take (take i (map length L)).sum L.flatten = (take i L).flatten

In a flatten, taking the first elements up to an index which is the sum of the lengths of the first i sublists, is the same as taking the flatten of the first i sublists.

theorem List.drop_sum_flatten {α : Type u_2} (L : List (List α)) (i : ℕ) : drop (take i (map length L)).sum L.flatten = (drop i L).flatten

In a flatten, dropping all the elements up to an index which is the sum of the lengths of the first i sublists, is the same as taking the join after dropping the first i sublists.

theorem List.length_le_sum_of_one_le (L : List ℕ) (h : ∀ (i : ℕ), i ∈ L → 1 ≤ i) : L.length ≤ L.sum

If all elements in a list are bounded below by 1, then the length of the list is bounded by the sum of the elements.