End

📁 Source: Mathlib/Algebra/Order/Group/Action/End.lean

Statistics

Metric	Count
Definitions applyMulAction, applyMulAction, applyMulAction	3
Theorems apply_faithfulSMul, smul_def, apply_faithfulSMul, smul_def, apply_faithfulSMul, smul_def	6
Total	9

RelEmbedding

Definitions

Name	Category	Theorems
applyMulAction 📖	CompOp	2 math math: smul_def, apply_faithfulSMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_faithfulSMul 📖	mathematical	—	FaithfulSMul RelEmbedding SemigroupAction.toSMul Monoid.toSemigroup instMonoid MulAction.toSemigroupAction applyMulAction	—	ext
smul_def 📖	mathematical	—	RelEmbedding SemigroupAction.toSMul Monoid.toSemigroup instMonoid MulAction.toSemigroupAction applyMulAction DFunLike.coe instFunLike	—	—

RelHom

Definitions

Name	Category	Theorems
applyMulAction 📖	CompOp	2 math math: smul_def, apply_faithfulSMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_faithfulSMul 📖	mathematical	—	FaithfulSMul RelHom SemigroupAction.toSMul Monoid.toSemigroup instMonoid MulAction.toSemigroupAction applyMulAction	—	ext
smul_def 📖	mathematical	—	RelHom SemigroupAction.toSMul Monoid.toSemigroup instMonoid MulAction.toSemigroupAction applyMulAction DFunLike.coe instFunLike	—	—

RelIso

Definitions

Name	Category	Theorems
applyMulAction 📖	CompOp	3 math math: smul_def, apply_faithfulSMul, Flag.coe_smul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_faithfulSMul 📖	mathematical	—	FaithfulSMul RelIso SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup MulAction.toSemigroupAction applyMulAction	—	ext
smul_def 📖	mathematical	—	RelIso SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid instGroup MulAction.toSemigroupAction applyMulAction DFunLike.coe instFunLike	—	—

---

← Back to Index