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	—
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