Documentation

Mathlib.Algebra.BigOperators.Group.List.Defs

Sums and products from lists #

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

source
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
    source
    def List.alternatingSum {G : Type u_8} [Zero G] [Add G] [Neg G] :
    List G → G

    The alternating sum of a list.

    Equations
    Instances For
      source
      def List.alternatingProd {G : Type u_8} [One G] [Mul G] [Inv G] :
      List G → G

      The alternating product of a list.

      Equations
      Instances For
        source
        @[simp]
        theorem List.prod_nil {M : Type u_4} [Mul M] [One M] :
        [].prod = 1
        source
        @[simp]
        theorem List.prod_cons {M : Type u_4} [Mul M] [One M] {a : M} {l : List M} :
        (a :: l).prod = a * l.prod
        source
        theorem List.prod_induction {M : Type u_4} [Mul M] [One M] {l : List M} (p : M → Prop) (hom : ∀ (a b : M), p a → p b → p (a * b)) (unit : p 1) (base : ∀ (x : M), x ∈ l → p x) :
        p l.prod
        source
        theorem List.sum_induction {M : Type u_4} [Add M] [Zero M] {l : List M} (p : M → Prop) (hom : ∀ (a b : M), p a → p b → p (a + b)) (unit : p 0) (base : ∀ (x : M), x ∈ l → p x) :
        p l.sum
        source
        theorem List.prod_singleton {M : Type u_4} [MulOneClass M] {a : M} :
        [a].prod = a
        source
        theorem List.sum_singleton {M : Type u_4} [AddZeroClass M] {a : M} :
        [a].sum = a
        source
        theorem List.prod_one_cons {M : Type u_4} [MulOneClass M] {l : List M} :
        (1 :: l).prod = l.prod
        source
        theorem List.sum_zero_cons {M : Type u_4} [AddZeroClass M] {l : List M} :
        (0 :: l).sum = l.sum
        source
        theorem List.prod_map_one {ι : Type u_1} {M : Type u_4} [MulOneClass M] {l : List ι} :
        (map (fun (x : ι) => 1) l).prod = 1
        source
        theorem List.sum_map_zero {ι : Type u_1} {M : Type u_4} [AddZeroClass M] {l : List ι} :
        (map (fun (x : ι) => 0) l).sum = 0
        source
        theorem List.prod_eq_foldr {M : Type u_4} [Monoid M] {l : List M} :
        l.prod = foldr (fun (x1 x2 : M) => x1 * x2) 1 l
        source
        theorem List.sum_eq_foldr {M : Type u_4} [AddMonoid M] {l : List M} :
        l.sum = foldr (fun (x1 x2 : M) => x1 + x2) 0 l
        source
        @[simp]
        theorem List.prod_replicate {M : Type u_4} [Monoid M] (n : ℕ) (a : M) :
        (replicate n a).prod = a ^ n
        source
        @[simp]
        theorem List.sum_replicate {M : Type u_4} [AddMonoid M] (n : ℕ) (a : M) :
        (replicate n a).sum = n • a
        source
        theorem List.prod_eq_pow_card {M : Type u_4} [Monoid M] (l : List M) (m : M) (h : ∀ (x : M), x ∈ l → x = m) :
        l.prod = m ^ l.length
        source
        theorem List.sum_eq_card_nsmul {M : Type u_4} [AddMonoid M] (l : List M) (m : M) (h : ∀ (x : M), x ∈ l → x = m) :
        l.sum = l.length • m
        source
        theorem List.prod_hom_rel {ι : Type u_1} {M : Type u_4} {N : Type u_5} [Monoid M] [Monoid N] (l : List ι) {r : M → N → Prop} {f : ι → M} {g : ι → N} (h₁ : r 1 1) (h₂ : ∀ ⦃i : ι⦄ ⦃a : M⦄ ⦃b : N⦄, r a b → r (f i * a) (g i * b)) :
        r (map f l).prod (map g l).prod
        source
        theorem List.sum_hom_rel {ι : Type u_1} {M : Type u_4} {N : Type u_5} [AddMonoid M] [AddMonoid N] (l : List ι) {r : M → N → Prop} {f : ι → M} {g : ι → N} (h₁ : r 0 0) (h₂ : ∀ ⦃i : ι⦄ ⦃a : M⦄ ⦃b : N⦄, r a b → r (f i + a) (g i + b)) :
        r (map f l).sum (map g l).sum