CancelIso

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

Statistics

Metric	Count
Definitions cancelIsoSimproc, tryCancelPair, cancelIso	3
Theorems hom_inv_id_of_eq, hom_inv_id_of_eq_assoc	2
Total	5

Mathlib.Tactic.CategoryTheory.CancelIso

Definitions

Name	Category	Theorems
cancelIsoSimproc 📖	CompOp	—
tryCancelPair 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hom_inv_id_of_eq 📖	mathematical	CategoryTheory.inv	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id	—	CategoryTheory.IsIso.hom_inv_id
hom_inv_id_of_eq_assoc 📖	mathematical	CategoryTheory.inv	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.IsIso.hom_inv_id_assoc

(root)

Definitions

Name	Category	Theorems
cancelIso 📖	CompOp	—

---

← Back to Index