Products and sums over lists

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

Sum of a list.

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

Equations

• List.sum = List.foldl (fun (x x_1 : α) => x + x_1) 0

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

Product of a list.

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

Equations

• List.prod = List.foldl (fun (x x_1 : α) => x * x_1) 1

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

The alternating sum of a list.

Equations

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

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

The alternating product of a list.

Equations

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