Documentation Verification Report

Prod

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

Statistics

Metric	Count
Definitions `prodEquiv`, `prodOfSMulCommClass`, `distribMulAction`, `distribSMul`, `mulActionWithZero`, `mulDistribMulAction`, `smulWithZero`, `smulZeroClass`	8
Theorems `smul_mk_zero`, `smul_zero_mk`	2
Total	10

DistribMulAction

Definitions

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

Prod

Definitions

Name	Category	Theorems
`distribMulAction` 📖	CompOp	29 math math: `NonUnitalStarAlgHom.inl_apply`, `NonUnitalAlgHom.fst_toFun`, `NonUnitalStarAlgHom.prodEquiv_symm_apply`, `NonUnitalAlgHom.prod_apply`, `NonUnitalStarAlgHom.prod_fst_snd`, `NonUnitalAlgHom.prod_fst_snd`, `NonUnitalAlgHom.prodEquiv_apply`, `NonUnitalAlgHom.prodEquiv_symm_apply`, `NonUnitalStarAlgHom.prod_apply`, `NonUnitalAlgHom.coe_inr`, `NonUnitalStarAlgHom.inr_apply`, `NonUnitalAlgHom.coe_prod`, `NonUnitalStarAlgHom.snd_apply`, `NonUnitalAlgHom.inl_apply`, `NonUnitalStarAlgHom.prodEquiv_apply`, `NonUnitalAlgHom.snd_prod`, `NonUnitalStarAlgHom.fst_apply`, `NonUnitalAlgHom.fst_prod`, `NonUnitalAlgHom.snd_apply`, `NonUnitalAlgHom.coe_inl`, `NonUnitalAlgHom.prod_toFun`, `NonUnitalStarAlgHom.fst_prod`, `NonUnitalStarAlgHom.coe_prod`, `NonUnitalStarAlgHom.snd_prod`, `NonUnitalAlgHom.inr_apply`, `NonUnitalStarAlgHom.coe_inr`, `NonUnitalStarAlgHom.coe_inl`, `NonUnitalAlgHom.fst_apply`, `NonUnitalAlgHom.snd_toFun`
`distribSMul` 📖	CompOp	3 math math: `Polynomial.adjSylvester_comp_sylveserMap`, `ContinuousMultilinearMap.smul_prod_smul`, `LinearMap.prodMap_smul`
`mulActionWithZero` 📖	CompOp	—
`mulDistribMulAction` 📖	CompOp	—
`smulWithZero` 📖	CompOp	1 math math: `instOrderedSMulProd`
`smulZeroClass` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`smul_mk_zero` 📖	mathematical	—	`instSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul`	—	`smul_zero`
`smul_zero_mk` 📖	mathematical	—	`instSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul`	—	`smul_zero`

---

← Back to Index