Basic

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

Statistics

Metric	Count
Definitions	0
Theorems mul_left_mem_add_closure, mul_mem_add_closure, mul_right_mem_add_closure	3
Total	3

MulMemClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mul_left_mem_add_closure 📖	mathematical	SetLike.instMembership AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid AddSubmonoid.instSetLike AddSubmonoid.closure SetLike.coe	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	mul_mem_add_closure AddSubmonoid.mem_closure
mul_mem_add_closure 📖	mathematical	AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid SetLike.instMembership AddSubmonoid.instSetLike AddSubmonoid.closure SetLike.coe	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	AddSubmonoid.closure_induction mul_right_mem_add_closure MulZeroClass.mul_zero ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass AddSubmonoid.instAddSubmonoidClass mul_add Distrib.leftDistribClass AddMemClass.add_mem AddSubmonoidClass.toAddMemClass
mul_right_mem_add_closure 📖	mathematical	AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid SetLike.instMembership AddSubmonoid.instSetLike AddSubmonoid.closure SetLike.coe	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	AddSubmonoid.closure_induction AddSubmonoid.mem_closure mul_mem MulZeroClass.zero_mul ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass AddSubmonoid.instAddSubmonoidClass add_mul Distrib.rightDistribClass AddMemClass.add_mem AddSubmonoidClass.toAddMemClass

---

← Back to Index