Documentation Verification Report

ActionHom

📁 Source: Mathlib/GroupTheory/GroupAction/DomAct/ActionHom.lean

Statistics

Metric	Count
Definitions `instMulActionDistribMulActionHomIdOfSMulCommClass`, `instMulActionMulActionHomIdOfSMulCommClass`, `instSMulDistribMulActionHomId`, `instSMulMulActionHomId`	4
Theorems `instSMulCommClassDistribMulActionHomId`, `instSMulCommClassMulActionHomId`, `mk_smul_mulActionHom_apply`, `mk_smul_mulDistribActionHom_apply`, `smul_mulActionHom_apply`, `smul_mulDistribActionHom_apply`	6
Total	10

DomMulAct

Definitions

Name	Category	Theorems
`instMulActionDistribMulActionHomIdOfSMulCommClass` 📖	CompOp	—
`instMulActionMulActionHomIdOfSMulCommClass` 📖	CompOp	—
`instSMulDistribMulActionHomId` 📖	CompOp	3 math math: `smul_mulDistribActionHom_apply`, `instSMulCommClassDistribMulActionHomId`, `mk_smul_mulDistribActionHom_apply`
`instSMulMulActionHomId` 📖	CompOp	3 math math: `smul_mulActionHom_apply`, `instSMulCommClassMulActionHomId`, `mk_smul_mulActionHom_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instSMulCommClassDistribMulActionHomId` 📖	mathematical	—	`SMulCommClass` `DomMulAct` `DistribMulActionHom` `MonoidHom.id` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instSMulDistribMulActionHomId`	—	`Function.Injective.smulCommClass` `instSMulCommClassForall_2` `DFunLike.coe_injective`
`instSMulCommClassMulActionHomId` 📖	mathematical	—	`SMulCommClass` `DomMulAct` `MulActionHom` `instSMulMulActionHomId`	—	`Function.Injective.smulCommClass` `instSMulCommClassForall_2` `DFunLike.coe_injective`
`mk_smul_mulActionHom_apply` 📖	mathematical	—	`DFunLike.coe` `MulActionHom` `instFunLikeMulActionHom` `DomMulAct` `instSMulMulActionHomId` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	—
`mk_smul_mulDistribActionHom_apply` 📖	mathematical	—	`DFunLike.coe` `DistribMulActionHom` `MonoidHom.id` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DistribMulActionHom.instFunLike` `DomMulAct` `instSMulDistribMulActionHomId` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass`	—	—
`smul_mulActionHom_apply` 📖	mathematical	—	`DFunLike.coe` `MulActionHom` `instFunLikeMulActionHom` `DomMulAct` `instSMulMulActionHomId` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm`	—	—
`smul_mulDistribActionHom_apply` 📖	mathematical	—	`DFunLike.coe` `DistribMulActionHom` `MonoidHom.id` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DistribMulActionHom.instFunLike` `DomMulAct` `instSMulDistribMulActionHomId` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm`	—	—

---

← Back to Index