Coequalizer

📁 Source: Mathlib/Logic/Function/Coequalizer.lean

Statistics

Metric	Count
Definitions Coequalizer, desc, mk	3
Theorems condition, desc_mk, mk_surjective	3
Total	6

Function

Definitions

Name	Category	Theorems
Coequalizer 📖	CompOp	5 math math: CategoryTheory.Limits.Types.coequalizerIso_quot_comp_inv, CategoryTheory.Limits.Types.coequalizerIso_π_comp_hom_apply, CategoryTheory.Limits.Types.coequalizerIso_quot_comp_inv_apply, CategoryTheory.Limits.Types.coequalizerIso_π_comp_hom, Coequalizer.mk_surjective

Function.Coequalizer

Definitions

Name	Category	Theorems
desc 📖	CompOp	1 math math: desc_mk
mk 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
condition 📖	—	—	—	—	—
desc_mk 📖	mathematical	—	desc	—	—
mk_surjective 📖	mathematical	—	Function.Coequalizer	—	—

---

← Back to Index