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_1} [inst : AddMonoid M] :
List.sum [] = 0
@[simp]
theorem List.prod_nil {M : Type u_1} [inst : Monoid M] :
theorem List.sum_singleton {M : Type u_1} [inst : AddMonoid M] {a : M} :
List.sum [a] = a
theorem List.prod_singleton {M : Type u_1} [inst : Monoid M] {a : M} :
List.prod [a] = a
@[simp]
theorem List.sum_cons {M : Type u_1} [inst : AddMonoid M] {l : List M} {a : M} :
List.sum (a :: l) = a + List.sum l
@[simp]
theorem List.prod_cons {M : Type u_1} [inst : Monoid M] {l : List M} {a : M} :
@[simp]
theorem List.sum_append {M : Type u_1} [inst : AddMonoid M] {l₁ : List M} {l₂ : List M} :
List.sum (l₁ ++ l₂) = List.sum l₁ + List.sum l₂
@[simp]
theorem List.prod_append {M : Type u_1} [inst : Monoid M] {l₁ : List M} {l₂ : List M} :
List.prod (l₁ ++ l₂) = List.prod l₁ * List.prod l₂
theorem List.sum_concat {M : Type u_1} [inst : AddMonoid M] {l : List M} {a : M} :
theorem List.prod_concat {M : Type u_1} [inst : Monoid M] {l : List M} {a : M} :
@[simp]
theorem List.sum_join {M : Type u_1} [inst : AddMonoid M] {l : List (List M)} :
@[simp]
theorem List.prod_join {M : Type u_1} [inst : Monoid M] {l : List (List M)} :
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
Equations
theorem List.sum_eq_foldr {M : Type u_1} [inst : AddMonoid M] {l : List M} :
List.sum l = List.foldr (fun x x_1 => x + x_1) 0 l
theorem List.prod_eq_foldr {M : Type u_1} [inst : Monoid M] {l : List M} :
List.prod l = List.foldr (fun x x_1 => x * x_1) 1 l
@[simp]
theorem List.sum_replicate {M : Type u_1} [inst : AddMonoid M] (n : ) (a : M) :
@[simp]
theorem List.prod_replicate {M : Type u_1} [inst : Monoid M] (n : ) (a : M) :
theorem List.sum_eq_card_nsmul {M : Type u_1} [inst : AddMonoid M] (l : List M) (m : M) (h : ∀ (x : M), x lx = m) :
theorem List.prod_eq_pow_card {M : Type u_1} [inst : Monoid M] (l : List M) (m : M) (h : ∀ (x : M), x lx = m) :
theorem List.sum_hom_rel {ι : Type u_1} {M : Type u_2} {N : Type u_3} [inst : AddMonoid M] [inst : AddMonoid N] (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_2} {N : Type u_3} [inst : Monoid M] [inst : Monoid N] (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_1} {N : Type u_3} [inst : AddMonoid M] [inst : AddMonoid N] (l : List M) {F : Type u_2} [inst : AddMonoidHomClass F M N] (f : F) :
List.sum (List.map (f) l) = f (List.sum l)
theorem List.prod_hom {M : Type u_1} {N : Type u_3} [inst : Monoid M] [inst : Monoid N] (l : List M) {F : Type u_2} [inst : MonoidHomClass F M N] (f : F) :
List.prod (List.map (f) l) = f (List.prod l)
theorem List.sum_hom₂ {ι : Type u_1} {M : Type u_3} {N : Type u_4} {P : Type u_2} [inst : AddMonoid M] [inst : AddMonoid N] [inst : AddMonoid P] (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_2} [inst : Monoid M] [inst : Monoid N] [inst : Monoid P] (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_2} {α : Type u_1} [inst : AddCommMonoid α] {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_2} {α : Type u_1} [inst : CommMonoid α] {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_1} [inst : CommMonoid α] [inst : HasDistribNeg α] (l : List α) :
theorem List.sum_map_hom {ι : Type u_1} {M : Type u_3} {N : Type u_4} [inst : AddMonoid M] [inst : AddMonoid N] (L : List ι) (f : ιM) {G : Type u_2} [inst : AddMonoidHomClass G M N] (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} [inst : Monoid M] [inst : Monoid N] (L : List ι) (f : ιM) {G : Type u_2} [inst : MonoidHomClass G M N] (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} [inst : AddMonoid M] (motive : (x : List M) → (∀ (m : M), m xIsAddUnit m) → Prop) :
(x : List M) → (x_1 : ∀ (m : M), m xIsAddUnit m) → ((x : ∀ (m : M), m []IsAddUnit m) → motive [] x) → ((h : M) → (t : List M) → (u : ∀ (m : M), m h :: tIsAddUnit m) → motive (h :: t) u) → motive x x_1
Equations
theorem List.sum_isAddUnit {M : Type u_1} [inst : AddMonoid M] {L : List M} :
(∀ (m : M), m LIsAddUnit m) → IsAddUnit (List.sum L)
theorem List.prod_isUnit {M : Type u_1} [inst : Monoid M] {L : List M} :
(∀ (m : M), m LIsUnit m) → IsUnit (List.prod L)
theorem List.sum_isAddUnit_iff {α : Type u_1} [inst : AddCommMonoid α] {L : List α} :
IsAddUnit (List.sum L) ∀ (m : α), m LIsAddUnit m
theorem List.prod_isUnit_iff {α : Type u_1} [inst : CommMonoid α] {L : List α} :
IsUnit (List.prod L) ∀ (m : α), m LIsUnit m
abbrev List.sum_take_add_sum_drop.match_1 {M : Type u_1} (motive : List MProp) :
(x : List M) → (x_1 : ) → ((i : ) → motive [] i) → ((L : List M) → motive L 0) → ((h : M) → (t : List M) → (n : ) → motive (h :: t) (Nat.succ n)) → motive x x_1
Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem List.sum_take_add_sum_drop {M : Type u_1} [inst : AddMonoid M] (L : List M) (i : ) :
@[simp]
theorem List.prod_take_mul_prod_drop {M : Type u_1} [inst : Monoid M] (L : List M) (i : ) :
@[simp]
theorem List.sum_take_succ {M : Type u_1} [inst : AddMonoid M] (L : List M) (i : ) (p : i < List.length L) :
abbrev List.sum_take_succ.match_1 {M : Type u_1} (motive : (x : List M) → (x_1 : ) → x_1 < List.length xProp) :
(x : List M) → (x_1 : ) → (x_2 : x_1 < List.length x) → ((i : ) → (p : i < List.length []) → 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) (Nat.succ n) p) → motive x x_1 x_2
Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem List.prod_take_succ {M : Type u_1} [inst : Monoid M] (L : List M) (i : ) (p : i < List.length L) :
theorem List.length_pos_of_sum_ne_zero {M : Type u_1} [inst : AddMonoid M] (L : List M) (h : List.sum L 0) :

