Submonoid

📁 Source: Mathlib/Algebra/Ring/Action/Submonoid.lean

Statistics

Metric	Count
Definitions addSubgroup, addSubmonoid, «term_^+_»	3
Theorems addSubgroup_toAddSubmonoid, mem_addSubgroup, mem_addSubmonoid	3
Total	6

FixedPoints

Definitions

Name	Category	Theorems
addSubgroup 📖	CompOp	2 math math: mem_addSubgroup, addSubgroup_toAddSubmonoid
addSubmonoid 📖	CompOp	2 math math: addSubgroup_toAddSubmonoid, mem_addSubmonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addSubgroup_toAddSubmonoid 📖	mathematical	—	AddSubgroup.toAddSubmonoid addSubgroup addSubmonoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	—
mem_addSubgroup 📖	mathematical	—	AddSubgroup SetLike.instMembership AddSubgroup.instSetLike addSubgroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	—	—
mem_addSubmonoid 📖	mathematical	—	AddSubmonoid AddMonoid.toAddZeroClass SetLike.instMembership AddSubmonoid.instSetLike addSubmonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	—	—

(root)

Definitions

Name	Category	Theorems
«term_^+_» 📖	CompOp	—

---

← Back to Index