Reassoc

📁 Source: Mathlib/Tactic/CategoryTheory/Reassoc.lean

Statistics

Metric	Count
Definitions categorySimp, reassoc, reassocExpr, reassocExpr', reassocExprHom, registerReassocExpr, toDualOpt, «termReassoc_of%_»	8
Theorems eq_whisker'	1
Total	9

Mathlib.Tactic.Reassoc

Definitions

Name	Category	Theorems
categorySimp 📖	CompOp	—
reassoc 📖	CompOp	—
reassocExpr 📖	CompOp	—
reassocExpr' 📖	CompOp	—
reassocExprHom 📖	CompOp	—
registerReassocExpr 📖	CompOp	—
toDualOpt 📖	CompOp	—
«termReassoc_of%_» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_whisker' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—

---

← Back to Index