Documentation Verification Report

Pi

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

Statistics

Metric	Count
Definitions `distribMulAction`, `distribMulAction'`, `distribSMul`, `distribSMul'`, `mulActionWithZero`, `mulActionWithZero'`, `mulDistribMulAction`, `mulDistribMulAction'`, `smulWithZero`, `smulWithZero'`, `smulZeroClass`, `smulZeroClass'`	12
Theorems `single_smul`, `single_smul'`, `single_smul₀`	3
Total	15

Pi

Definitions

Name	Category	Theorems
`distribMulAction` 📖	CompOp	10 math math: `Matrix.l2_opNorm_toEuclideanCLM`, `Matrix.cstar_nnnorm_def`, `BoxIntegral.unitPartition.mem_smul_span_iff`, `Matrix.toEuclideanCLM_toLp`, `Matrix.ofLp_toEuclideanCLM`, `Matrix.coe_toEuclideanCLM_eq_toEuclideanLin`, `evalNonUnitalStarAlgHom_apply`, `evalStarAlgHom_apply`, `Matrix.cstar_norm_def`, `BoxIntegral.unitPartition.tag_mem_smul_span`
`distribMulAction'` 📖	CompOp	—
`distribSMul` 📖	CompOp	5 math math: `BoxIntegral.unitPartition.mem_smul_span_iff`, `MultilinearMap.piFamily_smul`, `Matrix.cramer_smul`, `Matrix.diagonal_comp_single`, `BoxIntegral.unitPartition.tag_mem_smul_span`
`distribSMul'` 📖	CompOp	—
`mulActionWithZero` 📖	CompOp	—
`mulActionWithZero'` 📖	CompOp	—
`mulDistribMulAction` 📖	CompOp	—
`mulDistribMulAction'` 📖	CompOp	—
`smulWithZero` 📖	CompOp	1 math math: `orderedSMul`
`smulWithZero'` 📖	CompOp	—
`smulZeroClass` 📖	CompOp	4 math math: `ceilDiv_def`, `floorDiv_def`, `floorDiv_apply`, `ceilDiv_apply`
`smulZeroClass'` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`single_smul` 📖	mathematical	—	`single` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SMulZeroClass.toSMul` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `instSMul`	—	`single_op` `smul_zero`
`single_smul'` 📖	mathematical	—	`single` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SMulZeroClass.toSMul` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Function.hasSMul`	—	`single_smul`
`single_smul₀` 📖	mathematical	—	`single` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SMulZeroClass.toSMul` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `smul'` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass`	—	`single_op₂` `smul_zero`

---

← Back to Index