Documentation Verification Report

Synonym

📁 Source: Mathlib/Algebra/Order/Group/Action/Synonym.lean

Statistics

Metric	Count
Definitions `instAddAction`, `instAddAction'`, `instMulAction`, `instMulAction'`, `instAddAction`, `instAddAction'`, `instMulAction`, `instMulAction'`	8
Theorems `instIsScalarTower`, `instIsScalarTower'`, `instIsScalarTower''`, `instSMulCommClass`, `instSMulCommClass'`, `instSMulCommClass''`, `instVAddAssocClass`, `instVAddAssocClass'`, `instVAddAssocClass''`, `instVAddCommClass`, `instVAddCommClass'`, `instVAddCommClass''`, `instIsScalarTower`, `instIsScalarTower'`, `instIsScalarTower''`, `instSMulCommClass`, `instSMulCommClass'`, `instSMulCommClass''`, `instVAddAssocClass`, `instVAddAssocClass'`, `instVAddAssocClass''`, `instVAddCommClass`, `instVAddCommClass'`, `instVAddCommClass''`	24
Total	32

Lex

Definitions

Name	Category	Theorems
`instAddAction` 📖	CompOp	—
`instAddAction'` 📖	CompOp	—
`instMulAction` 📖	CompOp	—
`instMulAction'` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsScalarTower` 📖	mathematical	—	`IsScalarTower` `Lex` `instSMul'`	—	—
`instIsScalarTower'` 📖	mathematical	—	`IsScalarTower` `Lex` `instSMul` `instSMul'`	—	—
`instIsScalarTower''` 📖	mathematical	—	`IsScalarTower` `Lex` `instSMul`	—	—
`instSMulCommClass` 📖	mathematical	—	`SMulCommClass` `Lex` `instSMul'`	—	—
`instSMulCommClass'` 📖	mathematical	—	`SMulCommClass` `Lex` `instSMul'`	—	—
`instSMulCommClass''` 📖	mathematical	—	`SMulCommClass` `Lex` `instSMul`	—	—
`instVAddAssocClass` 📖	mathematical	—	`VAddAssocClass` `Lex` `instVAdd'`	—	—
`instVAddAssocClass'` 📖	mathematical	—	`VAddAssocClass` `Lex` `instVAdd` `instVAdd'`	—	—
`instVAddAssocClass''` 📖	mathematical	—	`VAddAssocClass` `Lex` `instVAdd`	—	—
`instVAddCommClass` 📖	mathematical	—	`VAddCommClass` `Lex` `instVAdd'`	—	—
`instVAddCommClass'` 📖	mathematical	—	`VAddCommClass` `Lex` `instVAdd'`	—	—
`instVAddCommClass''` 📖	mathematical	—	`VAddCommClass` `Lex` `instVAdd`	—	—

OrderDual

Definitions

Name	Category	Theorems
`instAddAction` 📖	CompOp	—
`instAddAction'` 📖	CompOp	—
`instMulAction` 📖	CompOp	—
`instMulAction'` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsScalarTower` 📖	mathematical	—	`IsScalarTower` `OrderDual` `instSMul'`	—	—
`instIsScalarTower'` 📖	mathematical	—	`IsScalarTower` `OrderDual` `instSMul` `instSMul'`	—	—
`instIsScalarTower''` 📖	mathematical	—	`IsScalarTower` `OrderDual` `instSMul`	—	—
`instSMulCommClass` 📖	mathematical	—	`SMulCommClass` `OrderDual` `instSMul'`	—	—
`instSMulCommClass'` 📖	mathematical	—	`SMulCommClass` `OrderDual` `instSMul'`	—	—
`instSMulCommClass''` 📖	mathematical	—	`SMulCommClass` `OrderDual` `instSMul`	—	—
`instVAddAssocClass` 📖	mathematical	—	`VAddAssocClass` `OrderDual` `instVAdd'`	—	—
`instVAddAssocClass'` 📖	mathematical	—	`VAddAssocClass` `OrderDual` `instVAdd` `instVAdd'`	—	—
`instVAddAssocClass''` 📖	mathematical	—	`VAddAssocClass` `OrderDual` `instVAdd`	—	—
`instVAddCommClass` 📖	mathematical	—	`VAddCommClass` `OrderDual` `instVAdd'`	—	—
`instVAddCommClass'` 📖	mathematical	—	`VAddCommClass` `OrderDual` `instVAdd'`	—	—
`instVAddCommClass''` 📖	mathematical	—	`VAddCommClass` `OrderDual` `instVAdd`	—	—

---

← Back to Index