Products / sums of lists of terms of a monoid #

This file provides basic results about list.prod (definition in data.list.defs) in a monoid. It is in a separate file so that data.list.big_operators does not depend on algebra.group_power.basic.

source

@[simp]

theorem list.prod_repeat {α : Type u} [monoid α] (a : α) (n : ℕ) :

(list.repeat a n).prod = a ^ n

source

@[simp]

theorem list.sum_repeat {α : Type u} [add_monoid α] (a : α) (n : ℕ) :

(list.repeat a n).sum = n • a

source

theorem list.prod_le_of_forall_le {α : Type u} [ordered_comm_monoid α] (l : list α) (n : α) (h : ∀ (x : α), x ∈ l → x ≤ n) :

l.prod ≤ n ^ l.length

source

theorem list.sum_le_of_forall_le {α : Type u} [ordered_add_comm_monoid α] (l : list α) (n : α) (h : ∀ (x : α), x ∈ l → x ≤ n) :

l.sum ≤ l.length • n