# Documentation

Mathlib.Data.List.BigOperators.Basic

# 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} [] :
List.sum [] = 0
@[simp]
theorem List.prod_nil {M : Type u_3} [] :
= 1
theorem List.sum_singleton {M : Type u_3} [] {a : M} :
List.sum [a] = a
theorem List.prod_singleton {M : Type u_3} [] {a : M} :
List.prod [a] = a
@[simp]
theorem List.sum_cons {M : Type u_3} [] {l : List M} {a : M} :
List.sum (a :: l) = a +
@[simp]
theorem List.prod_cons {M : Type u_3} [] {l : List M} {a : M} :
List.prod (a :: l) = a *
@[simp]
theorem List.sum_append {M : Type u_3} [] {l₁ : List M} {l₂ : List M} :
List.sum (l₁ ++ l₂) = List.sum l₁ + List.sum l₂
@[simp]
theorem List.prod_append {M : Type u_3} [] {l₁ : List M} {l₂ : List M} :
List.prod (l₁ ++ l₂) = *
theorem List.sum_concat {M : Type u_3} [] {l : List M} {a : M} :
List.sum () = + a
theorem List.prod_concat {M : Type u_3} [] {l : List M} {a : M} :
@[simp]
theorem List.sum_join {M : Type u_3} [] {l : List (List M)} :
= List.sum (List.map List.sum l)
@[simp]
theorem List.prod_join {M : Type u_3} [] {l : List (List M)} :
= List.prod (List.map List.prod l)
abbrev List.sum_eq_foldr.match_1 {M : Type u_1} (motive : List MProp) :
(x : List M) → (Unitmotive []) → ((a : M) → (l : List M) → motive (a :: l)) → motive x
Instances For
theorem List.sum_eq_foldr {M : Type u_3} [] {l : List M} :
= List.foldr (fun x x_1 => x + x_1) 0 l
theorem List.prod_eq_foldr {M : Type u_3} [] {l : List M} :
= List.foldr (fun x x_1 => x * x_1) 1 l
@[simp]
theorem List.sum_replicate {M : Type u_3} [] (n : ) (a : M) :
List.sum () = n a
@[simp]
theorem List.prod_replicate {M : Type u_3} [] (n : ) (a : M) :
List.prod () = a ^ n
theorem List.sum_eq_card_nsmul {M : Type u_3} [] (l : List M) (m : M) (h : ∀ (x : M), x lx = m) :
= m
theorem List.prod_eq_pow_card {M : Type u_3} [] (l : List M) (m : M) (h : ∀ (x : M), x lx = m) :
= m ^
theorem List.sum_hom_rel {ι : Type u_1} {M : Type u_3} {N : Type u_4} [] [] (l : List ι) {r : MNProp} {f : ιM} {g : ιN} (h₁ : r 0 0) (h₂ : i : ι⦄ → a : M⦄ → b : N⦄ → r a br (f i + a) (g i + b)) :
theorem List.prod_hom_rel {ι : Type u_1} {M : Type u_3} {N : Type u_4} [] [] (l : List ι) {r : MNProp} {f : ιM} {g : ιN} (h₁ : r 1 1) (h₂ : i : ι⦄ → a : M⦄ → b : N⦄ → r a br (f i * a) (g i * b)) :
theorem List.sum_hom {M : Type u_3} {N : Type u_4} [] [] (l : List M) {F : Type u_9} [] (f : F) :
List.sum (List.map (f) l) = f ()
theorem List.prod_hom {M : Type u_3} {N : Type u_4} [] [] (l : List M) {F : Type u_9} [] (f : F) :
List.prod (List.map (f) l) = f ()
theorem List.sum_hom₂ {ι : Type u_1} {M : Type u_3} {N : Type u_4} {P : Type u_5} [] [] [] (l : List ι) (f : MNP) (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.sum (List.map (fun i => f (f₁ i) (f₂ i)) l) = f (List.sum (List.map f₁ l)) (List.sum (List.map f₂ l))
theorem List.prod_hom₂ {ι : Type u_1} {M : Type u_3} {N : Type u_4} {P : Type u_5} [] [] [] (l : List ι) (f : MNP) (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.prod (List.map (fun i => f (f₁ i) (f₂ i)) l) = f (List.prod (List.map f₁ l)) (List.prod (List.map f₂ l))
@[simp]
theorem List.sum_map_add {ι : Type u_1} {α : Type u_9} [] {l : List ι} {f : ια} {g : ια} :
List.sum (List.map (fun i => f i + g i) l) = List.sum (List.map f l) + List.sum (List.map g l)
@[simp]
theorem List.prod_map_mul {ι : Type u_1} {α : Type u_9} [] {l : List ι} {f : ια} {g : ια} :
List.prod (List.map (fun i => f i * g i) l) = List.prod (List.map f l) * List.prod (List.map g l)
@[simp]
theorem List.prod_map_neg {α : Type u_9} [] [] (l : List α) :
List.prod (List.map Neg.neg l) = (-1) ^ *
theorem List.sum_map_hom {ι : Type u_1} {M : Type u_3} {N : Type u_4} [] [] (L : List ι) (f : ιM) {G : Type u_9} [] (g : G) :
List.sum (List.map (g f) L) = g (List.sum (List.map f L))
theorem List.prod_map_hom {ι : Type u_1} {M : Type u_3} {N : Type u_4} [] [] (L : List ι) (f : ιM) {G : Type u_9} [] (g : G) :
List.prod (List.map (g f) L) = g (List.prod (List.map f L))
abbrev List.sum_isAddUnit.match_1 {M : Type u_1} [] (motive : (x : List M) → (∀ (m : M), m x) → Prop) :
(x : List M) → (x_1 : ∀ (m : M), m x) → ((x : ∀ (m : M), m []) → motive [] x) → ((h : M) → (t : List M) → (u : ∀ (m : M), m h :: t) → motive (h :: t) u) → motive x x_1
Instances For
theorem List.sum_isAddUnit {M : Type u_3} [] {L : List M} :
(∀ (m : M), m L) →
theorem List.prod_isUnit {M : Type u_3} [] {L : List M} :
(∀ (m : M), m L) → IsUnit ()
theorem List.sum_isAddUnit_iff {α : Type u_9} [] {L : List α} :
∀ (m : α), m L
theorem List.prod_isUnit_iff {α : Type u_9} [] {L : List α} :
IsUnit () ∀ (m : α), m L
abbrev List.sum_take_add_sum_drop.match_1 {M : Type u_1} (motive : List M) :
(x : List M) → (x_1 : ) → ((i : ) → motive [] i) → ((L : List M) → motive L 0) → ((h : M) → (t : List M) → (n : ) → motive (h :: t) ()) → motive x x_1
Instances For
@[simp]
theorem List.sum_take_add_sum_drop {M : Type u_3} [] (L : List M) (i : ) :
@[simp]
theorem List.prod_take_mul_prod_drop {M : Type u_3} [] (L : List M) (i : ) :
abbrev List.sum_take_succ.match_1 {M : Type u_1} (motive : (x : List M) → (x_1 : ) → x_1 < Prop) :
(x : List M) → (x_1 : ) → (x_2 : x_1 < ) → ((i : ) → (p : i < ) → motive [] i p) → ((h : M) → (t : List M) → (x : 0 < List.length (h :: t)) → motive (h :: t) 0 x) → ((h : M) → (t : List M) → (n : ) → (p : n + 1 < List.length (h :: t)) → motive (h :: t) () p) → motive x x_1 x_2
Instances For
@[simp]
theorem List.sum_take_succ {M : Type u_3} [] (L : List M) (i : ) (p : i < ) :
@[simp]
theorem List.prod_take_succ {M : Type u_3} [] (L : List M) (i : ) (p : i < ) :
theorem List.length_pos_of_sum_ne_zero {M : Type u_3} [] (L : List M) (h : 0) :
0 <

A list with sum not zero must have positive length.

theorem List.length_pos_of_prod_ne_one {M : Type u_3} [] (L : List M) (h : 1) :
0 <

A list with product not one must have positive length.

theorem List.length_pos_of_sum_pos {M : Type u_3} [] [] (L : List M) (h : 0 < ) :
0 <

A list with positive sum must have positive length.

theorem List.length_pos_of_one_lt_prod {M : Type u_3} [] [] (L : List M) (h : 1 < ) :
0 <

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

theorem List.length_pos_of_sum_neg {M : Type u_3} [] [] (L : List M) (h : < 0) :
0 <

A list with negative sum must have positive length.

theorem List.length_pos_of_prod_lt_one {M : Type u_3} [] [] (L : List M) (h : < 1) :
0 <

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

abbrev List.sum_set.match_1 {M : Type u_1} (motive : List MMProp) :
(x : List M) → (x_1 : ) → (x_2 : M) → ((x : M) → (xs : List M) → (a : M) → motive (x :: xs) 0 a) → ((x : M) → (xs : List M) → (i : ) → (a : M) → motive (x :: xs) () a) → ((x : ) → (x_3 : M) → motive [] x x_3) → motive x x_1 x_2
Instances For
theorem List.sum_set {M : Type u_3} [] (L : List M) (n : ) (a : M) :
List.sum (List.set L n a) = (List.sum () + if n < then a else 0) + List.sum (List.drop (n + 1) L)
theorem List.prod_set {M : Type u_3} [] (L : List M) (n : ) (a : M) :
List.prod (List.set L n a) = (List.prod () * if n < then a else 1) * List.prod (List.drop (n + 1) L)
theorem List.get?_zero_add_tail_sum {M : Type u_3} [] (l : List M) :

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.get? 0).getD 0.

theorem List.get?_zero_mul_tail_prod {M : Type u_3} [] (l : List M) :

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.get? 0).getD 1.

