Submonoid

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

Statistics

Metric	Count
Definitions pos	1
Theorems coe_pos, mem_pos	2
Total	3

Submonoid

Definitions

Name	Category	Theorems
pos 📖	CompOp	3 math math: mem_pos, instIsLocalizationIntPosRat, coe_pos

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_pos 📖	mathematical	—	SetLike.coe Submonoid MulZeroOneClass.toMulOneClass instSetLike pos Set.Ioi PartialOrder.toPreorder MulZeroClass.toZero MulZeroOneClass.toMulZeroClass	—	—
mem_pos 📖	mathematical	—	Submonoid MulZeroOneClass.toMulOneClass SetLike.instMembership instSetLike pos Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero MulZeroOneClass.toMulZeroClass	—	—

---

← Back to Index