Documentation

Mathlib.Algebra.Order.BigOperators.Ring.List

Big operators on a list in ordered rings #

This file contains the results concerning the interaction of list big operators with ordered rings.

theorem List.prod_pos {R : Type u_1} [StrictOrderedSemiring R] (l : List R) (h : al, 0 < a) :
0 < l.prod

The product of a list of positive natural numbers is positive, and likewise for any nontrivial ordered semiring.

@[simp]
theorem CanonicallyOrderedCommSemiring.list_prod_pos {α : Type u_2} [CanonicallyOrderedCommSemiring α] [Nontrivial α] {l : List α} :
0 < l.prod xl, 0 < x

A variant of List.prod_pos for CanonicallyOrderedCommSemiring.