Prod

📁 Source: Mathlib/Algebra/Order/Ring/Prod.lean

Statistics

Metric	Count
Definitions	0
Theorems instIsOrderedRingProd	1
Total	1

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsOrderedRingProd 📖	mathematical	—	IsOrderedRing Prod.instSemiring Prod.instPartialOrder	—	Prod.instIsOrderedAddMonoid IsOrderedRing.toIsOrderedAddMonoid zero_le_one IsOrderedRing.toZeroLEOneClass mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono

---

← Back to Index