theorem List.headI_add_tail_sum_of_ne_nil {M : Type u_3} [] [] (l : List M) (h : l []) :
+ =

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

theorem List.headI_mul_tail_prod_of_ne_nil {M : Type u_3} [] [] (l : List M) (h : l []) :
=

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

theorem AddCommute.list_sum_right {M : Type u_3} [] (l : List M) (y : M) (h : ∀ (x : M), x l) :
theorem Commute.list_prod_right {M : Type u_3} [] (l : List M) (y : M) (h : ∀ (x : M), x lCommute y x) :
Commute y ()
theorem AddCommute.list_sum_left {M : Type u_3} [] (l : List M) (y : M) (h : ∀ (x : M), x l) :
theorem Commute.list_prod_left {M : Type u_3} [] (l : List M) (y : M) (h : ∀ (x : M), x lCommute x y) :
Commute () y
theorem List.Forall₂.sum_le_sum {M : Type u_3} [] [] [CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] [CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x x_1] {l₁ : List M} {l₂ : List M} (h : List.Forall₂ (fun x x_1 => x x_1) l₁ l₂) :
theorem List.Forall₂.prod_le_prod' {M : Type u_3} [] [] [CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] [CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x x_1] {l₁ : List M} {l₂ : List M} (h : List.Forall₂ (fun x x_1 => x x_1) l₁ l₂) :
theorem List.Sublist.sum_le_sum {M : Type u_3} [] [] [CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] [CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x x_1] {l₁ : List M} {l₂ : List M} (h : List.Sublist l₁ l₂) (h₁ : ∀ (a : M), a l₂0 a) :

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} [] [] [CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] [CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x x_1] {l₁ : List M} {l₂ : List M} (h : List.Sublist l₁ l₂) (h₁ : ∀ (a : M), a l₂1 a) :

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.SublistForall₂.sum_le_sum {M : Type u_3} [] [] [CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] [CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x x_1] {l₁ : List M} {l₂ : List M} (h : List.SublistForall₂ (fun x x_1 => x x_1) l₁ l₂) (h₁ : ∀ (a : M), a l₂0 a) :
abbrev List.SublistForall₂.sum_le_sum.match_1 {M : Type u_1} [] {l₁ : List M} {l₂ : List M} (motive : (l, List.Forall₂ (fun x x_1 => x x_1) l₁ l List.Sublist l l₂) → Prop) :
(x : l, List.Forall₂ (fun x x_1 => x x_1) l₁ l List.Sublist l l₂) → ((w : List M) → (hall : List.Forall₂ (fun x x_1 => x x_1) l₁ w) → (hsub : List.Sublist w l₂) → motive (_ : l, List.Forall₂ (fun x x_1 => x x_1) l₁ l List.Sublist l l₂)) → motive x
Instances For
theorem List.SublistForall₂.prod_le_prod' {M : Type u_3} [] [] [CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] [CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x x_1] {l₁ : List M} {l₂ : List M} (h : List.SublistForall₂ (fun x x_1 => x x_1) l₁ l₂) (h₁ : ∀ (a : M), a l₂1 a) :
theorem List.sum_le_sum {ι : Type u_1} {M : Type u_3} [] [] [CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] [CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x x_1] {l : List ι} {f : ιM} {g : ιM} (h : ∀ (i : ι), i lf i g i) :
theorem List.prod_le_prod' {ι : Type u_1} {M : Type u_3} [] [] [CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] [CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x x_1] {l : List ι} {f : ιM} {g : ιM} (h : ∀ (i : ι), i lf i g i) :
theorem List.sum_lt_sum {ι : Type u_1} {M : Type u_3} [] [] [CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x x_1] [CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] [CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] {l : List ι} (f : ιM) (g : ιM) (h₁ : ∀ (i : ι), i lf i g i) (h₂ : i, i l f i < g i) :
theorem List.prod_lt_prod' {ι : Type u_1} {M : Type u_3} [] [] [CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1] [CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x x_1] [CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] [CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] {l : List ι} (f : ιM) (g : ιM) (h₁ : ∀ (i : ι), i lf i g i) (h₂ : i, i l f i < g i) :
theorem List.sum_lt_sum_of_ne_nil {ι : Type u_1} {M : Type u_3} [] [] [CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x x_1] [CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] [CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] {l : List ι} (hl : l []) (f : ιM) (g : ιM) (hlt : ∀ (i : ι), i lf i < g i) :
theorem List.prod_lt_prod_of_ne_nil {ι : Type u_1} {M : Type u_3} [] [] [CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1] [CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x x_1] [CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] [CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] {l : List ι} (hl : l []) (f : ιM) (g : ιM) (hlt : ∀ (i : ι), i lf i < g i) :
theorem List.sum_le_card_nsmul {M : Type u_3} [] [] [CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] [CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x x_1] (l : List M) (n : M) (h : ∀ (x : M), x lx n) :
n
theorem List.prod_le_pow_card {M : Type u_3} [] [] [CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] [CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x x_1] (l : List M) (n : M) (h : ∀ (x : M), x lx n) :
n ^
theorem List.exists_lt_of_sum_lt {ι : Type u_1} {M : Type u_3} [] [] [CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] [CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x x_1] {l : List ι} (f : ιM) (g : ιM) (h : List.sum (List.map f l) < List.sum (List.map g l)) :
i, i l f i < g i
theorem List.exists_lt_of_prod_lt' {ι : Type u_1} {M : Type u_3} [] [] [CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] [CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x x_1] {l : List ι} (f : ιM) (g : ιM) (h : List.prod (List.map f l) < List.prod (List.map g l)) :
i, i l f i < g i
theorem List.exists_le_of_sum_le {ι : Type u_1} {M : Type u_3} [] [] [CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x x_1] [CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] [CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] {l : List ι} (hl : l []) (f : ιM) (g : ιM) (h : List.sum (List.map f l) List.sum (List.map g l)) :
x, x l f x g x
theorem List.exists_le_of_prod_le' {ι : Type u_1} {M : Type u_3} [] [] [CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1] [CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x x_1] [CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] [CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] {l : List ι} (hl : l []) (f : ιM) (g : ιM) (h : List.prod (List.map f l) List.prod (List.map g l)) :
x, x l f x g x
theorem List.sum_nonneg {M : Type u_3} [] [] [CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x x_1] {l : List M} (hl₁ : ∀ (x : M), x l0 x) :
0
theorem List.one_le_prod_of_one_le {M : Type u_3} [] [] [CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x x_1] {l : List M} (hl₁ : ∀ (x : M), x l1 x) :
1
theorem List.prod_eq_zero {M₀ : Type u_6} [] {L : List M₀} (h : 0 L) :
= 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} [] [] [] {L : List M₀} :
= 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} [] [] [] {L : List M₀} (hL : ¬0 L) :
0
theorem List.sum_neg_reverse {G : Type u_7} [] (L : List G) :
= List.sum (List.reverse (List.map (fun x => -x) L))

