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} [AddMonoid M] :
List.sum [] = 0
@[simp]
theorem List.prod_nil {M : Type u_3} [Monoid M] :
theorem List.sum_singleton {M : Type u_3} [AddMonoid M] {a : M} :
List.sum [a] = a
theorem List.prod_singleton {M : Type u_3} [Monoid M] {a : M} :
List.prod [a] = a
@[simp]
theorem List.sum_cons {M : Type u_3} [AddMonoid M] {l : List M} {a : M} :
List.sum (a :: l) = a + List.sum l
@[simp]
theorem List.prod_cons {M : Type u_3} [Monoid M] {l : List M} {a : M} :
@[simp]
theorem List.sum_append {M : Type u_3} [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_3} [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_3} [AddMonoid M] {l : List M} {a : M} :
theorem List.prod_concat {M : Type u_3} [Monoid M] {l : List M} {a : M} :
@[simp]
theorem List.sum_join {M : Type u_3} [AddMonoid M] {l : List (List M)} :
@[simp]
theorem List.prod_join {M : Type u_3} [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
Instances For
    theorem List.sum_eq_foldr {M : Type u_3} [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_3} [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_3} [AddMonoid M] (n : ) (a : M) :
    @[simp]
    theorem List.prod_replicate {M : Type u_3} [Monoid M] (n : ) (a : M) :
    theorem List.sum_eq_card_nsmul {M : Type u_3} [AddMonoid M] (l : List M) (m : M) (h : ∀ (x : M), x lx = m) :
    theorem List.prod_eq_pow_card {M : Type u_3} [Monoid M] (l : List M) (m : M) (h : ∀ (x : M), x lx = m) :
    theorem List.sum_hom_rel {ι : Type u_1} {M : Type u_3} {N : Type u_4} [AddMonoid M] [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_3} {N : Type u_4} [Monoid M] [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_3} {N : Type u_4} [AddMonoid M] [AddMonoid N] (l : List M) {F : Type u_9} [AddMonoidHomClass F M N] (f : F) :
    List.sum (List.map (f) l) = f (List.sum l)
    theorem List.prod_hom {M : Type u_3} {N : Type u_4} [Monoid M] [Monoid N] (l : List M) {F : Type u_9} [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_5} [AddMonoid M] [AddMonoid N] [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_5} [Monoid M] [Monoid N] [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_1} {α : Type u_9} [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_1} {α : Type u_9} [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_9} [CommMonoid α] [HasDistribNeg α] (l : List α) :
    theorem List.sum_map_hom {ι : Type u_1} {M : Type u_3} {N : Type u_4} [AddMonoid M] [AddMonoid N] (L : List ι) (f : ιM) {G : Type u_9} [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} [Monoid M] [Monoid N] (L : List ι) (f : ιM) {G : Type u_9} [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} [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
    Instances For
      theorem List.sum_isAddUnit {M : Type u_3} [AddMonoid M] {L : List M} :
      (∀ (m : M), m LIsAddUnit m) → IsAddUnit (List.sum L)
      theorem List.prod_isUnit {M : Type u_3} [Monoid M] {L : List M} :
      (∀ (m : M), m LIsUnit m) → IsUnit (List.prod L)
      theorem List.sum_isAddUnit_iff {α : Type u_9} [AddCommMonoid α] {L : List α} :
      IsAddUnit (List.sum L) ∀ (m : α), m LIsAddUnit m
      theorem List.prod_isUnit_iff {α : Type u_9} [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.
      Instances For
        @[simp]
        theorem List.sum_take_add_sum_drop {M : Type u_3} [AddMonoid M] (L : List M) (i : ) :
        @[simp]
        theorem List.prod_take_mul_prod_drop {M : Type u_3} [Monoid M] (L : List M) (i : ) :
        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.
        Instances For
          @[simp]
          theorem List.sum_take_succ {M : Type u_3} [AddMonoid M] (L : List M) (i : ) (p : i < List.length L) :
          @[simp]
          theorem List.prod_take_succ {M : Type u_3} [Monoid M] (L : List M) (i : ) (p : i < List.length L) :
          theorem List.length_pos_of_sum_ne_zero {M : Type u_3} [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_3} [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_3} [AddMonoid M] [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_3} [Monoid M] [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_3} [AddMonoid M] [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_3} [Monoid M] [Preorder M] (L : List M) (h : List.prod L < 1) :

          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) (Nat.succ i) a) → ((x : ) → (x_3 : M) → motive [] x x_3) → motive x x_1 x_2
          Equations
          Instances For
            theorem List.sum_set {M : Type u_3} [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)
            theorem List.prod_set {M : Type u_3} [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)

            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.

            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.

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

            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} [AddMonoid M] (l : List M) (y : M) (h : ∀ (x : M), x lAddCommute 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 AddCommute.list_sum_left {M : Type u_3} [AddMonoid M] (l : List M) (y : M) (h : ∀ (x : M), x lAddCommute 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 List.Forall₂.sum_le_sum {M : Type u_3} [AddMonoid M] [Preorder M] [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} [Monoid M] [Preorder M] [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} [AddMonoid M] [Preorder M] [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} [Monoid M] [Preorder M] [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} [AddMonoid M] [Preorder M] [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} [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
            Instances For
              theorem List.SublistForall₂.prod_le_prod' {M : Type u_3} [Monoid M] [Preorder M] [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} [AddMonoid M] [Preorder M] [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} [Monoid M] [Preorder M] [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} [AddMonoid M] [Preorder M] [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} [Monoid M] [Preorder M] [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} [AddMonoid M] [Preorder M] [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} [Monoid M] [Preorder M] [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} [AddMonoid M] [Preorder M] [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) :
              theorem List.prod_le_pow_card {M : Type u_3} [Monoid M] [Preorder M] [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) :
              theorem List.exists_lt_of_sum_lt {ι : Type u_1} {M : Type u_3} [AddMonoid M] [LinearOrder M] [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} [Monoid M] [LinearOrder M] [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} [AddMonoid M] [LinearOrder M] [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} [Monoid M] [LinearOrder M] [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} [AddMonoid M] [Preorder M] [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_3} [Monoid M] [Preorder M] [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_6} [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_6} [MonoidWithZero M₀] [Nontrivial M₀] [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. See also List.prod_eq_zero for an implication that needs weaker typeclass assumptions.

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

              This is the List.sum version of add_neg_rev

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

              This is the List.prod version of mul_inv_rev

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

              A non-commutative variant of List.sum_reverse

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

              A non-commutative variant of List.prod_reverse

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

              Counterpart to List.sum_take_succ when we have a negation operation

              @[simp]
              theorem List.prod_drop_succ {G : Type u_7} [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_7} [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_7} [CommGroup G] (L : List G) :

              This is the List.prod version of mul_inv

              theorem List.sum_set' {G : Type u_7} [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_7} [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_3} [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_3} [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_3} [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} [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.
              Instances For
                theorem List.one_lt_prod_of_one_lt {M : Type u_3} [OrderedCommMonoid M] (l : List M) :
                (∀ (x : M), x l1 < x) → l []1 < List.prod l
                theorem List.single_le_sum {M : Type u_3} [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_3} [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_3} [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_3} [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_3} [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_3} [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_3} [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_3} [Monoid M] {l : List M} (h : List.prod l 1) :
                x, x l x 1
                theorem List.sum_le_foldr_max {M : Type u_3} {N : Type u_4} [AddMonoid M] [AddMonoid N] [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)
                @[simp]
                theorem List.sum_erase {M : Type u_3} [DecidableEq M] [AddCommMonoid M] {a : M} {l : List M} :
                a la + List.sum (List.erase l a) = List.sum 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.
                Instances For
                  @[simp]
                  theorem List.prod_erase {M : Type u_3} [DecidableEq M] [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_3} [DecidableEq ι] [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_3} [DecidableEq ι] [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.sum_const_nat (m : ) (n : ) :
                  theorem List.prod_pos {R : Type u_8} [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.

                  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_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 : α) :
                  @[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 α) :
                  theorem List.alternatingProd_cons_cons' {α : Type u_2} [One α] [Mul α] [Inv α] (a : α) (b : α) (l : List α) :
                  theorem List.alternatingSum_cons_cons {α : Type u_2} [SubNegMonoid α] (a : α) (b : α) (l : List α) :
                  theorem List.alternatingProd_cons_cons {α : Type u_2} [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
                  Instances For
                    @[simp]
                    theorem List.alternatingSum_cons {α : Type u_2} [AddCommGroup α] (a : α) (l : List α) :
                    @[simp]
                    theorem List.alternatingProd_cons {α : Type u_2} [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_3} {N : Type u_4} [AddMonoid M] [AddMonoid N] {F : Type u_9} [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_3} {N : Type u_4} [Monoid M] [Monoid N] {F : Type u_9} [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_3} {N : Type u_4} [AddMonoid M] [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_3} {N : Type u_4} [Monoid M] [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.