List

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

Statistics

Metric	Count
Definitions	0
Theorems list_prod_pos	1
Total	1

CanonicallyOrderedAdd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
list_prod_pos 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	toZeroLEOneClass NeZero.one instIsEmptyFalse

---

← Back to Index