Multiset

📁 Source: Mathlib/Algebra/Order/BigOperators/Ring/Multiset.lean

Statistics

Metric	Count
Definitions	0
Theorems multiset_prod_pos, le_prod_of_submultiplicative_of_nonneg, le_prod_of_submultiplicative_on_pred_of_nonneg, mem_le_prod_of_one_le	4
Total	4

CanonicallyOrderedAdd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
multiset_prod_pos 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Multiset.prod CommSemiring.toCommMonoid	—	Multiset.quot_mk_to_coe'' Multiset.prod_coe list_prod_pos

Multiset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
le_prod_of_submultiplicative_of_nonneg 📖	mathematical	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid MulZeroOneClass.toMulOneClass MulOne.toMul MulZeroClass.toMul	prod CommMonoidWithZero.toCommMonoid map	—	le_prod_of_submultiplicative_on_pred_of_nonneg
le_prod_of_submultiplicative_on_pred_of_nonneg 📖	mathematical	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid MulZeroOneClass.toMulOneClass MulOne.toMul MulZeroClass.toMul	prod CommMonoidWithZero.toCommMonoid map	—	induction instIsEmptyFalse prod_singleton map_congr mem_cons_of_mem prod_induction_nonempty prod_cons map_cons LE.le.trans mem_cons_self mul_le_mul_of_nonneg_left
mem_le_prod_of_one_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero Multiset instMembership	prod CommMonoidWithZero.toCommMonoid map	—	exists_cons_of_mem map_cons prod_cons mul_one mul_le_mul_of_nonneg_left le_trans zero_le_one'

---

← Back to Index