This is the List.sum version of add_neg_rev

theorem List.prod_inv_reverse {G : Type u_7} [] (L : List G) :

This is the List.prod version of mul_inv_rev

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

A non-commutative variant of List.sum_reverse

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

A non-commutative variant of List.prod_reverse

@[simp]
theorem List.sum_drop_succ {G : Type u_7} [] (L : List G) (i : ) (p : i < ) :

Counterpart to List.sum_take_succ when we have a negation operation

@[simp]
theorem List.prod_drop_succ {G : Type u_7} [] (L : List G) (i : ) (p : i < ) :

Counterpart to List.prod_take_succ when we have an inverse operation

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

This is the List.sum version of add_neg

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

This is the List.prod version of mul_inv

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

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

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

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

theorem List.eq_of_sum_take_eq {M : Type u_3} {L : List M} {L' : List M} (h : ) (h' : ∀ (i : ), i List.sum () = List.sum (List.take i L')) :
L = L'
theorem List.eq_of_prod_take_eq {M : Type u_3} [] {L : List M} {L' : List M} (h : ) (h' : ∀ (i : ), i List.prod () = List.prod (List.take i L')) :
L = L'
theorem List.monotone_sum_take {M : Type u_3} (L : List M) :
Monotone fun i => List.sum ()
theorem List.monotone_prod_take {M : Type u_3} (L : List M) :
Monotone fun i => List.prod ()
theorem List.sum_pos {M : Type u_3} (l : List M) :
(∀ (x : M), x l0 < x) → l []0 <
abbrev List.sum_pos.match_1 {M : Type u_1} (motive : (x : List M) → (∀ (x_1 : M), x_1 x0 < x_1) → x []Prop) :
(x : List M) → (x_1 : ∀ (x_1 : M), x_1 x0 < x_1) → (x_2 : x []) → ((x : ∀ (x : M), x []0 < x) → (h : [] []) → motive [] x h) → ((b : M) → (h : ∀ (x : M), x [b]0 < x) → (x : [b] []) → motive [b] h x) → ((a b : M) → (l : List M) → (hl₁ : ∀ (x : M), x a :: b :: l0 < x) → (x : a :: b :: l []) → motive (a :: b :: l) hl₁ x) → motive x x_1 x_2
Instances For
theorem List.one_lt_prod_of_one_lt {M : Type u_3} (l : List M) :
(∀ (x : M), x l1 < x) → l []1 <
theorem List.single_le_sum {M : Type u_3} {l : List M} (hl₁ : ∀ (x : M), x l0 x) (x : M) :
x lx
theorem List.single_le_prod {M : Type u_3} {l : List M} (hl₁ : ∀ (x : M), x l1 x) (x : M) :
x lx
theorem List.all_zero_of_le_zero_le_of_sum_eq_zero {M : Type u_3} {l : List M} (hl₁ : ∀ (x : M), x l0 x) (hl₂ : = 0) {x : M} (hx : x l) :
x = 0
theorem List.all_one_of_le_one_le_of_prod_eq_one {M : Type u_3} {l : List M} (hl₁ : ∀ (x : M), x l1 x) (hl₂ : = 1) {x : M} (hx : x l) :
x = 1
theorem List.sum_eq_zero {M : Type u_3} [] {l : List M} (hl : ∀ (x : M), x lx = 0) :
= 0

Slightly more general version of List.sum_eq_zero_iff for a non-ordered AddMonoid

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

Slightly more general version of List.prod_eq_one_iff for a non-ordered Monoid

theorem List.exists_mem_ne_zero_of_sum_ne_zero {M : Type u_3} [] {l : List M} (h : 0) :
x, x l x 0
theorem List.exists_mem_ne_one_of_prod_ne_one {M : Type u_3} [] {l : List M} (h : 1) :
x, x l x 1
theorem List.sum_le_foldr_max {M : Type u_3} {N : Type u_4} [] [] [] (f : MN) (h0 : f 0 0) (hadd : ∀ (x y : M), f (x + y) max (f x) (f y)) (l : List M) :
f () List.foldr max 0 (List.map f l)
@[simp]
theorem List.sum_erase {M : Type u_3} [] [] {a : M} {l : List M} :
a la + List.sum () =
abbrev List.sum_erase.match_1 {M : Type u_1} {a : M} (motive : (x : List M) → a xProp) :
(x : List M) → (x_1 : a x) → ((b : M) → (l : List M) → (h : a b :: l) → motive (b :: l) h) → motive x x_1
Instances For
@[simp]
theorem List.prod_erase {M : Type u_3} [] [] {a : M} {l : List M} :
a la * List.prod () =
@[simp]
theorem List.sum_map_erase {ι : Type u_1} {M : Type u_3} [] [] (f : ιM) {a : ι} {l : List ι} :
a lf a + List.sum (List.map f ()) = List.sum (List.map f l)
@[simp]
theorem List.prod_map_erase {ι : Type u_1} {M : Type u_3} [] [] (f : ιM) {a : ι} {l : List ι} :
a lf a * List.prod (List.map f ()) = List.prod (List.map f l)
theorem List.sum_const_nat (m : ) (n : ) :
List.sum () = m * n
theorem List.prod_pos {R : Type u_8} (l : List R) (h : ∀ (a : R), a l0 < a) :
0 <

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

@[simp]
theorem CanonicallyOrderedCommSemiring.list_prod_pos {α : Type u_9} [] {l : List α} :
0 < ∀ (x : α), x l0 < x

A variant of List.prod_pos for CanonicallyOrderedCommSemiring.

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.

+ =

This relies on default ℕ = 0.

theorem List.headI_le_sum (L : ) :

This relies on default ℕ = 0.

theorem List.tail_sum (L : ) :
=

This relies on default ℕ = 0.

@[simp]
theorem List.alternatingSum_nil {α : Type u_2} [Zero α] [Add α] [Neg α] :
@[simp]
theorem List.alternatingProd_nil {α : Type u_2} [One α] [Mul α] [Inv α] :
@[simp]
theorem List.alternatingSum_singleton {α : Type u_2} [Zero α] [Add α] [Neg α] (a : α) :
= a
@[simp]
theorem List.alternatingProd_singleton {α : Type u_2} [One α] [Mul α] [Inv α] (a : α) :
theorem List.alternatingSum_cons_cons' {α : Type u_2} [Zero α] [Add α] [Neg α] (a : α) (b : α) (l : List α) :
List.alternatingSum (a :: b :: l) = a + -b +
theorem List.alternatingProd_cons_cons' {α : Type u_2} [One α] [Mul α] [Inv α] (a : α) (b : α) (l : List α) :
theorem List.alternatingSum_cons_cons {α : Type u_2} [] (a : α) (b : α) (l : List α) :
List.alternatingSum (a :: b :: l) = a - b +
theorem List.alternatingProd_cons_cons {α : Type u_2} [] (a : α) (b : α) (l : List α) :
List.alternatingProd (a :: b :: l) = a / b *
abbrev List.alternatingSum_cons'.match_1 {α : Type u_1} (motive : αList αProp) :
(x : α) → (x_1 : List α) → ((a : α) → motive a []) → ((a b : α) → (l : List α) → motive a (b :: l)) → motive x x_1
Instances For
theorem List.alternatingSum_cons' {α : Type u_2} [] (a : α) (l : List α) :
theorem List.alternatingProd_cons' {α : Type u_2} [] (a : α) (l : List α) :
@[simp]
theorem List.alternatingSum_cons {α : Type u_2} [] (a : α) (l : List α) :
@[simp]
theorem List.alternatingProd_cons {α : Type u_2} [] (a : α) (l : List α) :
theorem List.sum_nat_mod (l : ) (n : ) :
% n = List.sum (List.map (fun x => x % n) l) % n
theorem List.prod_nat_mod (l : ) (n : ) :
% n = List.prod (List.map (fun x => x % n) l) % n
theorem List.sum_int_mod (l : ) (n : ) :
% n = List.sum (List.map (fun x => x % n) l) % n
theorem List.prod_int_mod (l : ) (n : ) :
% n = List.prod (List.map (fun x => x % n) l) % n
theorem map_list_sum {M : Type u_3} {N : Type u_4} [] [] {F : Type u_9} [] (f : F) (l : List M) :
f () = List.sum (List.map (f) l)
theorem map_list_prod {M : Type u_3} {N : Type u_4} [] [] {F : Type u_9} [] (f : F) (l : List M) :
f () = List.prod (List.map (f) l)
theorem AddMonoidHom.map_list_sum {M : Type u_3} {N : Type u_4} [] [] (f : M →+ N) (l : List M) :
f () = List.sum (List.map (f) l)

Deprecated, use _root_.map_list_sum instead.

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

Deprecated, use _root_.map_list_prod instead.