Subgroup

📁 Source: Mathlib/Algebra/Ring/Subgroup.lean

Statistics

Metric	Count
Definitions mul	1
Theorems mul_toAddSubmonoid, zero_smul	2
Total	3

AddSubgroup

Definitions

Name	Category	Theorems
mul 📖	CompOp	1 math math: mul_toAddSubmonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mul_toAddSubmonoid 📖	mathematical	—	toAddSubmonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup AddSubgroup mul AddSubmonoid AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubmonoid.mul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring	—	—
zero_smul 📖	mathematical	—	AddSubgroup AddCommGroup.toAddGroup SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction pointwiseMulAction Module.toDistribMulAction AddCommGroup.toAddCommMonoid MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Bot.bot instBot	—	zero_smul

---

← Back to Index