A list with sum not zero must have positive length.

theorem List.length_pos_of_prod_ne_one {M : Type u_1} [inst : Monoid M] (L : List M) (h : List.prod L 1) :

A list with product not one must have positive length.

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

A list with positive sum must have positive length.

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

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

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

A list with negative sum must have positive length.

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

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

theorem List.sum_set {M : Type u_1} [inst : AddMonoid M] (L : List M) (n : ) (a : M) :
List.sum (List.set L n a) = (List.sum (List.take n L) + if n < List.length L then a else 0) + List.sum (List.drop (n + 1) L)
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) (Nat.succ i) a) → ((x : ) → (x_3 : M) → motive [] x x_3) → motive x x_1 x_2
Equations
theorem List.prod_set {M : Type u_1} [inst : Monoid M] (L : List M) (n : ) (a : M) :
List.prod (List.set L n a) = (List.prod (List.take n L) * if n < List.length L then a else 1) * List.prod (List.drop (n + 1) L)
theorem List.get?_zero_add_tail_sum {M : Type u_1} [inst : AddMonoid M] (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_1} [inst : Monoid M] (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_1} [inst : AddMonoid M] [inst : Inhabited M] (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_1} [inst : Monoid M] [inst : Inhabited M] (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_1} [inst : AddMonoid M] (l : List M) (y : M) (h : ∀ (x : M), x lAddCommute y x) :
theorem Commute.list_prod_right {M : Type u_1} [inst : Monoid M] (l : List M) (y : M) (h : ∀ (x : M), x lCommute y x) :
theorem AddCommute.list_sum_left {M : Type u_1} [inst : AddMonoid M] (l : List M) (y : M) (h : ∀ (x : M), x lAddCommute x y) :
theorem Commute.list_prod_left {M : Type u_1} [inst : Monoid M] (l : List M) (y : M) (h : ∀ (x : M), x lCommute x y) :
theorem List.Forall₂.sum_le_sum {M : Type u_1} [inst : AddMonoid M] [inst : Preorder M] [inst : CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] [inst : 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_1} [inst : Monoid M] [inst : Preorder M] [inst : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] [inst : 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_1} [inst : AddMonoid M] [inst : Preorder M] [inst : CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] [inst : 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≤ l₂.sum. One can prove a stronger version assuming ∀ a ∈ l₂.diff l₁, 0 ≤ a∀ a ∈ l₂.diff l₁, 0 ≤ a∈ l₂.diff l₁, 0 ≤ a≤ a instead of ∀ a ∈ l₂, 0 ≤ a∀ a ∈ l₂, 0 ≤ a∈ l₂, 0 ≤ a≤ a but this lemma is not yet in mathlib.

theorem List.Sublist.prod_le_prod' {M : Type u_1} [inst : Monoid M] [inst : Preorder M] [inst : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] [inst : 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≤ l₂.prod. One can prove a stronger version assuming ∀ a ∈ l₂.diff l₁, 1 ≤ a∀ a ∈ l₂.diff l₁, 1 ≤ a∈ l₂.diff l₁, 1 ≤ a≤ a instead of ∀ a ∈ l₂, 1 ≤ a∀ a ∈ l₂, 1 ≤ a∈ l₂, 1 ≤ a≤ a but this lemma is not yet in mathlib.

theorem List.SublistForall₂.sum_le_sum {M : Type u_1} [inst : AddMonoid M] [inst : Preorder M] [inst : CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] [inst : 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} [inst : Preorder M] {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
Equations
theorem List.SublistForall₂.prod_le_prod' {M : Type u_1} [inst : Monoid M] [inst : Preorder M] [inst : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] [inst : 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_2} {M : Type u_1} [inst : AddMonoid M] [inst : Preorder M] [inst : CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] [inst : 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_2} {M : Type u_1} [inst : Monoid M] [inst : Preorder M] [inst : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] [inst : 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_2} {M : Type u_1} [inst : AddMonoid M] [inst : Preorder M] [inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x x_1] [inst : CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : 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_2} {M : Type u_1} [inst : Monoid M] [inst : Preorder M] [inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x x_1] [inst : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : 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_2} {M : Type u_1} [inst : AddMonoid M] [inst : Preorder M] [inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x x_1] [inst : CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : 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_2} {M : Type u_1} [inst : Monoid M] [inst : Preorder M] [inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x x_1] [inst : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : 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_1} [inst : AddMonoid M] [inst : Preorder M] [inst : CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] [inst : 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) :
theorem List.prod_le_pow_card {M : Type u_1} [inst : Monoid M] [inst : Preorder M] [inst : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] [inst : 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) :
theorem List.exists_lt_of_sum_lt {ι : Type u_2} {M : Type u_1} [inst : AddMonoid M] [inst : LinearOrder M] [inst : CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] [inst : 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_2} {M : Type u_1} [inst : Monoid M] [inst : LinearOrder M] [inst : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] [inst : 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_2} {M : Type u_1} [inst : AddMonoid M] [inst : LinearOrder M] [inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x x_1] [inst : CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : 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_2} {M : Type u_1} [inst : Monoid M] [inst : LinearOrder M] [inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x x_1] [inst : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : 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_1} [inst : AddMonoid M] [inst : Preorder M] [inst : 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) :
theorem List.one_le_prod_of_one_le {M : Type u_1} [inst : Monoid M] [inst : Preorder M] [inst : 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) :
theorem List.prod_eq_zero {M₀ : Type u_1} [inst : MonoidWithZero M₀] {L : List M₀} (h : 0 L) :

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_1} [inst : MonoidWithZero M₀] [inst : Nontrivial M₀] [inst : NoZeroDivisors M₀] {L : List M₀} :
List.prod L = 0 0 L

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

theorem List.prod_ne_zero {M₀ : Type u_1} [inst : MonoidWithZero M₀] [inst : Nontrivial M₀] [inst : NoZeroDivisors M₀] {L : List M₀} (hL : ¬0 L) :
theorem List.sum_neg_reverse {G : Type u_1} [inst : AddGroup G] (L : List G) :

This is the List.sum version of add_neg_rev

theorem List.prod_inv_reverse {G : Type u_1} [inst : Group G] (L : List G) :

This is the List.prod version of mul_inv_rev

theorem List.sum_reverse_noncomm {G : Type u_1} [inst : AddGroup G] (L : List G) :

A non-commutative variant of List.sum_reverse

theorem List.prod_reverse_noncomm {G : Type u_1} [inst : Group G] (L : List G) :

A non-commutative variant of List.prod_reverse

@[simp]
theorem List.sum_drop_succ {G : Type u_1} [inst : AddGroup G] (L : List G) (i : ) (p : i < List.length L) :

Counterpart to List.sum_take_succ when we have an negation operation

@[simp]
theorem List.prod_drop_succ {G : Type u_1} [inst : Group G] (L : List G) (i : ) (p : i < List.length L) :

Counterpart to List.prod_take_succ when we have an inverse operation

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

This is the List.sum version of add_neg

theorem List.prod_inv {G : Type u_1} [inst : CommGroup G] (L : List G) :

This is the List.prod version of mul_inv

theorem List.sum_set' {G : Type u_1} [inst : AddCommGroup G] (L : List G) (n : ) (a : G) :
List.sum (List.set L n a) = List.sum L + if hn : n < List.length L 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_1} [inst : CommGroup G] (L : List G) (n : ) (a : G) :
List.prod (List.set L n a) = List.prod L * if hn : n < List.length L 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_1} [inst : AddLeftCancelMonoid M] {L : List M} {L' : List M} (h : List.length L = List.length L') (h' : ∀ (i : ), i List.length LList.sum (List.take i L) = List.sum (List.take i L')) :
L = L'
theorem List.eq_of_prod_take_eq {M : Type u_1} [inst : LeftCancelMonoid M] {L : List M} {L' : List M} (h : List.length L = List.length L') (h' : ∀ (i : ), i List.length LList.prod (List.take i L) = List.prod (List.take i L')) :
L = L'
theorem List.sum_pos {M : Type u_1} [inst : OrderedAddCommMonoid M] (l : List M) :
(∀ (x : M), x l0 < x) → l []0 < List.sum l
abbrev List.sum_pos.match_1 {M : Type u_1} [inst : OrderedAddCommMonoid M] (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
Equations
  • One or more equations did not get rendered due to their size.
theorem List.one_lt_prod_of_one_lt {M : Type u_1} [inst : OrderedCommMonoid M] (l : List M) :
(∀ (x : M), x l1 < x) → l []1 < List.prod l
theorem List.single_le_sum {M : Type u_1} [inst : OrderedAddCommMonoid M] {l : List M} (hl₁ : ∀ (x : M), x l0 x) (x : M) :
x lx List.sum l
theorem List.single_le_prod {M : Type u_1} [inst : OrderedCommMonoid M] {l : List M} (hl₁ : ∀ (x : M), x l1 x) (x : M) :
x lx List.prod l
theorem List.all_zero_of_le_zero_le_of_sum_eq_zero {M : Type u_1} [inst : OrderedAddCommMonoid M] {l : List M} (hl₁ : ∀ (x : M), x l0 x) (hl₂ : List.sum l = 0) {x : M} (hx : x l) :
x = 0
theorem List.all_one_of_le_one_le_of_prod_eq_one {M : Type u_1} [inst : OrderedCommMonoid M] {l : List M} (hl₁ : ∀ (x : M), x l1 x) (hl₂ : List.prod l = 1) {x : M} (hx : x l) :
x = 1
theorem List.sum_eq_zero {M : Type u_1} [inst : AddMonoid M] {l : List M} (hl : ∀ (x : M), x lx = 0) :

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

theorem List.prod_eq_one {M : Type u_1} [inst : Monoid M] {l : List M} (hl : ∀ (x : M), x lx = 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_1} [inst : AddMonoid M] {l : List M} (h : List.sum l 0) :
x, x l x 0
theorem List.exists_mem_ne_one_of_prod_ne_one {M : Type u_1} [inst : Monoid M] {l : List M} (h : List.prod l 1) :
x, x l x 1
theorem List.sum_le_foldr_max {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst : AddMonoid N] [inst : LinearOrder N] (f : MN) (h0 : f 0 0) (hadd : ∀ (x y : M), f (x + y) max (f x) (f y)) (l : List M) :
f (List.sum l) List.foldr max 0 (List.map f l)
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
Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem List.sum_erase {M : Type u_1} [inst : DecidableEq M] [inst : AddCommMonoid M] {a : M} {l : List M} :
a la + List.sum (List.erase l a) = List.sum l
@[simp]
theorem List.prod_erase {M : Type u_1} [inst : DecidableEq M] [inst : CommMonoid M] {a : M} {l : List M} :
a la * List.prod (List.erase l a) = List.prod l
@[simp]
theorem List.sum_map_erase {ι : Type u_1} {M : Type u_2} [inst : DecidableEq ι] [inst : AddCommMonoid M] (f : ιM) {a : ι} {l : List ι} :
a lf a + List.sum (List.map f (List.erase l a)) = List.sum (List.map f l)
@[simp]
theorem List.prod_map_erase {ι : Type u_1} {M : Type u_2} [inst : DecidableEq ι] [inst : CommMonoid M] (f : ιM) {a : ι} {l : List ι} :
a lf a * List.prod (List.map f (List.erase l a)) = List.prod (List.map f l)
theorem List.prod_pos {R : Type u_1} [inst : StrictOrderedSemiring R] (l : List R) (h : ∀ (a : R), a l0 < a) :

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_1} [inst : CanonicallyOrderedCommSemiring α] [inst : Nontrivial α] {l : List α} :
0 < List.prod l ∀ (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.

This relies on default ℕ = 0.

This relies on default ℕ = 0.

@[simp]
theorem List.alternatingSum_nil {α : Type u_1} [inst : Zero α] [inst : Add α] [inst : Neg α] :
@[simp]
theorem List.alternatingProd_nil {α : Type u_1} [inst : One α] [inst : Mul α] [inst : Inv α] :
@[simp]
theorem List.alternatingSum_singleton {α : Type u_1} [inst : Zero α] [inst : Add α] [inst : Neg α] (a : α) :
@[simp]
theorem List.alternatingProd_singleton {α : Type u_1} [inst : One α] [inst : Mul α] [inst : Inv α] (a : α) :
theorem List.alternatingSum_cons_cons' {α : Type u_1} [inst : Zero α] [inst : Add α] [inst : Neg α] (a : α) (b : α) (l : List α) :
theorem List.alternatingProd_cons_cons' {α : Type u_1} [inst : One α] [inst : Mul α] [inst : Inv α] (a : α) (b : α) (l : List α) :
theorem List.alternatingSum_cons_cons {α : Type u_1} [inst : SubNegMonoid α] (a : α) (b : α) (l : List α) :
theorem List.alternatingProd_cons_cons {α : Type u_1} [inst : DivInvMonoid α] (a : α) (b : α) (l : List α) :
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
Equations
theorem List.alternatingSum_cons' {α : Type u_1} [inst : AddCommGroup α] (a : α) (l : List α) :
theorem List.alternatingProd_cons' {α : Type u_1} [inst : CommGroup α] (a : α) (l : List α) :
@[simp]
theorem List.alternatingSum_cons {α : Type u_1} [inst : AddCommGroup α] (a : α) (l : List α) :
@[simp]
theorem List.alternatingProd_cons {α : Type u_1} [inst : CommGroup α] (a : α) (l : List α) :
theorem List.sum_nat_mod (l : List ) (n : ) :
List.sum l % n = List.sum (List.map (fun x => x % n) l) % n
theorem List.prod_nat_mod (l : List ) (n : ) :
List.prod l % n = List.prod (List.map (fun x => x % n) l) % n
theorem List.sum_int_mod (l : List ) (n : ) :
List.sum l % n = List.sum (List.map (fun x => x % n) l) % n
theorem List.prod_int_mod (l : List ) (n : ) :
List.prod l % n = List.prod (List.map (fun x => x % n) l) % n
theorem map_list_sum {M : Type u_2} {N : Type u_3} [inst : AddMonoid M] [inst : AddMonoid N] {F : Type u_1} [inst : AddMonoidHomClass F M N] (f : F) (l : List M) :
f (List.sum l) = List.sum (List.map (f) l)
theorem map_list_prod {M : Type u_2} {N : Type u_3} [inst : Monoid M] [inst : Monoid N] {F : Type u_1} [inst : MonoidHomClass F M N] (f : F) (l : List M) :
f (List.prod l) = List.prod (List.map (f) l)
theorem AddMonoidHom.map_list_sum {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst : AddMonoid N] (f : M →+ N) (l : List M) :
f (List.sum l) = List.sum (List.map (f) l)

Deprecated, use _root_.map_list_sum instead.

theorem MonoidHom.map_list_prod {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst : Monoid N] (f : M →* N) (l : List M) :
f (List.prod l) = List.prod (List.map (f) l)

Deprecated, use _root_.map_list_prod instead.