Documentation Verification Report

PUnit

📁 Source: Mathlib/Algebra/Module/PUnit.lean

Statistics

Metric	Count
Definitions `distribMulAction`, `instDistribMulAction`, `instMulAction`, `instSMulZeroClass`, `instSMul_mathlib`, `instVAdd_mathlib`, `mulAction`, `mulActionWithZero`, `mulDistribMulAction`, `mulSemiringAction`, `smul`, `smulWithZero`, `vadd`	13
Theorems `instIsCentralScalar`, `instIsCentralVAdd`, `instIsScalarTower`, `instIsScalarTowerOfSMul`, `instSMulCommClass`, `instSMulCommClass_1`, `instVAddAssocClassOfVAdd`, `instVAddCommClass`, `instVAddCommClass_1`, `smul_eq`, `smul_eq'`, `vadd_eq`, `vadd_eq'`	13
Total	26

PUnit

Definitions

Name	Category	Theorems
`distribMulAction` 📖	CompOp	—
`instDistribMulAction` 📖	CompOp	—
`instMulAction` 📖	CompOp	—
`instSMulZeroClass` 📖	CompOp	—
`instSMul_mathlib` 📖	CompOp	3 math math: `smul_eq'`, `instSMulCommClass_1`, `instIsScalarTower`
`instVAdd_mathlib` 📖	CompOp	2 math math: `vadd_eq'`, `instVAddCommClass_1`
`mulAction` 📖	CompOp	—
`mulActionWithZero` 📖	CompOp	—
`mulDistribMulAction` 📖	CompOp	—
`mulSemiringAction` 📖	CompOp	—
`smul` 📖	CompOp	4 math math: `smul_eq`, `instIsScalarTowerOfSMul`, `instSMulCommClass`, `instIsCentralScalar`
`smulWithZero` 📖	CompOp	—
`vadd` 📖	CompOp	4 math math: `instVAddAssocClassOfVAdd`, `instVAddCommClass`, `vadd_eq`, `instIsCentralVAdd`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsCentralScalar` 📖	mathematical	—	`IsCentralScalar` `smul` `MulOpposite`	—	—
`instIsCentralVAdd` 📖	mathematical	—	`IsCentralVAdd` `vadd` `AddOpposite`	—	—
`instIsScalarTower` 📖	mathematical	—	`IsScalarTower` `instSMul_mathlib`	—	—
`instIsScalarTowerOfSMul` 📖	mathematical	—	`IsScalarTower` `smul`	—	—
`instSMulCommClass` 📖	mathematical	—	`SMulCommClass` `smul`	—	—
`instSMulCommClass_1` 📖	mathematical	—	`SMulCommClass` `instSMul_mathlib`	—	—
`instVAddAssocClassOfVAdd` 📖	mathematical	—	`VAddAssocClass` `vadd`	—	—
`instVAddCommClass` 📖	mathematical	—	`VAddCommClass` `vadd`	—	—
`instVAddCommClass_1` 📖	mathematical	—	`VAddCommClass` `instVAdd_mathlib`	—	—
`smul_eq` 📖	mathematical	—	`smul`	—	—
`smul_eq'` 📖	mathematical	—	`instSMul_mathlib`	—	—
`vadd_eq` 📖	mathematical	—	`HVAdd.hVAdd` `instHVAdd` `vadd`	—	—
`vadd_eq'` 📖	mathematical	—	`HVAdd.hVAdd` `instHVAdd` `instVAdd_mathlib`	—	—

---

← Back to Index