List

📁 Source: Mathlib/Algebra/Order/BigOperators/GroupWithZero/List.lean

Statistics

Metric	Count
Definitions	0
Theorems one_le_prod, prod_map_le_pow_length₀, prod_map_le_prod_map₀, prod_map_lt_prod_map, prod_nonneg, prod_pos	6
Total	6

List

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
one_le_prod 📖	mathematical	Preorder.toLE PartialOrder.toPreorder MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero	MulZeroClass.toMul MulZeroOneClass.toMulZeroClass	—	one_le_mul_of_one_le_of_one_le
prod_map_le_pow_length₀ 📖	mathematical	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero DFunLike.coe	MulZeroClass.toMul MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass Monoid.toNatPow MonoidWithZero.toMonoid	—	prod_replicate prod_map_le_prod_map₀
prod_map_le_prod_map₀ 📖	mathematical	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero	MulZeroClass.toMul MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass	—	posMulMono_iff_mulPosMono CommMagma.to_isCommutative mul_le_mul LE.le.trans
prod_map_lt_prod_map 📖	mathematical	Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero	MulZeroClass.toMul MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass	—	posMulStrictMono_iff_mulPosStrictMono CommMagma.to_isCommutative mul_lt_mul PosMulStrictMono.toPosMulMono prod_map_le_prod_map₀ le_of_lt prod_pos LT.lt.trans
prod_nonneg 📖	mathematical	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero	MulZeroClass.toMul MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass	—	mul_nonneg
prod_pos 📖	mathematical	Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero	MulZeroClass.toMul MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass	—	mul_pos

---

← Back to Index