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.

def List.prod {α : Type u_8} [Mul α] [One α] : List α → α

Product of a list.

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

Equations

• List.prod = List.foldr (fun (x1 x2 : α) => x1 * x2) 1

def List.alternatingSum {G : Type u_8} [Zero G] [Add G] [Neg G] : List G → G

The alternating sum of a list.

Equations

• [].alternatingSum = 0
• [g].alternatingSum = g
• (g :: h :: t).alternatingSum = g + -h + t.alternatingSum

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

The alternating product of a list.

Equations

• [].alternatingProd = 1
• [g].alternatingProd = g
• (g :: h :: t).alternatingProd = g * h⁻¹ * t.alternatingProd

@[simp]

theorem List.prod_nil {M : Type u_4} [Mul M] [One M] : [].prod = 1

@[simp]

theorem List.prod_cons {M : Type u_4} [Mul M] [One M] {a : M} {l : List M} : (a :: l).prod = a * l.prod

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

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

theorem List.prod_singleton {M : Type u_4} [MulOneClass M] {a : M} : [a].prod = a

theorem List.sum_singleton {M : Type u_4} [AddZeroClass M] {a : M} : [a].sum = a

theorem List.prod_one_cons {M : Type u_4} [MulOneClass M] {l : List M} : (1 :: l).prod = l.prod

theorem List.sum_zero_cons {M : Type u_4} [AddZeroClass M] {l : List M} : (0 :: l).sum = l.sum

theorem List.prod_map_one {ι : Type u_1} {M : Type u_4} [MulOneClass M] {l : List ι} : (List.map (fun (x : ι) => 1) l).prod = 1

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_eq_foldr {M : Type u_4} [Monoid M] {l : List M} : l.prod = List.foldr (fun (x1 x2 : M) => x1 * x2) 1 l

theorem List.sum_eq_foldr {M : Type u_4} [AddMonoid M] {l : List M} : l.sum = List.foldr (fun (x1 x2 : M) => x1 + x2) 0 l

@[simp]

theorem List.prod_replicate {M : Type u_4} [Monoid M] (n : ℕ) (a : M) : (List.replicate n a).prod = a ^ n

@[simp]

theorem List.sum_replicate {M : Type u_4} [AddMonoid M] (n : ℕ) (a : M) : (List.replicate n a).sum = n • a

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

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

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 (List.map f l).prod (List.map g l).prod

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 (List.map f l).sum (List.map g l).sum