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.le_prod_of_submultiplicative_on_pred_of_nonneg {α : Type u_1} {β : Type u_2} [CommMonoid α] [CommMonoidWithZero β] [PartialOrder β] [PosMulMono β] (f : αβ) (p : αProp) (h0 : ∀ (a : α), 0 f a) (h_one : f 1 1) (h_mul : ∀ (a b : α), p ap bf (a * b) f a * f b) (hp_mul : ∀ (a b : α), p ap bp (a * b)) (s : Multiset α) (hps : as, p a) :
f s.prod (map f s).prod
theorem Multiset.le_prod_of_submultiplicative_of_nonneg {α : Type u_1} {β : Type u_2} [CommMonoid α] [CommMonoidWithZero β] [PartialOrder β] [PosMulMono β] (f : αβ) (h0 : ∀ (a : α), 0 f a) (h_one : f 1 1) (h_mul : ∀ (a b : α), f (a * b) f a * f b) (s : Multiset α) :
f s.prod (map f s).prod