Associated

📁 Source: Mathlib/Algebra/Order/Monoid/Associated.lean

Statistics

Metric	Count
Definitions	0
Theorems instCanonicallyOrderedMul, instIsOrderedMonoid	2
Total	2

Associates

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instCanonicallyOrderedMul 📖	mathematical	—	CanonicallyOrderedMul Associates MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero instMul CommMonoidWithZero.toCommMonoid Preorder.toLE instPreorder	—	mul_comm
instIsOrderedMonoid 📖	mathematical	—	IsOrderedMonoid Associates MonoidWithZero.toMonoid CommMonoidWithZero.toMonoidWithZero instCommMonoid CommMonoidWithZero.toCommMonoid instPartialOrder	—	mul_right_comm

---

← Back to Index