Opposite

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

Statistics

Metric	Count
Definitions	0
Theorems instIsOrderedRing, instIsOrderedRing	2
Total	2

AddOpposite

Theorems

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

MulOpposite

Theorems

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

---

← Back to Index