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

The alternating sum of a list.

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

The alternating product of a list.

theorem List.prod_induction {M : Type u_2} [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 ∈ l, p x) : p l.prod

theorem List.sum_induction {M : Type u_2} [Add M] [Zero M] {l : List M} (p : M → Prop) (hom : ∀ (a b : M), p a → p b → p (a + b)) (addUnit : p 0) (base : ∀ x ∈ l, p x) : p l.sum

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

theorem List.sum_map_zero {ι : Type u_1} {M : Type u_2} [AddZeroClass M] {l : List ι} : (map (fun (x : ι) => 0) l).sum = 0

theorem List.prod_induction_nonempty {M : Type u_2} [MulOneClass M] {l : List M} (p : M → Prop) (hom : ∀ (a b : M), p a → p b → p (a * b)) (hl : l ≠ []) (base : ∀ x ∈ l, p x) : p l.prod

theorem List.sum_induction_nonempty {M : Type u_2} [AddZeroClass M] {l : List M} (p : M → Prop) (hom : ∀ (a b : M), p a → p b → p (a + b)) (hl : l ≠ []) (base : ∀ x ∈ l, p x) : p l.sum

@[simp]

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

@[simp]

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

theorem List.prod_eq_pow_card {M : Type u_2} [Monoid M] (l : List M) (m : M) (h : ∀ x ∈ l, x = m) : l.prod = m ^ l.length

theorem List.sum_eq_card_nsmul {M : Type u_2} [AddMonoid M] (l : List M) (m : M) (h : ∀ x ∈ l, x = m) : l.sum = l.length • m

theorem List.prod_hom_rel {ι : Type u_1} {M : Type u_2} {N : Type u_3} [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

theorem List.sum_hom_rel {ι : Type u_1} {M : Type u_2} {N : Type u_3} [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