Documentation Verification Report

Sigma

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

Statistics

Metric	Count
Definitions `VAdd`, `instAddAction`, `instMulAction`, `instSMul_mathlib`	4
Theorems `FaithfulSMul'`, `FaithfulVAdd'`, `instFaithfulSMulOfNonempty`, `instFaithfulVAddOfNonempty`, `instIsCentralScalar`, `instIsCentralVAdd`, `instIsScalarTowerOfSMul`, `instSMulCommClass`, `instVAddAssocClassOfVAdd`, `instVAddCommClass`, `smul_def`, `smul_mk`, `vadd_def`, `vadd_mk`	14
Total	18

Sigma

Definitions

Name	Category	Theorems
`VAdd` 📖	CompOp	7 math math: `FaithfulVAdd'`, `instVAddCommClass`, `vadd_mk`, `instIsCentralVAdd`, `instVAddAssocClassOfVAdd`, `instFaithfulVAddOfNonempty`, `vadd_def`
`instAddAction` 📖	CompOp	—
`instMulAction` 📖	CompOp	—
`instSMul_mathlib` 📖	CompOp	7 math math: `instIsScalarTowerOfSMul`, `smul_mk`, `instIsCentralScalar`, `FaithfulSMul'`, `smul_def`, `instSMulCommClass`, `instFaithfulSMulOfNonempty`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`FaithfulSMul'` 📖	mathematical	—	`FaithfulSMul` `instSMul_mathlib`	—	`FaithfulSMul.eq_of_smul_eq_smul`
`FaithfulVAdd'` 📖	mathematical	—	`FaithfulVAdd` `VAdd`	—	`FaithfulVAdd.eq_of_vadd_eq_vadd`
`instFaithfulSMulOfNonempty` 📖	mathematical	`FaithfulSMul`	`instSMul_mathlib`	—	`FaithfulSMul'`
`instFaithfulVAddOfNonempty` 📖	mathematical	`FaithfulVAdd`	`VAdd`	—	`FaithfulVAdd'`
`instIsCentralScalar` 📖	mathematical	`IsCentralScalar`	`instSMul_mathlib` `MulOpposite`	—	`IsCentralScalar.op_smul_eq_smul`
`instIsCentralVAdd` 📖	mathematical	`IsCentralVAdd`	`VAdd` `AddOpposite`	—	`IsCentralVAdd.op_vadd_eq_vadd`
`instIsScalarTowerOfSMul` 📖	mathematical	`IsScalarTower`	`instSMul_mathlib`	—	`smul_assoc`
`instSMulCommClass` 📖	mathematical	`SMulCommClass`	`instSMul_mathlib`	—	`SMulCommClass.smul_comm`
`instVAddAssocClassOfVAdd` 📖	mathematical	`VAddAssocClass`	`VAdd`	—	`vadd_assoc`
`instVAddCommClass` 📖	mathematical	`VAddCommClass`	`VAdd`	—	`VAddCommClass.vadd_comm`
`smul_def` 📖	mathematical	—	`instSMul_mathlib` `map`	—	—
`smul_mk` 📖	mathematical	—	`instSMul_mathlib`	—	—
`vadd_def` 📖	mathematical	—	`HVAdd.hVAdd` `instHVAdd` `VAdd` `map`	—	—
`vadd_mk` 📖	mathematical	—	`HVAdd.hVAdd` `instHVAdd` `VAdd`	—	—

---

← Back to Index