Documentation Verification Report

Sum

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

Statistics

Metric	Count
Definitions `instAddAction`, `instMulAction`, `instSMul`, `instVAdd`	4
Theorems `FaithfulSMulLeft`, `FaithfulSMulRight`, `FaithfulVAddLeft`, `FaithfulVAddRight`, `instIsCentralScalar`, `instIsCentralVAdd`, `instIsScalarTower`, `instSMulCommClass`, `instVAddCommClass`, `smul_def`, `smul_inl`, `smul_inr`, `smul_swap`, `vadd_def`, `vadd_inl`, `vadd_inr`, `vadd_swap`	17
Total	21

Sum

Definitions

Name	Category	Theorems
`instAddAction` 📖	CompOp	—
`instMulAction` 📖	CompOp	—
`instSMul` 📖	CompOp	9 math math: `FaithfulSMulLeft`, `smul_inl`, `instSMulCommClass`, `smul_inr`, `FaithfulSMulRight`, `instIsCentralScalar`, `smul_def`, `smul_swap`, `instIsScalarTower`
`instVAdd` 📖	CompOp	8 math math: `vadd_inr`, `FaithfulVAddRight`, `instVAddCommClass`, `vadd_def`, `vadd_swap`, `instIsCentralVAdd`, `vadd_inl`, `FaithfulVAddLeft`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`FaithfulSMulLeft` 📖	mathematical	—	`FaithfulSMul` `instSMul`	—	`FaithfulSMul.eq_of_smul_eq_smul`
`FaithfulSMulRight` 📖	mathematical	—	`FaithfulSMul` `instSMul`	—	`FaithfulSMul.eq_of_smul_eq_smul`
`FaithfulVAddLeft` 📖	mathematical	—	`FaithfulVAdd` `instVAdd`	—	`FaithfulVAdd.eq_of_vadd_eq_vadd`
`FaithfulVAddRight` 📖	mathematical	—	`FaithfulVAdd` `instVAdd`	—	`FaithfulVAdd.eq_of_vadd_eq_vadd`
`instIsCentralScalar` 📖	mathematical	—	`IsCentralScalar` `instSMul` `MulOpposite`	—	`IsCentralScalar.op_smul_eq_smul`
`instIsCentralVAdd` 📖	mathematical	—	`IsCentralVAdd` `instVAdd` `AddOpposite`	—	`IsCentralVAdd.op_vadd_eq_vadd`
`instIsScalarTower` 📖	mathematical	—	`IsScalarTower` `instSMul`	—	`smul_assoc`
`instSMulCommClass` 📖	mathematical	—	`SMulCommClass` `instSMul`	—	`SMulCommClass.smul_comm`
`instVAddCommClass` 📖	mathematical	—	`VAddCommClass` `instVAdd`	—	`VAddCommClass.vadd_comm`
`smul_def` 📖	mathematical	—	`instSMul`	—	—
`smul_inl` 📖	mathematical	—	`instSMul`	—	—
`smul_inr` 📖	mathematical	—	`instSMul`	—	—
`smul_swap` 📖	mathematical	—	`instSMul`	—	—
`vadd_def` 📖	mathematical	—	`HVAdd.hVAdd` `instHVAdd` `instVAdd`	—	—
`vadd_inl` 📖	mathematical	—	`HVAdd.hVAdd` `instHVAdd` `instVAdd`	—	—
`vadd_inr` 📖	mathematical	—	`HVAdd.hVAdd` `instHVAdd` `instVAdd`	—	—
`vadd_swap` 📖	mathematical	—	`HVAdd.hVAdd` `instHVAdd` `instVAdd`	—	—

---

← Back to Index