Finset

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

Statistics

Metric	Count
Definitions	0
Theorems one_le_prod	1
Total	1

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
one_le_prod 📖	mathematical	Preorder.toLE MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero	prod CommMonoidWithZero.toCommMonoid	—	induction prod_insert one_le_mul_of_one_le_of_one_le

---

← Back to Index