Theorems · Theorem · order theory

Multiset.mem_le_prod_of_one_le

∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoidWithZero β] [inst_1 : PartialOrder β] [PosMulMono β]
  [ZeroLEOneClass β] {f : α → β},
  (∀ (a : α), 1 ≤ f a) → ∀ {s : Multiset α} {a : α}, a ∈ s → f a ≤ (Multiset.map f s).prod

Defined in

Mathlib.Algebra.Order.BigOperators.Ring.Multiset

Cited by

1 results in Mathlib

Foundations

Depth 19 from the axioms · uses propext, Quot.sound

Assumes

CommMonoidWithZeroPartialOrderPosMulMonoZeroLEOneClass