Hom

📁 Source: Mathlib/Algebra/Group/Action/Hom.lean

Statistics

Metric	Count
Definitions compHom, vaddZeroHom, addActionLeft, mulActionLeft, smulOneHom, compHom, addMonoidHomEquivAddActionVAddAssocClass, monoidHomEquivMulActionIsScalarTower	8
Theorems of_compHom, compHom_vadd_def, isPretransitive_compHom, vaddZeroHom_apply, smulOneHom_apply, of_compHom, compHom_smul_def, isPretransitive_compHom	8
Total	16

AddAction

Definitions

Name	Category	Theorems
compHom 📖	CompOp	3 math math: isPretransitive_compHom, continuousVAdd_compHom, compHom_vadd_def

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compHom_vadd_def 📖	mathematical	—	HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup toAddSemigroupAction compHom DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidHom.instFunLike	—	—
isPretransitive_compHom 📖	mathematical	DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidHom.instFunLike	IsPretransitive AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup toAddSemigroupAction compHom	—	exists_vadd_eq

AddAction.IsPretransitive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_compHom 📖	mathematical	—	AddAction.IsPretransitive AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddAction.toAddSemigroupAction	—	of_vadd_eq

AddMonoidHom

Definitions

Name	Category	Theorems
vaddZeroHom 📖	CompOp	1 math math: vaddZeroHom_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
vaddZeroHom_apply 📖	mathematical	—	DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass instFunLike vaddZeroHom HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup AddAction.toAddSemigroupAction AddZero.toZero	—	—

Function.Surjective

Definitions

Name	Category	Theorems
addActionLeft 📖	CompOp	—
mulActionLeft 📖	CompOp	—

MonoidHom

Definitions

Name	Category	Theorems
smulOneHom 📖	CompOp	1 math math: smulOneHom_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
smulOneHom_apply 📖	mathematical	—	DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass instFunLike smulOneHom SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction MulOne.toOne	—	—

MulAction

Definitions

Name	Category	Theorems
compHom 📖	CompOp	4 math math: compHom_smul_def, isPretransitive_compHom, IsScalarTower.of_compHom, continuousSMul_compHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compHom_smul_def 📖	mathematical	—	SemigroupAction.toSMul Monoid.toSemigroup toSemigroupAction compHom DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike	—	—
isPretransitive_compHom 📖	mathematical	DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonoidHom.instFunLike	IsPretransitive SemigroupAction.toSMul Monoid.toSemigroup toSemigroupAction compHom	—	exists_smul_eq

MulAction.IsPretransitive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_compHom 📖	mathematical	—	MulAction.IsPretransitive SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction	—	of_smul_eq

(root)

Definitions

Name	Category	Theorems
addMonoidHomEquivAddActionVAddAssocClass 📖	CompOp	—
monoidHomEquivMulActionIsScalarTower 📖	CompOp	—

---

← Back to Index