Submonoid

📁 Source: Mathlib/Algebra/Order/Archimedean/Submonoid.lean

Statistics

Metric	Count
Definitions	0
Theorems instAddArchimedean, instMulArchimedean	2
Total	2

AddSubmonoidClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instAddArchimedean 📖	mathematical	—	Archimedean SetLike.instMembership toAddCommMonoid Subtype.partialOrder	—	Subtype.coe_lt_coe Archimedean.arch

SubmonoidClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instMulArchimedean 📖	mathematical	—	MulArchimedean SetLike.instMembership toCommMonoid Subtype.partialOrder	—	MulArchimedean.arch

---

← Back to Index