End

📁 Source: Mathlib/Algebra/GroupWithZero/Action/End.lean

Statistics

Metric	Count
Definitions applyDistribMulAction, compHom, toAddEquiv₀, distribMulActionLeft, compHom	5
Theorems applyFaithfulSMul, smul_def	2
Total	7

AddMonoid.End

Definitions

Name	Category	Theorems
applyDistribMulAction 📖	CompOp	2 math math: smul_def, applyFaithfulSMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
applyFaithfulSMul 📖	mathematical	—	FaithfulSMul AddMonoid.End AddZeroClass.toAddZero AddMonoid.toAddZeroClass SMulZeroClass.toSMul AddZero.toZero DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul instMonoid applyDistribMulAction	—	AddMonoidHom.ext
smul_def 📖	mathematical	—	AddMonoid.End AddZeroClass.toAddZero AddMonoid.toAddZeroClass SMulZeroClass.toSMul AddZero.toZero DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul instMonoid applyDistribMulAction DFunLike.coe instFunLike	—	—

DistribMulAction

Definitions

Name	Category	Theorems
compHom 📖	CompOp	—
toAddEquiv₀ 📖	CompOp	—

Function.Surjective

Definitions

Name	Category	Theorems
distribMulActionLeft 📖	CompOp	—

MulDistribMulAction

Definitions

Name	Category	Theorems
compHom 📖	CompOp	—

---

← Back to Index