Documentation Verification Report

Option

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

Statistics

Metric	Count
Definitions `VAdd`, `instMulAction`, `instSMul_mathlib`	3
Theorems `instFaithfulSMul`, `instFaithfulVAdd`, `instIsCentralScalar`, `instIsCentralVAdd`, `instIsScalarTowerOfSMul`, `instSMulCommClass`, `instVAddAssocClassOfVAdd`, `instVAddCommClass`, `smul_def`, `smul_none`, `smul_some`, `vadd_def`, `vadd_none`, `vadd_some`	14
Total	17

Option

Definitions

Name	Category	Theorems
`VAdd` 📖	CompOp	7 math math: `vadd_some`, `instVAddCommClass`, `instFaithfulVAdd`, `instVAddAssocClassOfVAdd`, `vadd_def`, `instIsCentralVAdd`, `vadd_none`
`instMulAction` 📖	CompOp	—
`instSMul_mathlib` 📖	CompOp	7 math math: `smul_some`, `instIsScalarTowerOfSMul`, `instIsCentralScalar`, `instSMulCommClass`, `instFaithfulSMul`, `smul_none`, `smul_def`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instFaithfulSMul` 📖	mathematical	—	`FaithfulSMul` `instSMul_mathlib`	—	`FaithfulSMul.eq_of_smul_eq_smul`
`instFaithfulVAdd` 📖	mathematical	—	`FaithfulVAdd` `VAdd`	—	`FaithfulVAdd.eq_of_vadd_eq_vadd`
`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`	—	`Function.Commute.option_map` `SMulCommClass.smul_comm`
`instVAddAssocClassOfVAdd` 📖	mathematical	—	`VAddAssocClass` `VAdd`	—	`vadd_assoc`
`instVAddCommClass` 📖	mathematical	—	`VAddCommClass` `VAdd`	—	`Function.Commute.option_map` `VAddCommClass.vadd_comm`
`smul_def` 📖	mathematical	—	`instSMul_mathlib`	—	—
`smul_none` 📖	mathematical	—	`instSMul_mathlib`	—	—
`smul_some` 📖	mathematical	—	`instSMul_mathlib`	—	—
`vadd_def` 📖	mathematical	—	`HVAdd.hVAdd` `instHVAdd` `VAdd`	—	—
`vadd_none` 📖	mathematical	—	`HVAdd.hVAdd` `instHVAdd` `VAdd`	—	—
`vadd_some` 📖	mathematical	—	`HVAdd.hVAdd` `instHVAdd` `VAdd`	—	—

---

← Back to Index