Documentation

Mathlib.Algebra.BigOperators.Group.List

Sums and products from lists #

This file provides basic results about List.prod, List.sum, which calculate the product and sum of elements of a list and List.alternatingProd, List.alternatingSum, their alternating counterparts.

def List.sum {α : Type u_8} [Add α] [Zero α] :
List αα

Sum of a list.

List.sum [a, b, c] = ((0 + a) + b) + c

Equations
Instances For
    def List.prod {α : Type u_8} [Mul α] [One α] :
    List αα

    Product of a list.

    List.prod [a, b, c] = ((1 * a) * b) * c

    Equations
    Instances For
      def List.alternatingSum {G : Type u_8} [Zero G] [Add G] [Neg G] :
      List GG

      The alternating sum of a list.

      Equations
      • [].alternatingSum = 0
      • [g].alternatingSum = g
      • (g :: h :: t).alternatingSum = g + -h + t.alternatingSum
      Instances For
        def List.alternatingProd {G : Type u_8} [One G] [Mul G] [Inv G] :
        List GG

        The alternating product of a list.

        Equations
        • [].alternatingProd = 1
        • [g].alternatingProd = g
        • (g :: h :: t).alternatingProd = g * h⁻¹ * t.alternatingProd
        Instances For
          @[simp]
          theorem List.sum_nil {M : Type u_4} [AddZeroClass M] :
          [].sum = 0
          @[simp]
          theorem List.prod_nil {M : Type u_4} [MulOneClass M] :
          [].prod = 1
          theorem List.sum_singleton {M : Type u_4} [AddZeroClass M] {a : M} :
          [a].sum = a
          theorem List.prod_singleton {M : Type u_4} [MulOneClass M] {a : M} :
          [a].prod = a
          @[simp]
          theorem List.sum_zero_cons {M : Type u_4} [AddZeroClass M] {l : List M} :
          (0 :: l).sum = l.sum
          @[simp]
          theorem List.prod_one_cons {M : Type u_4} [MulOneClass M] {l : List M} :
          (1 :: l).prod = l.prod
          theorem List.sum_map_zero {ι : Type u_1} {M : Type u_4} [AddZeroClass M] {l : List ι} :
          (List.map (fun (x : ι) => 0) l).sum = 0
          theorem List.prod_map_one {ι : Type u_1} {M : Type u_4} [MulOneClass M] {l : List ι} :
          (List.map (fun (x : ι) => 1) l).prod = 1
          @[simp]
          theorem List.sum_cons {M : Type u_4} [AddMonoid M] {l : List M} {a : M} :
          (a :: l).sum = a + l.sum
          @[simp]
          theorem List.prod_cons {M : Type u_4} [Monoid M] {l : List M} {a : M} :
          (a :: l).prod = a * l.prod
          theorem List.sum_induction {M : Type u_4} [AddMonoid M] {l : List M} (p : MProp) (hom : ∀ (a b : M), p ap bp (a + b)) (unit : p 0) (base : xl, p x) :
          p l.sum
          theorem List.prod_induction {M : Type u_4} [Monoid M] {l : List M} (p : MProp) (hom : ∀ (a b : M), p ap bp (a * b)) (unit : p 1) (base : xl, p x) :
          p l.prod
          @[simp]
          theorem List.sum_append {M : Type u_4} [AddMonoid M] {l₁ : List M} {l₂ : List M} :
          (l₁ ++ l₂).sum = l₁.sum + l₂.sum
          @[simp]
          theorem List.prod_append {M : Type u_4} [Monoid M] {l₁ : List M} {l₂ : List M} :
          (l₁ ++ l₂).prod = l₁.prod * l₂.prod
          theorem List.sum_concat {M : Type u_4} [AddMonoid M] {l : List M} {a : M} :
          (l.concat a).sum = l.sum + a
          theorem List.prod_concat {M : Type u_4} [Monoid M] {l : List M} {a : M} :
          (l.concat a).prod = l.prod * a
          @[simp]
          theorem List.sum_join {M : Type u_4} [AddMonoid M] {l : List (List M)} :
          l.join.sum = (List.map List.sum l).sum
          @[simp]
          theorem List.prod_join {M : Type u_4} [Monoid M] {l : List (List M)} :
          l.join.prod = (List.map List.prod l).prod
          theorem List.sum_eq_foldr {M : Type u_4} [AddMonoid M] {l : List M} :
          l.sum = List.foldr (fun (x x_1 : M) => x + x_1) 0 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
          Equations
          • =
          Instances For
            theorem List.prod_eq_foldr {M : Type u_4} [Monoid M] {l : List M} :
            l.prod = List.foldr (fun (x x_1 : M) => x * x_1) 1 l
            @[simp]
            theorem List.sum_replicate {M : Type u_4} [AddMonoid M] (n : ) (a : M) :
            (List.replicate n a).sum = n a
            @[simp]
            theorem List.prod_replicate {M : Type u_4} [Monoid M] (n : ) (a : M) :
            (List.replicate n a).prod = a ^ n
            theorem List.sum_eq_card_nsmul {M : Type u_4} [AddMonoid M] (l : List M) (m : M) (h : xl, x = m) :
            l.sum = l.length m
            theorem List.prod_eq_pow_card {M : Type u_4} [Monoid M] (l : List M) (m : M) (h : xl, x = m) :
            l.prod = m ^ l.length
            theorem List.sum_hom_rel {ι : Type u_1} {M : Type u_4} {N : Type u_5} [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)) :
            r (List.map f l).sum (List.map g l).sum
            theorem List.prod_hom_rel {ι : Type u_1} {M : Type u_4} {N : Type u_5} [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)) :
            r (List.map f l).prod (List.map g l).prod
            theorem List.rel_sum {M : Type u_4} {N : Type u_5} [AddMonoid M] [AddMonoid N] {R : MNProp} (h : R 0 0) (hf : (R R R) (fun (x x_1 : M) => x + x_1) fun (x x_1 : N) => x + x_1) :
            (List.Forall₂ R R) List.sum List.sum
            theorem List.rel_prod {M : Type u_4} {N : Type u_5} [Monoid M] [Monoid N] {R : MNProp} (h : R 1 1) (hf : (R R R) (fun (x x_1 : M) => x * x_1) fun (x x_1 : N) => x * x_1) :
            (List.Forall₂ R R) List.prod List.prod
            theorem List.sum_hom {M : Type u_4} {N : Type u_5} [AddMonoid M] [AddMonoid N] (l : List M) {F : Type u_8} [FunLike F M N] [AddMonoidHomClass F M N] (f : F) :
            (List.map (f) l).sum = f l.sum
            theorem List.prod_hom {M : Type u_4} {N : Type u_5} [Monoid M] [Monoid N] (l : List M) {F : Type u_8} [FunLike F M N] [MonoidHomClass F M N] (f : F) :
            (List.map (f) l).prod = f l.prod
            theorem List.sum_hom₂ {ι : Type u_1} {M : Type u_4} {N : Type u_5} {P : Type u_6} [AddMonoid M] [AddMonoid N] [AddMonoid P] (l : List ι) (f : 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.map (fun (i : ι) => f (f₁ i) (f₂ i)) l).sum = f (List.map f₁ l).sum (List.map f₂ l).sum
            theorem List.prod_hom₂ {ι : Type u_1} {M : Type u_4} {N : Type u_5} {P : Type u_6} [Monoid M] [Monoid N] [Monoid P] (l : List ι) (f : 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.map (fun (i : ι) => f (f₁ i) (f₂ i)) l).prod = f (List.map f₁ l).prod (List.map f₂ l).prod
            @[simp]
            theorem List.sum_map_add {ι : Type u_1} {α : Type u_8} [AddCommMonoid α] {l : List ι} {f : ια} {g : ια} :
            (List.map (fun (i : ι) => f i + g i) l).sum = (List.map f l).sum + (List.map g l).sum
            @[simp]
            theorem List.prod_map_mul {ι : Type u_1} {α : Type u_8} [CommMonoid α] {l : List ι} {f : ια} {g : ια} :
            (List.map (fun (i : ι) => f i * g i) l).prod = (List.map f l).prod * (List.map g l).prod
            theorem List.sum_map_hom {ι : Type u_1} {M : Type u_4} {N : Type u_5} [AddMonoid M] [AddMonoid N] (L : List ι) (f : ιM) {G : Type u_8} [FunLike G M N] [AddMonoidHomClass G M N] (g : G) :
            (List.map (g f) L).sum = g (List.map f L).sum
            theorem List.prod_map_hom {ι : Type u_1} {M : Type u_4} {N : Type u_5} [Monoid M] [Monoid N] (L : List ι) (f : ιM) {G : Type u_8} [FunLike G M N] [MonoidHomClass G M N] (g : G) :
            (List.map (g f) L).prod = g (List.map f L).prod
            theorem List.sum_isAddUnit {M : Type u_4} [AddMonoid M] {L : List M} :
            (mL, IsAddUnit m)IsAddUnit L.sum
            abbrev List.sum_isAddUnit.match_1 {M : Type u_1} [AddMonoid M] (motive : (x : List M) → (mx, IsAddUnit m)Prop) :
            ∀ (x : List M) (x_1 : mx, IsAddUnit m), (∀ (x : m[], IsAddUnit m), motive [] x)(∀ (h : M) (t : List M) (u : mh :: t, IsAddUnit m), motive (h :: t) u)motive x x_1
            Equations
            • =
            Instances For
              theorem List.prod_isUnit {M : Type u_4} [Monoid M] {L : List M} :
              (mL, IsUnit m)IsUnit L.prod
              theorem List.sum_isAddUnit_iff {α : Type u_8} [AddCommMonoid α] {L : List α} :
              IsAddUnit L.sum mL, IsAddUnit m
              theorem List.prod_isUnit_iff {α : Type u_8} [CommMonoid α] {L : List α} :
              IsUnit L.prod mL, IsUnit m
              @[simp]
              theorem List.sum_take_add_sum_drop {M : Type u_4} [AddMonoid M] (L : List M) (i : ) :
              (List.take i L).sum + (List.drop i L).sum = L.sum
              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) n.succ)motive x x_1
              Equations
              • =
              Instances For
                @[simp]
                theorem List.prod_take_mul_prod_drop {M : Type u_4} [Monoid M] (L : List M) (i : ) :
                (List.take i L).prod * (List.drop i L).prod = L.prod
                @[simp]
                theorem List.sum_take_succ {M : Type u_4} [AddMonoid M] (L : List M) (i : ) (p : i < L.length) :
                (List.take (i + 1) L).sum = (List.take i L).sum + L[i]
                abbrev List.sum_take_succ.match_1 {M : Type u_1} (motive : (x : List M) → (x_1 : ) → x_1 < x.lengthProp) :
                ∀ (x : List M) (x_1 : ) (x_2 : x_1 < x.length), (∀ (i : ) (p : i < [].length), motive [] i p)(∀ (h : M) (t : List M) (x : 0 < (h :: t).length), motive (h :: t) 0 x)(∀ (h : M) (t : List M) (n : ) (p : n + 1 < (h :: t).length), motive (h :: t) n.succ p)motive x x_1 x_2
                Equations
                • =
                Instances For
                  @[simp]
                  theorem List.prod_take_succ {M : Type u_4} [Monoid M] (L : List M) (i : ) (p : i < L.length) :
                  (List.take (i + 1) L).prod = (List.take i L).prod * L[i]
                  theorem List.length_pos_of_sum_ne_zero {M : Type u_4} [AddMonoid M] (L : List M) (h : L.sum 0) :
                  0 < L.length

                  A list with sum not zero must have positive length.

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

                  A list with product not one must have positive length.

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

                  A list with positive sum must have positive length.

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

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

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

                  A list with negative sum must have positive length.

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

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

                  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) i.succ 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_4} [AddMonoid M] (L : List M) (n : ) (a : M) :
                    (L.set n a).sum = ((List.take n L).sum + if n < L.length then a else 0) + (List.drop (n + 1) L).sum
                    theorem List.prod_set {M : Type u_4} [Monoid M] (L : List M) (n : ) (a : M) :
                    (L.set n a).prod = ((List.take n L).prod * if n < L.length then a else 1) * (List.drop (n + 1) L).prod
                    theorem List.get?_zero_add_tail_sum {M : Type u_4} [AddMonoid M] (l : List M) :
                    (l.get? 0).getD 0 + l.tail.sum = l.sum

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

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

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

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

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

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

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

                    theorem AddCommute.list_sum_right {M : Type u_4} [AddMonoid M] (l : List M) (y : M) (h : xl, AddCommute y x) :
                    AddCommute y l.sum
                    theorem Commute.list_prod_right {M : Type u_4} [Monoid M] (l : List M) (y : M) (h : xl, Commute y x) :
                    Commute y l.prod
                    theorem AddCommute.list_sum_left {M : Type u_4} [AddMonoid M] (l : List M) (y : M) (h : xl, AddCommute x y) :
                    AddCommute l.sum y
                    theorem Commute.list_prod_left {M : Type u_4} [Monoid M] (l : List M) (y : M) (h : xl, Commute x y) :
                    Commute l.prod y
                    theorem List.sum_range_succ {M : Type u_4} [AddMonoid M] (f : M) (n : ) :
                    (List.map f (List.range n.succ)).sum = (List.map f (List.range n)).sum + f n
                    theorem List.prod_range_succ {M : Type u_4} [Monoid M] (f : M) (n : ) :
                    (List.map f (List.range n.succ)).prod = (List.map f (List.range n)).prod * f n
                    theorem List.sum_range_succ' {M : Type u_4} [AddMonoid M] (f : M) (n : ) :
                    (List.map f (List.range n.succ)).sum = f 0 + (List.map (fun (i : ) => f i.succ) (List.range n)).sum

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

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

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

                    theorem List.sum_eq_zero {M : Type u_4} [AddMonoid M] {l : List M} (hl : xl, x = 0) :
                    l.sum = 0
                    theorem List.prod_eq_one {M : Type u_4} [Monoid M] {l : List M} (hl : xl, x = 1) :
                    l.prod = 1
                    theorem List.exists_mem_ne_zero_of_sum_ne_zero {M : Type u_4} [AddMonoid M] {l : List M} (h : l.sum 0) :
                    xl, x 0
                    theorem List.exists_mem_ne_one_of_prod_ne_one {M : Type u_4} [Monoid M] {l : List M} (h : l.prod 1) :
                    xl, x 1
                    theorem List.sum_erase_of_comm {M : Type u_4} [AddMonoid M] {l : List M} {a : M} [DecidableEq M] (ha : a l) (comm : xl, yl, x + y = y + x) :
                    a + (l.erase a).sum = l.sum
                    theorem List.prod_erase_of_comm {M : Type u_4} [Monoid M] {l : List M} {a : M} [DecidableEq M] (ha : a l) (comm : xl, yl, x * y = y * x) :
                    a * (l.erase a).prod = l.prod
                    theorem List.sum_map_eq_nsmul_single {α : Type u_2} {M : Type u_4} [AddMonoid M] [DecidableEq α] {l : List α} (a : α) (f : αM) (hf : ∀ (a' : α), a' aa' lf a' = 0) :
                    (List.map f l).sum = List.count a l f a
                    theorem List.prod_map_eq_pow_single {α : Type u_2} {M : Type u_4} [Monoid M] [DecidableEq α] {l : List α} (a : α) (f : αM) (hf : ∀ (a' : α), a' aa' lf a' = 1) :
                    (List.map f l).prod = f a ^ List.count a l
                    theorem List.sum_eq_nsmul_single {M : Type u_4} [AddMonoid M] {l : List M} [DecidableEq M] (a : M) (h : ∀ (a' : M), a' aa' la' = 0) :
                    l.sum = List.count a l a
                    theorem List.prod_eq_pow_single {M : Type u_4} [Monoid M] {l : List M} [DecidableEq M] (a : M) (h : ∀ (a' : M), a' aa' la' = 1) :
                    l.prod = a ^ List.count a l
                    theorem List.Perm.sum_eq' {M : Type u_4} [AddMonoid M] {l₁ : List M} {l₂ : List M} (h : l₁.Perm l₂) (hc : List.Pairwise AddCommute l₁) :
                    l₁.sum = l₂.sum

                    If elements of a list additively commute with each other, then their sum does not depend on the order of elements.

                    theorem List.Perm.prod_eq' {M : Type u_4} [Monoid M] {l₁ : List M} {l₂ : List M} (h : l₁.Perm l₂) (hc : List.Pairwise Commute l₁) :
                    l₁.prod = l₂.prod

                    If elements of a list commute with each other, then their product does not depend on the order of elements.

                    @[simp]
                    theorem List.sum_erase {M : Type u_4} [AddCommMonoid M] {a : M} {l : List M} [DecidableEq M] (ha : a l) :
                    a + (l.erase a).sum = l.sum
                    @[simp]
                    theorem List.prod_erase {M : Type u_4} [CommMonoid M] {a : M} {l : List M} [DecidableEq M] (ha : a l) :
                    a * (l.erase a).prod = l.prod
                    @[simp]
                    theorem List.sum_map_erase {α : Type u_2} {M : Type u_4} [AddCommMonoid M] [DecidableEq α] (f : αM) {a : α} {l : List α} :
                    a lf a + (List.map f (l.erase a)).sum = (List.map f l).sum
                    abbrev List.sum_map_erase.match_1 {α : Type u_1} {a : α} (motive : (x : List α) → a xProp) :
                    ∀ (x : List α) (x_1 : a x), (∀ (b : α) (l : List α) (h : a b :: l), motive (b :: l) h)motive x x_1
                    Equations
                    • =
                    Instances For
                      @[simp]
                      theorem List.prod_map_erase {α : Type u_2} {M : Type u_4} [CommMonoid M] [DecidableEq α] (f : αM) {a : α} {l : List α} :
                      a lf a * (List.map f (l.erase a)).prod = (List.map f l).prod
                      theorem List.Perm.sum_eq {M : Type u_4} [AddCommMonoid M] {l₁ : List M} {l₂ : List M} (h : l₁.Perm l₂) :
                      l₁.sum = l₂.sum
                      theorem List.Perm.prod_eq {M : Type u_4} [CommMonoid M] {l₁ : List M} {l₂ : List M} (h : l₁.Perm l₂) :
                      l₁.prod = l₂.prod
                      theorem List.sum_reverse {M : Type u_4} [AddCommMonoid M] (l : List M) :
                      l.reverse.sum = l.sum
                      theorem List.prod_reverse {M : Type u_4} [CommMonoid M] (l : List M) :
                      l.reverse.prod = l.prod
                      abbrev List.sum_add_sum_eq_sum_zipWith_add_sum_drop.match_1 {M : Type u_1} (motive : List MList MProp) :
                      ∀ (x x_1 : List M), (∀ (ys : List M), motive [] ys)(∀ (xs : List M), motive xs [])(∀ (x : M) (xs : List M) (y : M) (ys : List M), motive (x :: xs) (y :: ys))motive x x_1
                      Equations
                      • =
                      Instances For
                        theorem List.sum_add_sum_eq_sum_zipWith_add_sum_drop {M : Type u_4} [AddCommMonoid M] (l : List M) (l' : List M) :
                        l.sum + l'.sum = (List.zipWith (fun (x x_1 : M) => x + x_1) l l').sum + (List.drop l'.length l).sum + (List.drop l.length l').sum
                        theorem List.prod_mul_prod_eq_prod_zipWith_mul_prod_drop {M : Type u_4} [CommMonoid M] (l : List M) (l' : List M) :
                        l.prod * l'.prod = (List.zipWith (fun (x x_1 : M) => x * x_1) l l').prod * (List.drop l'.length l).prod * (List.drop l.length l').prod
                        theorem List.sum_add_sum_eq_sum_zipWith_of_length_eq {M : Type u_4} [AddCommMonoid M] (l : List M) (l' : List M) (h : l.length = l'.length) :
                        l.sum + l'.sum = (List.zipWith (fun (x x_1 : M) => x + x_1) l l').sum
                        theorem List.prod_mul_prod_eq_prod_zipWith_of_length_eq {M : Type u_4} [CommMonoid M] (l : List M) (l' : List M) (h : l.length = l'.length) :
                        l.prod * l'.prod = (List.zipWith (fun (x x_1 : M) => x * x_1) l l').prod
                        theorem List.sum_map_ite {α : Type u_2} {M : Type u_4} [AddCommMonoid M] (p : αProp) [DecidablePred p] (f : αM) (g : αM) (l : List α) :
                        (List.map (fun (a : α) => if p a then f a else g a) l).sum = (List.map f (List.filter (fun (b : α) => decide (p b)) l)).sum + (List.map g (List.filter (fun (a : α) => decide ¬p a) l)).sum
                        theorem List.prod_map_ite {α : Type u_2} {M : Type u_4} [CommMonoid M] (p : αProp) [DecidablePred p] (f : αM) (g : αM) (l : List α) :
                        (List.map (fun (a : α) => if p a then f a else g a) l).prod = (List.map f (List.filter (fun (b : α) => decide (p b)) l)).prod * (List.map g (List.filter (fun (a : α) => decide ¬p a) l)).prod
                        theorem List.sum_map_filter_add_sum_map_filter_not {α : Type u_2} {M : Type u_4} [AddCommMonoid M] (p : αProp) [DecidablePred p] (f : αM) (l : List α) :
                        (List.map f (List.filter (fun (b : α) => decide (p b)) l)).sum + (List.map f (List.filter (fun (x : α) => decide ¬p x) l)).sum = (List.map f l).sum
                        theorem List.prod_map_filter_mul_prod_map_filter_not {α : Type u_2} {M : Type u_4} [CommMonoid M] (p : αProp) [DecidablePred p] (f : αM) (l : List α) :
                        (List.map f (List.filter (fun (b : α) => decide (p b)) l)).prod * (List.map f (List.filter (fun (x : α) => decide ¬p x) l)).prod = (List.map f l).prod
                        theorem List.eq_of_sum_take_eq {M : Type u_4} [AddLeftCancelMonoid M] {L : List M} {L' : List M} (h : L.length = L'.length) (h' : iL.length, (List.take i L).sum = (List.take i L').sum) :
                        L = L'
                        theorem List.eq_of_prod_take_eq {M : Type u_4} [LeftCancelMonoid M] {L : List M} {L' : List M} (h : L.length = L'.length) (h' : iL.length, (List.take i L).prod = (List.take i L').prod) :
                        L = L'
                        theorem List.sum_neg_reverse {G : Type u_7} [AddGroup G] (L : List G) :
                        -L.sum = (List.map (fun (x : G) => -x) L).reverse.sum

                        This is the List.sum version of add_neg_rev

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

                        This is the List.prod version of mul_inv_rev

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

                        A non-commutative variant of List.sum_reverse

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

                        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 < L.length) :
                        (List.drop (i + 1) L).sum = -L.get i, p + (List.drop i L).sum

                        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 < L.length) :
                        (List.drop (i + 1) L).prod = (L.get i, p)⁻¹ * (List.drop i L).prod

                        Counterpart to List.prod_take_succ when we have an inverse operation

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

                        Cancellation of a telescoping sum.

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

                        Cancellation of a telescoping product.

                        theorem List.prod_rotate_eq_one_of_prod_eq_one {G : Type u_7} [Group G] {l : List G} :
                        l.prod = 1∀ (n : ), (l.rotate n).prod = 1
                        theorem List.sum_neg {G : Type u_7} [AddCommGroup G] (L : List G) :
                        -L.sum = (List.map (fun (x : G) => -x) L).sum

                        This is the List.sum version of add_neg

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

                        This is the List.prod version of mul_inv

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

                        Cancellation of a telescoping sum.

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

                        Cancellation of a telescoping product.

                        theorem List.sum_set' {G : Type u_7} [AddCommGroup G] (L : List G) (n : ) (a : G) :
                        (L.set n a).sum = L.sum + if hn : n < L.length then -L.get 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) :
                        (L.set n a).prod = L.prod * if hn : n < L.length then (L.get n, hn)⁻¹ * a else 1

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

                        theorem List.sum_map_ite_eq {G : Type u_7} [AddCommGroup G] {A : Type u_8} [DecidableEq A] (l : List A) (f : AG) (g : AG) (a : A) :
                        (List.map (fun (x : A) => if x = a then f x else g x) l).sum = List.count a l (f a - g a) + (List.map g l).sum
                        theorem List.prod_map_ite_eq {G : Type u_7} [CommGroup G] {A : Type u_8} [DecidableEq A] (l : List A) (f : AG) (g : AG) (a : A) :
                        (List.map (fun (x : A) => if x = a then f x else g x) l).prod = (f a / g a) ^ List.count a l * (List.map g l).prod
                        theorem List.sum_const_nat (m : ) (n : ) :
                        (List.replicate m n).sum = m * n

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

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

                        This relies on default ℕ = 0.

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

                        This relies on default ℕ = 0.

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

                        This relies on default ℕ = 0.

                        @[simp]
                        theorem List.alternatingSum_nil {α : Type u_2} [Zero α] [Add α] [Neg α] :
                        [].alternatingSum = 0
                        @[simp]
                        theorem List.alternatingProd_nil {α : Type u_2} [One α] [Mul α] [Inv α] :
                        [].alternatingProd = 1
                        @[simp]
                        theorem List.alternatingSum_singleton {α : Type u_2} [Zero α] [Add α] [Neg α] (a : α) :
                        [a].alternatingSum = a
                        @[simp]
                        theorem List.alternatingProd_singleton {α : Type u_2} [One α] [Mul α] [Inv α] (a : α) :
                        [a].alternatingProd = a
                        theorem List.alternatingSum_cons_cons' {α : Type u_2} [Zero α] [Add α] [Neg α] (a : α) (b : α) (l : List α) :
                        (a :: b :: l).alternatingSum = a + -b + l.alternatingSum
                        theorem List.alternatingProd_cons_cons' {α : Type u_2} [One α] [Mul α] [Inv α] (a : α) (b : α) (l : List α) :
                        (a :: b :: l).alternatingProd = a * b⁻¹ * l.alternatingProd
                        theorem List.alternatingSum_cons_cons {α : Type u_2} [SubNegMonoid α] (a : α) (b : α) (l : List α) :
                        (a :: b :: l).alternatingSum = a - b + l.alternatingSum
                        theorem List.alternatingProd_cons_cons {α : Type u_2} [DivInvMonoid α] (a : α) (b : α) (l : List α) :
                        (a :: b :: l).alternatingProd = a / b * l.alternatingProd
                        theorem List.alternatingSum_cons' {α : Type u_2} [AddCommGroup α] (a : α) (l : List α) :
                        (a :: l).alternatingSum = a + -l.alternatingSum
                        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
                          theorem List.alternatingProd_cons' {α : Type u_2} [CommGroup α] (a : α) (l : List α) :
                          (a :: l).alternatingProd = a * l.alternatingProd⁻¹
                          @[simp]
                          theorem List.alternatingSum_cons {α : Type u_2} [AddCommGroup α] (a : α) (l : List α) :
                          (a :: l).alternatingSum = a - l.alternatingSum
                          @[simp]
                          theorem List.alternatingProd_cons {α : Type u_2} [CommGroup α] (a : α) (l : List α) :
                          (a :: l).alternatingProd = a / l.alternatingProd
                          theorem List.sum_nat_mod (l : List ) (n : ) :
                          l.sum % n = (List.map (fun (x : ) => x % n) l).sum % n
                          theorem List.prod_nat_mod (l : List ) (n : ) :
                          l.prod % n = (List.map (fun (x : ) => x % n) l).prod % n
                          theorem List.sum_int_mod (l : List ) (n : ) :
                          l.sum % n = (List.map (fun (x : ) => x % n) l).sum % n
                          theorem List.prod_int_mod (l : List ) (n : ) :
                          l.prod % n = (List.map (fun (x : ) => x % n) l).prod % n
                          theorem List.sum_map_count_dedup_filter_eq_countP {α : Type u_2} [DecidableEq α] (p : αBool) (l : List α) :
                          (List.map (fun (x : α) => List.count x l) (List.filter p l.dedup)).sum = List.countP p l

                          Summing the count of x over a list filtered by some p is just countP applied to p

                          theorem List.sum_map_count_dedup_eq_length {α : Type u_2} [DecidableEq α] (l : List α) :
                          (List.map (fun (x : α) => List.count x l) l.dedup).sum = l.length
                          theorem map_list_sum {M : Type u_4} {N : Type u_5} [AddMonoid M] [AddMonoid N] {F : Type u_8} [FunLike F M N] [AddMonoidHomClass F M N] (f : F) (l : List M) :
                          f l.sum = (List.map (f) l).sum
                          theorem map_list_prod {M : Type u_4} {N : Type u_5} [Monoid M] [Monoid N] {F : Type u_8} [FunLike F M N] [MonoidHomClass F M N] (f : F) (l : List M) :
                          f l.prod = (List.map (f) l).prod
                          @[deprecated map_list_sum]
                          theorem AddMonoidHom.map_list_sum {M : Type u_4} {N : Type u_5} [AddMonoid M] [AddMonoid N] (f : M →+ N) (l : List M) :
                          f l.sum = (List.map (f) l).sum
                          @[deprecated map_list_prod]
                          theorem MonoidHom.map_list_prod {M : Type u_4} {N : Type u_5} [Monoid M] [Monoid N] (f : M →* N) (l : List M) :
                          f l.prod = (List.map (f) l).prod
                          @[simp]
                          theorem Nat.sum_eq_listSum (l : List ) :
                          Nat.sum l = l.sum
                          theorem List.length_sigma {α : Type u_2} {σ : αType u_8} (l₁ : List α) (l₂ : (a : α) → List (σ a)) :
                          (l₁.sigma l₂).length = (List.map (fun (a : α) => (l₂ a).length) l₁).sum
                          theorem List.ranges_join (l : List ) :
                          l.ranges.join = List.range l.sum
                          theorem List.mem_mem_ranges_iff_lt_sum (l : List ) {n : } :
                          (sl.ranges, n s) n < l.sum

                          Any entry of any member of l.ranges is strictly smaller than l.sum.

                          @[simp]
                          theorem List.length_join {α : Type u_2} (L : List (List α)) :
                          L.join.length = (List.map List.length L).sum
                          theorem List.countP_join {α : Type u_2} (p : αBool) (L : List (List α)) :
                          List.countP p L.join = (List.map (List.countP p) L).sum
                          theorem List.count_join {α : Type u_2} [BEq α] (L : List (List α)) (a : α) :
                          List.count a L.join = (List.map (List.count a) L).sum
                          @[simp]
                          theorem List.length_bind {α : Type u_2} {β : Type u_3} (l : List α) (f : αList β) :
                          (l.bind f).length = (List.map (List.length f) l).sum
                          theorem List.countP_bind {α : Type u_2} {β : Type u_3} (p : βBool) (l : List α) (f : αList β) :
                          List.countP p (l.bind f) = (List.map (List.countP p f) l).sum
                          theorem List.count_bind {α : Type u_2} {β : Type u_3} [BEq β] (l : List α) (f : αList β) (x : β) :
                          List.count x (l.bind f) = (List.map (List.count x f) l).sum
                          theorem List.take_sum_join {α : Type u_2} (L : List (List α)) (i : ) :
                          List.take (List.take i (List.map List.length L)).sum L.join = (List.take i L).join

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

                          theorem List.drop_sum_join {α : Type u_2} (L : List (List α)) (i : ) :
                          List.drop (List.take i (List.map List.length L)).sum L.join = (List.drop i L).join

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

                          theorem List.drop_take_succ_join_eq_getElem {α : Type u_2} (L : List (List α)) (i : ) (h : i < L.length) :
                          List.drop (List.take i (List.map List.length L)).sum (List.take (List.take (i + 1) (List.map List.length L)).sum L.join) = L[i]

                          In a join of sublists, taking the slice between the indices A and B - 1 gives back the original sublist of index i if A is the sum of the lengths of sublists of index < i, and B is the sum of the lengths of sublists of index ≤ i.

                          @[deprecated List.drop_take_succ_join_eq_getElem]
                          theorem List.drop_take_succ_join_eq_get {α : Type u_2} (L : List (List α)) (i : Fin L.length) :
                          List.drop (List.take (i) (List.map List.length L)).sum (List.take (List.take (i + 1) (List.map List.length L)).sum L.join) = L.get i
                          theorem List.neg_one_mem_of_prod_eq_neg_one {l : List } (h : l.prod = -1) :
                          -1 l

                          If a product of integers is -1, then at least one factor must be -1.

                          theorem List.length_le_sum_of_one_le (L : List ) (h : iL, 1 i) :
                          L.length L.sum

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

                          theorem List.dvd_prod {M : Type u_4} [CommMonoid M] {a : M} {l : List M} (ha : a l) :
                          a l.prod
                          theorem List.Sublist.prod_dvd_prod {M : Type u_4} [CommMonoid M] {l₁ : List M} {l₂ : List M} (h : l₁.Sublist l₂) :
                          l₁.prod l₂.prod
                          abbrev List.alternatingSum_append.match_1 {α : Type u_1} (motive : List αList αProp) :
                          ∀ (x x_1 : List α), (∀ (l₂ : List α), motive [] l₂)(∀ (a : α) (l₁ l₂ : List α), motive (a :: l₁) l₂)motive x x_1
                          Equations
                          • =
                          Instances For
                            theorem List.alternatingSum_append {α : Type u_2} [AddCommGroup α] (l₁ : List α) (l₂ : List α) :
                            (l₁ ++ l₂).alternatingSum = l₁.alternatingSum + (-1) ^ l₁.length l₂.alternatingSum
                            theorem List.alternatingProd_append {α : Type u_2} [CommGroup α] (l₁ : List α) (l₂ : List α) :
                            (l₁ ++ l₂).alternatingProd = l₁.alternatingProd * l₂.alternatingProd ^ (-1) ^ l₁.length
                            theorem List.alternatingSum_reverse {α : Type u_2} [AddCommGroup α] (l : List α) :
                            l.reverse.alternatingSum = (-1) ^ (l.length + 1) l.alternatingSum
                            theorem List.alternatingProd_reverse {α : Type u_2} [CommGroup α] (l : List α) :
                            l.reverse.alternatingProd = l.alternatingProd ^ (-1) ^ (l.length + 1)
                            theorem MulOpposite.op_list_prod {M : Type u_4} [Monoid M] (l : List M) :
                            MulOpposite.op l.prod = (List.map MulOpposite.op l).reverse.prod
                            theorem MulOpposite.unop_list_prod {M : Type u_4} [Monoid M] (l : List Mᵐᵒᵖ) :
                            MulOpposite.unop l.prod = (List.map MulOpposite.unop l).reverse.prod
                            theorem unop_map_list_prod {M : Type u_4} {N : Type u_5} [Monoid M] [Monoid N] {F : Type u_8} [FunLike F M Nᵐᵒᵖ] [MonoidHomClass F M Nᵐᵒᵖ] (f : F) (l : List M) :
                            MulOpposite.unop (f l.prod) = (List.map (MulOpposite.unop f) l).reverse.prod

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

                            @[deprecated unop_map_list_prod]
                            theorem MonoidHom.unop_map_list_prod {M : Type u_4} {N : Type u_5} [Monoid M] [Monoid N] (f : M →* Nᵐᵒᵖ) (l : List M) :
                            MulOpposite.unop (f l.prod) = (List.map (MulOpposite.unop f) l).reverse.prod

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