Documentation

Mathlib.Data.List.BigOperators.Defs

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
Instances For
    def List.prod {α : Type u_1} [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_1} [Zero G] [Add G] [Neg G] :
      List GG

      The alternating sum of a list.

      Equations
      Instances For
        def List.alternatingProd {G : Type u_1} [One G] [Mul G] [Inv G] :
        List GG

        The alternating product of a list.

        Equations
        Instances For