mathlib documentation

data.list.big_operators

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.alternating_prod, list.alternating_sum, their alternating counterparts. These are defined in data.list.defs.

@[simp]
theorem list.sum_nil {M : Type u_3} [add_monoid M] :
@[simp]
theorem list.prod_nil {M : Type u_3} [monoid M] :
theorem list.sum_singleton {M : Type u_3} [add_monoid M] {a : M} :
[a].sum = a
theorem list.prod_singleton {M : Type u_3} [monoid M] {a : M} :
[a].prod = a
@[simp]
theorem list.sum_cons {M : Type u_3} [add_monoid M] {l : list M} {a : M} :
(a :: l).sum = a + l.sum
@[simp]
theorem list.prod_cons {M : Type u_3} [monoid M] {l : list M} {a : M} :
(a :: l).prod = a * l.prod
@[simp]
theorem list.prod_append {M : Type u_3} [monoid M] {l₁ l₂ : list M} :
(l₁ ++ l₂).prod = l₁.prod * l₂.prod
@[simp]
theorem list.sum_append {M : Type u_3} [add_monoid M] {l₁ l₂ : list M} :
(l₁ ++ l₂).sum = l₁.sum + l₂.sum
theorem list.sum_concat {M : Type u_3} [add_monoid M] {l : list M} {a : M} :
(l.concat a).sum = l.sum + a
theorem list.prod_concat {M : Type u_3} [monoid M] {l : list M} {a : M} :
(l.concat a).prod = l.prod * a
@[simp]
theorem list.sum_join {M : Type u_3} [add_monoid M] {l : list (list M)} :
@[simp]
theorem list.prod_join {M : Type u_3} [monoid M] {l : list (list M)} :
theorem list.sum_eq_foldr {M : Type u_3} [add_monoid M] {l : list M} :
theorem list.prod_eq_foldr {M : Type u_3} [monoid M] {l : list M} :
@[simp]
theorem list.prod_repeat {M : Type u_3} [monoid M] (a : M) (n : ) :
(list.repeat a n).prod = a ^ n
@[simp]
theorem list.sum_repeat {M : Type u_3} [add_monoid M] (a : M) (n : ) :
(list.repeat a n).sum = n a
theorem list.prod_eq_pow_card {M : Type u_3} [monoid M] (l : list M) (m : M) (h : ∀ (x : M), x lx = m) :
l.prod = m ^ l.length
theorem list.sum_eq_card_nsmul {M : Type u_3} [add_monoid M] (l : list M) (m : M) (h : ∀ (x : M), x lx = m) :
l.sum = l.length m
theorem list.prod_hom_rel {ι : Type u_1} {M : Type u_3} {N : Type u_4} [monoid M] [monoid N] (l : list ι) {r : M → N → Prop} {f : ι → M} {g : ι → N} (h₁ : r 1 1) (h₂ : ∀ ⦃i : ι⦄ ⦃a : M⦄ ⦃b : N⦄, r a br (f i * a) (g i * b)) :
r (list.map f l).prod (list.map g l).prod
theorem list.sum_hom_rel {ι : Type u_1} {M : Type u_3} {N : Type u_4} [add_monoid M] [add_monoid N] (l : list ι) {r : M → N → Prop} {f : ι → M} {g : ι → N} (h₁ : r 0 0) (h₂ : ∀ ⦃i : ι⦄ ⦃a : M⦄ ⦃b : N⦄, r a br (f i + a) (g i + b)) :
r (list.map f l).sum (list.map g l).sum
theorem list.sum_hom {M : Type u_3} {N : Type u_4} [add_monoid M] [add_monoid N] (l : list M) {F : Type u_1} [add_monoid_hom_class F M N] (f : F) :
theorem list.prod_hom {M : Type u_3} {N : Type u_4} [monoid M] [monoid N] (l : list M) {F : Type u_1} [monoid_hom_class F M N] (f : F) :
theorem list.prod_hom₂ {ι : Type u_1} {M : Type u_3} {N : Type u_4} {P : Type u_5} [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) :
(list.map (λ (i : ι), f (f₁ i) (f₂ i)) l).prod = f (list.map f₁ l).prod (list.map f₂ l).prod
theorem list.sum_hom₂ {ι : Type u_1} {M : Type u_3} {N : Type u_4} {P : Type u_5} [add_monoid M] [add_monoid N] [add_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 0 0 = 0) (f₁ : ι → M) (f₂ : ι → N) :
(list.map (λ (i : ι), f (f₁ i) (f₂ i)) l).sum = f (list.map f₁ l).sum (list.map f₂ l).sum
@[simp]
theorem list.prod_map_mul {ι : Type u_1} {α : Type u_2} [comm_monoid α] {l : list ι} {f g : ι → α} :
(list.map (λ (i : ι), f i * g i) l).prod = (list.map f l).prod * (list.map g l).prod
@[simp]
theorem list.sum_map_add {ι : Type u_1} {α : Type u_2} [add_comm_monoid α] {l : list ι} {f g : ι → α} :
(list.map (λ (i : ι), f i + g i) l).sum = (list.map f l).sum + (list.map g l).sum
@[simp]
theorem list.prod_map_neg {α : Type u_1} [comm_monoid α] [has_distrib_neg α] (l : list α) :
theorem list.prod_map_hom {ι : Type u_1} {M : Type u_3} {N : Type u_4} [monoid M] [monoid N] (L : list ι) (f : ι → M) {G : Type u_2} [monoid_hom_class G M N] (g : G) :
(list.map (g f) L).prod = g (list.map f L).prod
theorem list.sum_map_hom {ι : Type u_1} {M : Type u_3} {N : Type u_4} [add_monoid M] [add_monoid N] (L : list ι) (f : ι → M) {G : Type u_2} [add_monoid_hom_class G M N] (g : G) :
(list.map (g f) L).sum = g (list.map f L).sum
theorem list.sum_is_add_unit {M : Type u_3} [add_monoid M] {L : list M} (u : ∀ (m : M), m Lis_add_unit m) :
theorem list.prod_is_unit {M : Type u_3} [monoid M] {L : list M} (u : ∀ (m : M), m Lis_unit m) :
@[simp]
theorem list.sum_take_add_sum_drop {M : Type u_3} [add_monoid M] (L : list M) (i : ) :
(list.take i L).sum + (list.drop i L).sum = L.sum
@[simp]
theorem list.prod_take_mul_prod_drop {M : Type u_3} [monoid M] (L : list M) (i : ) :
@[simp]
theorem list.sum_take_succ {M : Type u_3} [add_monoid M] (L : list M) (i : ) (p : i < L.length) :
(list.take (i + 1) L).sum = (list.take i L).sum + L.nth_le i p
@[simp]
theorem list.prod_take_succ {M : Type u_3} [monoid M] (L : list M) (i : ) (p : i < L.length) :
(list.take (i + 1) L).prod = (list.take i L).prod * L.nth_le i p
theorem list.length_pos_of_prod_ne_one {M : Type u_3} [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_3} [add_monoid 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_3} [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_3} [add_monoid 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_3} [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_3} [add_monoid 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_update_nth {M : Type u_3} [monoid M] (L : list M) (n : ) (a : M) :
(L.update_nth n a).prod = (list.take n L).prod * ite (n < L.length) a 1 * (list.drop (n + 1) L).prod
theorem list.sum_update_nth {M : Type u_3} [add_monoid M] (L : list M) (n : ) (a : M) :
(L.update_nth n a).sum = (list.take n L).sum + ite (n < L.length) a 0 + (list.drop (n + 1) L).sum
theorem list.nth_zero_add_tail_sum {M : Type u_3} [add_monoid M] (l : list M) :
(l.nth 0).get_or_else 0 + l.tail.sum = l.sum

We'd like to state this as L.head + L.tail.sum = L.sum, but because L.head 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.nth 0).get_or_else 0.

theorem list.nth_zero_mul_tail_prod {M : Type u_3} [monoid M] (l : list M) :

We'd like to state this as L.head * L.tail.prod = L.prod, but because L.head 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.nth 0).get_or_else 1.

theorem list.head_add_tail_sum_of_ne_nil {M : Type u_3} [add_monoid M] [inhabited M] (l : list M) (h : l list.nil) :
l.head + l.tail.sum = l.sum

Same as nth_zero_add_tail_sum, but avoiding the list.head garbage complication by requiring the list to be nonempty.

theorem list.head_mul_tail_prod_of_ne_nil {M : Type u_3} [monoid M] [inhabited M] (l : list M) (h : l list.nil) :

Same as nth_zero_mul_tail_prod, but avoiding the list.head garbage complication by requiring the list to be nonempty.

theorem add_commute.list_sum_right {M : Type u_3} [add_monoid M] (l : list M) (y : M) (h : ∀ (x : M), x ladd_commute y x) :
theorem commute.list_prod_right {M : Type u_3} [monoid M] (l : list M) (y : M) (h : ∀ (x : M), x lcommute y x) :
theorem add_commute.list_sum_left {M : Type u_3} [add_monoid M] (l : list M) (y : M) (h : ∀ (x : M), x ladd_commute x y) :
theorem commute.list_prod_left {M : Type u_3} [monoid M] (l : list M) (y : M) (h : ∀ (x : M), x lcommute x y) :
theorem commute.list_sum_right {R : Type u_8} [non_unital_non_assoc_semiring R] (a : R) (l : list R) (h : ∀ (b : R), b lcommute a b) :
theorem commute.list_sum_left {R : Type u_8} [non_unital_non_assoc_semiring R] (b : R) (l : list R) (h : ∀ (a : R), a lcommute a b) :
theorem list.sublist.sum_le_sum {M : Type u_3} [add_monoid M] [preorder M] [covariant_class M M (function.swap has_add.add) has_le.le] [covariant_class M M has_add.add has_le.le] {l₁ l₂ : list M} (h : l₁ <+ l₂) (h₁ : ∀ (a : M), a l₂0 a) :
l₁.sum l₂.sum

If l₁ is a sublist of l₂ and all elements of l₂ are nonnegative, then l₁.sum ≤ l₂.sum. One can prove a stronger version assuming ∀ a ∈ l₂.diff l₁, 0 ≤ a instead of ∀ a ∈ l₂, 0 ≤ a but this lemma is not yet in mathlib.

theorem list.sublist.prod_le_prod' {M : Type u_3} [monoid M] [preorder M] [covariant_class M M (function.swap has_mul.mul) has_le.le] [covariant_class M M has_mul.mul has_le.le] {l₁ l₂ : list M} (h : l₁ <+ l₂) (h₁ : ∀ (a : M), a l₂1 a) :
l₁.prod l₂.prod

If l₁ is a sublist of l₂ and all elements of l₂ are greater than or equal to one, then l₁.prod ≤ l₂.prod. One can prove a stronger version assuming ∀ a ∈ l₂.diff l₁, 1 ≤ a instead of ∀ a ∈ l₂, 1 ≤ a but this lemma is not yet in mathlib.

theorem list.sublist_forall₂.sum_le_sum {M : Type u_3} [add_monoid M] [preorder M] [covariant_class M M (function.swap has_add.add) has_le.le] [covariant_class M M has_add.add has_le.le] {l₁ l₂ : list M} (h : list.sublist_forall₂ has_le.le l₁ l₂) (h₁ : ∀ (a : M), a l₂0 a) :
l₁.sum l₂.sum
theorem list.sublist_forall₂.prod_le_prod' {M : Type u_3} [monoid M] [preorder M] [covariant_class M M (function.swap has_mul.mul) has_le.le] [covariant_class M M has_mul.mul has_le.le] {l₁ l₂ : list M} (h : list.sublist_forall₂ has_le.le l₁ l₂) (h₁ : ∀ (a : M), a l₂1 a) :
l₁.prod l₂.prod
theorem list.sum_le_sum {ι : Type u_1} {M : Type u_3} [add_monoid M] [preorder M] [covariant_class M M (function.swap has_add.add) has_le.le] [covariant_class M M has_add.add has_le.le] {l : list ι} {f g : ι → M} (h : ∀ (i : ι), i lf i g i) :
theorem list.prod_le_prod' {ι : Type u_1} {M : Type u_3} [monoid M] [preorder M] [covariant_class M M (function.swap has_mul.mul) has_le.le] [covariant_class M M has_mul.mul has_le.le] {l : list ι} {f g : ι → M} (h : ∀ (i : ι), i lf i g i) :
theorem list.prod_lt_prod' {ι : Type u_1} {M : Type u_3} [monoid M] [preorder M] [covariant_class M M has_mul.mul has_lt.lt] [covariant_class M M has_mul.mul has_le.le] [covariant_class M M (function.swap has_mul.mul) has_lt.lt] [covariant_class M M (function.swap has_mul.mul) has_le.le] {l : list ι} (f g : ι → M) (h₁ : ∀ (i : ι), i lf i g i) (h₂ : ∃ (i : ι) (H : i l), f i < g i) :
theorem list.sum_lt_sum {ι : Type u_1} {M : Type u_3} [add_monoid M] [preorder M] [covariant_class M M has_add.add has_lt.lt] [covariant_class M M has_add.add has_le.le] [covariant_class M M (function.swap has_add.add) has_lt.lt] [covariant_class M M (function.swap has_add.add) has_le.le] {l : list ι} (f g : ι → M) (h₁ : ∀ (i : ι), i lf i g i) (h₂ : ∃ (i : ι) (H : i l), f i < g i) :
(list.map f l).sum < (list.map g l).sum
theorem list.sum_lt_sum_of_ne_nil {ι : Type u_1} {M : Type u_3} [add_monoid M] [preorder M] [covariant_class M M has_add.add has_lt.lt] [covariant_class M M has_add.add has_le.le] [covariant_class M M (function.swap has_add.add) has_lt.lt] [covariant_class M M (function.swap has_add.add) has_le.le] {l : list ι} (hl : l list.nil) (f g : ι → M) (hlt : ∀ (i : ι), i lf i < g i) :
(list.map f l).sum < (list.map g l).sum
theorem list.prod_lt_prod_of_ne_nil {ι : Type u_1} {M : Type u_3} [monoid M] [preorder M] [covariant_class M M has_mul.mul has_lt.lt] [covariant_class M M has_mul.mul has_le.le] [covariant_class M M (function.swap has_mul.mul) has_lt.lt] [covariant_class M M (function.swap has_mul.mul) has_le.le] {l : list ι} (hl : l list.nil) (f g : ι → M) (hlt : ∀ (i : ι), i lf i < g i) :
theorem list.prod_le_pow_card {M : Type u_3} [monoid M] [preorder M] [covariant_class M M (function.swap has_mul.mul) has_le.le] [covariant_class M M has_mul.mul has_le.le] (l : list M) (n : M) (h : ∀ (x : M), x lx n) :
theorem list.sum_le_card_nsmul {M : Type u_3} [add_monoid M] [preorder M] [covariant_class M M (function.swap has_add.add) has_le.le] [covariant_class M M has_add.add has_le.le] (l : list M) (n : M) (h : ∀ (x : M), x lx n) :
theorem list.pow_card_le_prod {M : Type u_3} [monoid M] [preorder M] [covariant_class M M (function.swap has_mul.mul) has_le.le] [covariant_class M M has_mul.mul has_le.le] (l : list M) (n : M) (h : ∀ (x : M), x ln x) :
theorem list.card_nsmul_le_sum {M : Type u_3} [add_monoid M] [preorder M] [covariant_class M M (function.swap has_add.add) has_le.le] [covariant_class M M has_add.add has_le.le] (l : list M) (n : M) (h : ∀ (x : M), x ln x) :
theorem list.exists_lt_of_prod_lt' {ι : Type u_1} {M : Type u_3} [monoid M] [linear_order M] [covariant_class M M (function.swap has_mul.mul) has_le.le] [covariant_class M M has_mul.mul has_le.le] {l : list ι} (f g : ι → M) (h : (list.map f l).prod < (list.map g l).prod) :
∃ (i : ι) (H : i l), f i < g i
theorem list.exists_lt_of_sum_lt {ι : Type u_1} {M : Type u_3} [add_monoid M] [linear_order M] [covariant_class M M (function.swap has_add.add) has_le.le] [covariant_class M M has_add.add has_le.le] {l : list ι} (f g : ι → M) (h : (list.map f l).sum < (list.map g l).sum) :
∃ (i : ι) (H : i l), f i < g i
theorem list.exists_le_of_sum_le {ι : Type u_1} {M : Type u_3} [add_monoid M] [linear_order M] [covariant_class M M has_add.add has_lt.lt] [covariant_class M M has_add.add has_le.le] [covariant_class M M (function.swap has_add.add) has_lt.lt] [covariant_class M M (function.swap has_add.add) has_le.le] {l : list ι} (hl : l list.nil) (f g : ι → M) (h : (list.map f l).sum (list.map g l).sum) :
∃ (x : ι) (H : x l), f x g x
theorem list.exists_le_of_prod_le' {ι : Type u_1} {M : Type u_3} [monoid M] [linear_order M] [covariant_class M M has_mul.mul has_lt.lt] [covariant_class M M has_mul.mul has_le.le] [covariant_class M M (function.swap has_mul.mul) has_lt.lt] [covariant_class M M (function.swap has_mul.mul) has_le.le] {l : list ι} (hl : l list.nil) (f g : ι → M) (h : (list.map f l).prod (list.map g l).prod) :
∃ (x : ι) (H : x l), f x g x
theorem list.sum_nonneg {M : Type u_3} [add_monoid M] [preorder M] [covariant_class M M has_add.add has_le.le] {l : list M} (hl₁ : ∀ (x : M), x l0 x) :
0 l.sum
theorem list.one_le_prod_of_one_le {M : Type u_3} [monoid M] [preorder M] [covariant_class M M has_mul.mul has_le.le] {l : list M} (hl₁ : ∀ (x : M), x l1 x) :
1 l.prod
theorem list.prod_eq_zero {M₀ : Type u_6} [monoid_with_zero M₀] {L : list M₀} (h : 0 L) :
L.prod = 0

If zero is an element of a list L, then list.prod L = 0. If the domain is a nontrivial monoid with zero with no divisors, then this implication becomes an iff, see list.prod_eq_zero_iff.

@[simp]
theorem list.prod_eq_zero_iff {M₀ : Type u_6} [monoid_with_zero M₀] [nontrivial M₀] [no_zero_divisors M₀] {L : list M₀} :
L.prod = 0 0 L

Product of elements of a list L equals zero if and only if 0 ∈ L. See also list.prod_eq_zero for an implication that needs weaker typeclass assumptions.

theorem list.prod_ne_zero {M₀ : Type u_6} [monoid_with_zero M₀] [nontrivial M₀] [no_zero_divisors M₀] {L : list M₀} (hL : 0 L) :
L.prod 0
theorem list.prod_inv_reverse {G : Type u_7} [group G] (L : list G) :
(L.prod)⁻¹ = (list.map (λ (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} [add_group G] (L : list G) :
-L.sum = (list.map (λ (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 = ((list.map (λ (x : G), x⁻¹) L).prod)⁻¹

A non-commutative variant of list.prod_reverse

theorem list.sum_reverse_noncomm {G : Type u_7} [add_group G] (L : list G) :
L.reverse.sum = -(list.map (λ (x : G), -x) L).sum

A non-commutative variant of list.sum_reverse

@[simp]
theorem list.sum_drop_succ {G : Type u_7} [add_group G] (L : list G) (i : ) (p : i < L.length) :
(list.drop (i + 1) L).sum = -L.nth_le i p + (list.drop i L).sum

Counterpart to list.sum_take_succ when we have an negation operation

@[simp]
theorem list.prod_drop_succ {G : Type u_7} [group G] (L : list G) (i : ) (p : i < L.length) :
(list.drop (i + 1) L).prod = (L.nth_le i p)⁻¹ * (list.drop i L).prod

Counterpart to list.prod_take_succ when we have an inverse operation

theorem list.sum_neg {G : Type u_7} [add_comm_group G] (L : list G) :
-L.sum = (list.map (λ (x : G), -x) L).sum

This is the list.sum version of add_neg

theorem list.prod_inv {G : Type u_7} [comm_group G] (L : list G) :
(L.prod)⁻¹ = (list.map (λ (x : G), x⁻¹) L).prod

This is the list.prod version of mul_inv

theorem list.prod_update_nth' {G : Type u_7} [comm_group G] (L : list G) (n : ) (a : G) :
(L.update_nth n a).prod = L.prod * dite (n < L.length) (λ (hn : n < L.length), (L.nth_le n hn)⁻¹ * a) (λ (hn : ¬n < L.length), 1)

Alternative version of list.prod_update_nth when the list is over a group

theorem list.sum_update_nth' {G : Type u_7} [add_comm_group G] (L : list G) (n : ) (a : G) :
(L.update_nth n a).sum = L.sum + dite (n < L.length) (λ (hn : n < L.length), -L.nth_le n hn + a) (λ (hn : ¬n < L.length), 0)

Alternative version of list.sum_update_nth when the list is over a group

theorem list.eq_of_sum_take_eq {M : Type u_3} [add_left_cancel_monoid M] {L L' : list M} (h : L.length = L'.length) (h' : ∀ (i : ), i L.length(list.take i L).sum = (list.take i L').sum) :
L = L'
theorem list.eq_of_prod_take_eq {M : Type u_3} [left_cancel_monoid M] {L L' : list M} (h : L.length = L'.length) (h' : ∀ (i : ), i L.length(list.take i L).prod = (list.take i L').prod) :
L = L'
theorem list.monotone_sum_take {M : Type u_3} [canonically_ordered_add_monoid M] (L : list M) :
monotone (λ (i : ), (list.take i L).sum)
theorem list.monotone_prod_take {M : Type u_3} [canonically_ordered_monoid M] (L : list M) :
monotone (λ (i : ), (list.take i L).prod)
theorem list.one_lt_prod_of_one_lt {M : Type u_3} [ordered_comm_monoid M] (l : list M) (hl : ∀ (x : M), x l1 < x) (hl₂ : l list.nil) :
1 < l.prod
theorem list.sum_pos {M : Type u_3} [ordered_add_comm_monoid M] (l : list M) (hl : ∀ (x : M), x l0 < x) (hl₂ : l list.nil) :
0 < l.sum
theorem list.single_le_sum {M : Type u_3} [ordered_add_comm_monoid M] {l : list M} (hl₁ : ∀ (x : M), x l0 x) (x : M) (H : x l) :
x l.sum
theorem list.single_le_prod {M : Type u_3} [ordered_comm_monoid M] {l : list M} (hl₁ : ∀ (x : M), x l1 x) (x : M) (H : x l) :
x l.prod
theorem list.all_zero_of_le_zero_le_of_sum_eq_zero {M : Type u_3} [ordered_add_comm_monoid M] {l : list M} (hl₁ : ∀ (x : M), x l0 x) (hl₂ : l.sum = 0) {x : M} (hx : x l) :
x = 0
theorem list.all_one_of_le_one_le_of_prod_eq_one {M : Type u_3} [ordered_comm_monoid M] {l : list M} (hl₁ : ∀ (x : M), x l1 x) (hl₂ : l.prod = 1) {x : M} (hx : x l) :
x = 1
theorem list.sum_eq_zero_iff {M : Type u_3} [canonically_ordered_add_monoid M] (l : list M) :
l.sum = 0 ∀ (x : M), x lx = 0
theorem list.prod_eq_one_iff {M : Type u_3} [canonically_ordered_monoid M] (l : list M) :
l.prod = 1 ∀ (x : M), x lx = 1
theorem list.sum_eq_zero {M : Type u_3} [add_monoid M] {l : list M} (hl : ∀ (x : M), x lx = 0) :
l.sum = 0

Slightly more general version of list.sum_eq_zero_iff for a non-ordered add_monoid

theorem list.prod_eq_one {M : Type u_3} [monoid M] {l : list M} (hl : ∀ (x : M), x lx = 1) :
l.prod = 1

Slightly more general version of list.prod_eq_one_iff for a non-ordered monoid

theorem list.length_le_sum_of_one_le (L : list ) (h : ∀ (i : ), i L1 i) :

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.

theorem list.sum_le_foldr_max {M : Type u_3} {N : Type u_4} [add_monoid M] [add_monoid N] [linear_order N] (f : M → N) (h0 : f 0 0) (hadd : ∀ (x y : M), f (x + y) linear_order.max (f x) (f y)) (l : list M) :
@[simp]
theorem list.sum_erase {M : Type u_3} [decidable_eq M] [add_comm_monoid M] {a : M} {l : list M} :
a la + (l.erase a).sum = l.sum
@[simp]
theorem list.prod_erase {M : Type u_3} [decidable_eq M] [comm_monoid M] {a : M} {l : list M} :
a la * (l.erase a).prod = l.prod
@[simp]
theorem list.prod_map_erase {ι : Type u_1} {M : Type u_3} [decidable_eq ι] [comm_monoid M] (f : ι → M) {a : ι} {l : list ι} :
a lf a * (list.map f (l.erase a)).prod = (list.map f l).prod
@[simp]
theorem list.sum_map_erase {ι : Type u_1} {M : Type u_3} [decidable_eq ι] [add_comm_monoid M] (f : ι → M) {a : ι} {l : list ι} :
a lf a + (list.map f (l.erase a)).sum = (list.map f l).sum
theorem list.dvd_prod {M : Type u_3} [comm_monoid M] {a : M} {l : list M} (ha : a l) :
a l.prod
@[simp]
theorem list.sum_const_nat (m n : ) :
(list.repeat m n).sum = m * n
theorem list.dvd_sum {R : Type u_8} [semiring R] {a : R} {l : list R} (h : ∀ (x : R), x la x) :
a l.sum
theorem list.prod_pos {R : Type u_8} [ordered_semiring R] [nontrivial R] (l : list R) (h : ∀ (a : R), a l0 < a) :
0 < l.prod

The product of a list of positive natural numbers is positive, and likewise for any nontrivial ordered semiring.

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.head_add_tail_sum (L : list ) :
L.head + L.tail.sum = L.sum

This relies on default ℕ = 0.

theorem list.head_le_sum (L : list ) :

This relies on default ℕ = 0.

theorem list.tail_sum (L : list ) :
L.tail.sum = L.sum - L.head

This relies on default ℕ = 0.

@[simp]
theorem list.alternating_sum_nil {α : Type u_2} [has_zero α] [has_add α] [has_neg α] :
@[simp]
theorem list.alternating_prod_nil {α : Type u_2} [has_one α] [has_mul α] [has_inv α] :
@[simp]
theorem list.alternating_prod_singleton {α : Type u_2} [has_one α] [has_mul α] [has_inv α] (a : α) :
@[simp]
theorem list.alternating_sum_singleton {α : Type u_2} [has_zero α] [has_add α] [has_neg α] (a : α) :
theorem list.alternating_prod_cons_cons' {α : Type u_2} [has_one α] [has_mul α] [has_inv α] (a b : α) (l : list α) :
theorem list.alternating_sum_cons_cons' {α : Type u_2} [has_zero α] [has_add α] [has_neg α] (a b : α) (l : list α) :
theorem list.alternating_prod_cons_cons {α : Type u_2} [div_inv_monoid α] (a b : α) (l : list α) :
theorem list.alternating_sum_cons_cons {α : Type u_2} [sub_neg_monoid α] (a b : α) (l : list α) :
theorem list.alternating_prod_cons' {α : Type u_2} [comm_group α] (a : α) (l : list α) :
theorem list.alternating_sum_cons' {α : Type u_2} [add_comm_group α] (a : α) (l : list α) :
@[simp]
theorem list.alternating_prod_cons {α : Type u_2} [comm_group α] (a : α) (l : list α) :
@[simp]
theorem list.alternating_sum_cons {α : Type u_2} [add_comm_group α] (a : α) (l : list α) :
theorem list.alternating_prod_append {α : Type u_2} [comm_group α] (l₁ l₂ : list α) :
(l₁ ++ l₂).alternating_prod = l₁.alternating_prod * l₂.alternating_prod ^ (-1) ^ l₁.length
theorem list.alternating_sum_append {α : Type u_2} [add_comm_group α] (l₁ l₂ : list α) :
(l₁ ++ l₂).alternating_sum = l₁.alternating_sum + (-1) ^ l₁.length l₂.alternating_sum
theorem list.alternating_prod_reverse {α : Type u_2} [comm_group α] (l : list α) :
theorem list.alternating_sum_reverse {α : Type u_2} [add_comm_group α] (l : list α) :
theorem list.sum_map_mul_left {ι : Type u_1} {R : Type u_8} [non_unital_non_assoc_semiring R] (L : list ι) (f : ι → R) (r : R) :
(list.map (λ (b : ι), r * f b) L).sum = r * (list.map f L).sum
theorem list.sum_map_mul_right {ι : Type u_1} {R : Type u_8} [non_unital_non_assoc_semiring R] (L : list ι) (f : ι → R) (r : R) :
(list.map (λ (b : ι), f b * r) L).sum = (list.map f L).sum * r
theorem map_list_sum {M : Type u_3} {N : Type u_4} [add_monoid M] [add_monoid N] {F : Type u_1} [add_monoid_hom_class F M N] (f : F) (l : list M) :
theorem map_list_prod {M : Type u_3} {N : Type u_4} [monoid M] [monoid N] {F : Type u_1} [monoid_hom_class F M N] (f : F) (l : list M) :
theorem unop_map_list_prod {M : Type u_3} {N : Type u_4} [monoid M] [monoid N] {F : Type u_1} [monoid_hom_class F M Nᵐᵒᵖ] (f : F) (l : list M) :

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

@[protected]
theorem monoid_hom.map_list_prod {M : Type u_3} {N : Type u_4} [monoid M] [monoid N] (f : M →* N) (l : list M) :

Deprecated, use _root_.map_list_prod instead.

@[protected]
theorem add_monoid_hom.map_list_sum {M : Type u_3} {N : Type u_4} [add_monoid M] [add_monoid N] (f : M →+ N) (l : list M) :

Deprecated, use _root_.map_list_sum instead.

@[protected]
theorem monoid_hom.unop_map_list_prod {M : Type u_3} {N : Type u_4} [monoid M] [monoid N] (f : M →* Nᵐᵒᵖ) (l : list M) :

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

Deprecated, use _root_.unop_map_list_prod instead.