Theorems · Theorem · order theory
Multiset.prod_map_nonneg
∀ {R : Type u_1} [inst : CommMonoidWithZero R] [inst_1 : PartialOrder R] [ZeroLEOneClass R] [PosMulMono R]
{α : Type u_2} {s : Multiset α} {f : α → R}, (∀ a ∈ s, 0 ≤ f a) → 0 ≤ (Multiset.map f s).prod- Cited by
- 4 results in Mathlib
- Foundations
- Depth 18 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- PartialOrderstatement and proof · cited by 6,410
- Multisetstatement and proof · cited by 2,627
- CommMonoidWithZerostatement and proof · cited by 913
- Multiset.mapstatement and proof · cited by 876
- Multiset.prodstatement · cited by 528
- ZeroLEOneClassstatement and proof · cited by 304
- PosMulMonostatement and proof · cited by 165
- Multiset.mem_mapproof · cited by 72
- Multiset.prod_nonnegproof · cited by 1
Cited by4
Results whose statement or proof uses this declaration.
- Height.mulHeight_eval_leproof · cited by 3
- Height.mulHeight_linearMap_apply_leproof · cited by 2
- Height.mulHeight_comp_leproof · cited by 2
- Height.mulHeight₁_sum_leproof · cited by 2