Theorems · Theorem · order theory
List.single_le_prod
∀ {M : Type u_3} [inst : CommMonoid M] [inst_1 : Preorder M] [IsOrderedMonoid M] {l : List M},
(∀ x ∈ l, 1 ≤ x) → ∀ x ∈ l, x ≤ l.prodSee also List.le_prod_of_mem.
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 13 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Preorderstatement and proof · cited by 7,952
- CommMonoidstatement and proof · cited by 2,264
- IsOrderedMonoidstatement and proof · cited by 577
- le_mul_of_one_le_right'proof · cited by 17
- le_mul_of_one_le_of_leproof · cited by 4
- List.one_le_prod_of_one_leproof · cited by 2
Cited by2
Results whose statement or proof uses this declaration.
- List.all_one_of_le_one_le_of_prod_eq_oneproof · cited by 2
- Multiset.single_le_prodproof · cited by 0