Hom

📁 Source: Mathlib/Algebra/Module/Hom.lean

Statistics

Metric	Count
Definitions applyModule, instDistribMulAction, instDistribSMul, instModule, instDomMulActModule, instModule, smul, smulLeft, instModule	9
Theorems coe_smul, isCentralScalar, isScalarTower, smulCommClass, smul_apply, coe_smul', smulLeft_apply	7
Total	16

AddMonoid.End

Definitions

Name	Category	Theorems
applyModule 📖	CompOp	—
instDistribMulAction 📖	CompOp	—
instDistribSMul 📖	CompOp	6 math math: CentroidHom.toEnd_smul, smul_apply, isCentralScalar, smulCommClass, isScalarTower, coe_smul
instModule 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_smul 📖	mathematical	—	DFunLike.coe AddMonoid.End AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instFunLike SMulZeroClass.toSMul AddZero.toZero AddMonoidWithOne.toAddMonoid instAddMonoidWithOne DistribSMul.toSMulZeroClass instDistribSMul DistribMulAction.toDistribSMul Pi.instSMul	—	—
isCentralScalar 📖	mathematical	—	IsCentralScalar AddMonoid.End AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SMulZeroClass.toSMul AddZero.toZero AddMonoidWithOne.toAddMonoid instAddMonoidWithOne DistribSMul.toSMulZeroClass instDistribSMul DistribMulAction.toDistribSMul MulOpposite MulOpposite.instMonoid	—	AddMonoidHom.instIsCentralScalar
isScalarTower 📖	mathematical	—	IsScalarTower AddMonoid.End AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SMulZeroClass.toSMul AddZero.toZero AddMonoidWithOne.toAddMonoid instAddMonoidWithOne DistribSMul.toSMulZeroClass instDistribSMul DistribMulAction.toDistribSMul	—	AddMonoidHom.instIsScalarTower
smulCommClass 📖	mathematical	—	SMulCommClass AddMonoid.End AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SMulZeroClass.toSMul AddZero.toZero AddMonoidWithOne.toAddMonoid instAddMonoidWithOne DistribSMul.toSMulZeroClass instDistribSMul DistribMulAction.toDistribSMul	—	AddMonoidHom.instSMulCommClass
smul_apply 📖	mathematical	—	DFunLike.coe AddMonoid.End AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instFunLike SMulZeroClass.toSMul AddZero.toZero AddMonoidWithOne.toAddMonoid instAddMonoidWithOne DistribSMul.toSMulZeroClass instDistribSMul DistribMulAction.toDistribSMul	—	—

AddMonoidHom

Definitions

Name	Category	Theorems
instDomMulActModule 📖	CompOp	—
instModule 📖	CompOp	13 math math: addMonoidHomLequivNat_symm_apply, addMonoidHomLequivInt_apply, groupCohomology.H1IsoOfIsTrivial_inv_apply, groupCohomology.cocycles₁IsoOfIsTrivial_hom_hom_apply_apply, groupCohomology.H1IsoOfIsTrivial_H1π_apply_apply, addMonoidEndRingEquivInt_apply, groupCohomology.cocycles₁IsoOfIsTrivial_inv_hom_apply_coe, groupCohomology.H1π_comp_H1IsoOfIsTrivial_hom_apply, addMonoidHomLequivNat_apply, addMonoidHomLequivInt_symm_apply, groupCohomology.H1π_comp_H1IsoOfIsTrivial_hom, addMonoidEndRingEquivInt_symm_apply, groupCohomology.H1π_comp_H1IsoOfIsTrivial_hom_assoc
smul 📖	CompOp	1 math math: coe_smul'
smulLeft 📖	CompOp	1 math math: smulLeft_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_smul' 📖	mathematical	—	DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring instAddCommMonoid instFunLike smul DistribSMul.toAddMonoidHom DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	—
smulLeft_apply 📖	mathematical	—	DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass instFunLike smulLeft SMulZeroClass.toSMul AddZero.toZero DistribSMul.toSMulZeroClass	—	—

ZeroHom

Definitions

Name	Category	Theorems
instModule 📖	CompOp	—

---

← Back to Index