Basic
📁 Source: Mathlib/Tactic/CategoryTheory/Coherence/Basic.lean
Statistics
| Metric | Count |
|---|---|
| 4 | |
| 2 | |
| Total | 6 |
Mathlib.Tactic.BicategoryLike
Definitions
| Name | Category | Theorems |
|---|---|---|
main 📖 | CompOp | — |
normalForm 📖 | CompOp | — |
ofNormalizedEq 📖 | CompOp | — |
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
mk_eq 📖 | — | — | — | — | — |
mk_eq_of_cons 📖 | mathematical | — | CategoryTheory.CategoryStruct.comp | — | — |
Mathlib.Tactic.BicategoryLike.List
Definitions
| Name | Category | Theorems |
|---|---|---|
splitEvenOdd 📖 | CompOp | — |
---