Documentation Verification Report

Hom

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

Statistics

Metric	Count
Definitions `Hom`, `instDistribMulAction`, `instDistribSMul`, `instSMulZeroClassOfDistribSMul`, `instMulActionWithZero`, `instSMulWithZero`, `instSMulZeroClass`	7
Theorems `coe_smul`, `instIsCentralScalar`, `instIsScalarTower`, `instSMulCommClass`, `smul_apply`, `smul_comp`, `coe_smul`, `instIsCentralScalar`, `instIsScalarTower`, `instSMulCommClass`, `smul_apply`, `smul_comp`	12
Total	19

Action

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	1 math math: `hom_injective`

AddMonoidHom

Definitions

Name	Category	Theorems
`instDistribMulAction` 📖	CompOp	—
`instDistribSMul` 📖	CompOp	—
`instSMulZeroClassOfDistribSMul` 📖	CompOp	8 math math: `instSMulCommClass`, `smul_comp`, `coe_smul`, `instIsCentralScalar`, `smul_apply`, `DomMulAct.instSMulCommClassAddMonoidHom_1`, `instIsScalarTower`, `mapMatrix_smul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_smul` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `instFunLike` `SMulZeroClass.toSMul` `instZeroAddMonoidHom` `instSMulZeroClassOfDistribSMul` `Pi.instSMul` `AddZero.toZero` `DistribSMul.toSMulZeroClass`	—	—
`instIsCentralScalar` 📖	mathematical	—	`IsCentralScalar` `AddMonoidHom` `AddZeroClass.toAddZero` `SMulZeroClass.toSMul` `instZeroAddMonoidHom` `instSMulZeroClassOfDistribSMul` `MulOpposite`	—	`ext` `IsCentralScalar.op_smul_eq_smul`
`instIsScalarTower` 📖	mathematical	—	`IsScalarTower` `AddMonoidHom` `AddZeroClass.toAddZero` `SMulZeroClass.toSMul` `instZeroAddMonoidHom` `instSMulZeroClassOfDistribSMul`	—	`ext` `smul_assoc`
`instSMulCommClass` 📖	mathematical	—	`SMulCommClass` `AddMonoidHom` `AddZeroClass.toAddZero` `SMulZeroClass.toSMul` `instZeroAddMonoidHom` `instSMulZeroClassOfDistribSMul`	—	`ext` `SMulCommClass.smul_comm`
`smul_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `instFunLike` `SMulZeroClass.toSMul` `instZeroAddMonoidHom` `instSMulZeroClassOfDistribSMul` `AddZero.toZero` `DistribSMul.toSMulZeroClass`	—	—
`smul_comp` 📖	mathematical	—	`comp` `AddZeroClass.toAddZero` `AddMonoidHom` `SMulZeroClass.toSMul` `instZeroAddMonoidHom` `instSMulZeroClassOfDistribSMul`	—	—

ZeroHom

Definitions

Name	Category	Theorems
`instMulActionWithZero` 📖	CompOp	—
`instSMulWithZero` 📖	CompOp	—
`instSMulZeroClass` 📖	CompOp	6 math math: `instSMulCommClass`, `smul_comp`, `instIsCentralScalar`, `coe_smul`, `smul_apply`, `instIsScalarTower`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_smul` 📖	mathematical	—	`DFunLike.coe` `ZeroHom` `funLike` `SMulZeroClass.toSMul` `instZeroZeroHom` `instSMulZeroClass` `Pi.instSMul`	—	—
`instIsCentralScalar` 📖	mathematical	—	`IsCentralScalar` `ZeroHom` `SMulZeroClass.toSMul` `instZeroZeroHom` `instSMulZeroClass` `MulOpposite`	—	`ext` `IsCentralScalar.op_smul_eq_smul`
`instIsScalarTower` 📖	mathematical	—	`IsScalarTower` `ZeroHom` `SMulZeroClass.toSMul` `instZeroZeroHom` `instSMulZeroClass`	—	`ext` `smul_assoc`
`instSMulCommClass` 📖	mathematical	—	`SMulCommClass` `ZeroHom` `SMulZeroClass.toSMul` `instZeroZeroHom` `instSMulZeroClass`	—	`ext` `SMulCommClass.smul_comm`
`smul_apply` 📖	mathematical	—	`DFunLike.coe` `ZeroHom` `funLike` `SMulZeroClass.toSMul` `instZeroZeroHom` `instSMulZeroClass`	—	—
`smul_comp` 📖	mathematical	—	`comp` `ZeroHom` `SMulZeroClass.toSMul` `instZeroZeroHom` `instSMulZeroClass`	—	—

---

← Back to Index