Order

📁 Source: Mathlib/Algebra/Module/Submodule/Order.lean

Statistics

Metric	Count
Definitions	0
Theorems toIsOrderedAddMonoid, toIsOrderedCancelAddMonoid	2
Total	2

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toIsOrderedAddMonoid 📖	mathematical	—	IsOrderedAddMonoid Submodule SetLike.instMembership setLike addCommMonoid Subtype.partialOrder	—	Function.Injective.isOrderedAddMonoid
toIsOrderedCancelAddMonoid 📖	mathematical	—	IsOrderedCancelAddMonoid Submodule SetLike.instMembership setLike addCommMonoid Subtype.partialOrder	—	Function.Injective.isOrderedCancelAddMonoid

---

← Back to Index