Documentation Verification Report

Prod

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

Statistics

Metric	Count
Definitions `prodEquiv`, `prodOfVAddCommClass`, `prodEquiv`, `prodOfSMulCommClass`, `addAction`, `mulAction`, `smulMonoidHom`, `smulMulHom`	8
Theorems `faithfulSMulLeft`, `faithfulSMulRight`, `faithfulVAddLeft`, `faithfulVAddRight`, `isCentralScalar`, `isCentralVAdd`, `isScalarTower`, `isScalarTowerBoth`, `smulCommClass`, `smulCommClassBoth`, `vaddAssocClass`, `vaddCommClass`, `vaddCommClassBoth`, `smulMonoidHom_apply`, `smulMulHom_apply`	15
Total	23

AddAction

Definitions

Name	Category	Theorems
`prodEquiv` 📖	CompOp	—
`prodOfVAddCommClass` 📖	CompOp	—

MulAction

Definitions

Name	Category	Theorems
`prodEquiv` 📖	CompOp	—
`prodOfSMulCommClass` 📖	CompOp	—

Prod

Definitions

Name	Category	Theorems
`addAction` 📖	CompOp	2 math math: `AddAction.orbitRel_le_fst`, `AddAction.orbitRel_le_snd`
`mulAction` 📖	CompOp	2 math math: `MulAction.orbitRel_le_snd`, `MulAction.orbitRel_le_fst`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`faithfulSMulLeft` 📖	mathematical	—	`FaithfulSMul` `instSMul`	—	`FaithfulSMul.eq_of_smul_eq_smul`
`faithfulSMulRight` 📖	mathematical	—	`FaithfulSMul` `instSMul`	—	`FaithfulSMul.eq_of_smul_eq_smul`
`faithfulVAddLeft` 📖	mathematical	—	`FaithfulVAdd` `instVAdd`	—	`FaithfulVAdd.eq_of_vadd_eq_vadd`
`faithfulVAddRight` 📖	mathematical	—	`FaithfulVAdd` `instVAdd`	—	`FaithfulVAdd.eq_of_vadd_eq_vadd`
`isCentralScalar` 📖	mathematical	—	`IsCentralScalar` `instSMul` `MulOpposite`	—	`IsCentralScalar.op_smul_eq_smul`
`isCentralVAdd` 📖	mathematical	—	`IsCentralVAdd` `instVAdd` `AddOpposite`	—	`IsCentralVAdd.op_vadd_eq_vadd`
`isScalarTower` 📖	mathematical	—	`IsScalarTower` `instSMul`	—	`smul_assoc`
`isScalarTowerBoth` 📖	mathematical	—	`IsScalarTower` `instSMul` `instMul`	—	`smul_mul_assoc`
`smulCommClass` 📖	mathematical	—	`SMulCommClass` `instSMul`	—	`SMulCommClass.smul_comm`
`smulCommClassBoth` 📖	mathematical	—	`SMulCommClass` `instSMul` `instMul`	—	`mul_smul_comm`
`vaddAssocClass` 📖	mathematical	—	`VAddAssocClass` `instVAdd`	—	`vadd_assoc`
`vaddCommClass` 📖	mathematical	—	`VAddCommClass` `instVAdd`	—	`VAddCommClass.vadd_comm`
`vaddCommClassBoth` 📖	mathematical	—	`VAddCommClass` `instVAdd` `Add.toVAdd` `instAdd`	—	`add_vadd_comm`

(root)

Definitions

Name	Category	Theorems
`smulMonoidHom` 📖	CompOp	2 math math: `smulMonoidWithZeroHom_apply`, `smulMonoidHom_apply`
`smulMulHom` 📖	CompOp	2 math math: `smulMulHom_apply`, `smulMonoidHom_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`smulMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Prod.instMulOneClass` `Monoid.toMulOneClass` `MonoidHom.instFunLike` `smulMonoidHom` `MulHom.toFun` `Prod.instMul` `MulOne.toMul` `smulMulHom`	—	—
`smulMulHom_apply` 📖	mathematical	—	`DFunLike.coe` `MulHom` `Prod.instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulHom.funLike` `smulMulHom` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction`	—	—

---

← Back to Index