Documentation

Mathlib.Algebra.Order.BigOperators.Ring.Multiset

Big operators on a multiset in ordered rings #

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

theorem Multiset.prod_nonneg {R : Type u_1} [OrderedCommSemiring R] {s : Multiset R} (h : as, 0 a) :
0 s.prod
@[simp]