Subquiver

📁 Source: Mathlib/Combinatorics/Quiver/Subquiver.lean

Statistics

Metric	Count
Definitions Labelling, Total, hom, left, right, instBotWideSubquiver, instInhabitedLabelling, instInhabitedWideSubquiver, instTopWideSubquiver, wideSubquiverEquivSetTotal, WideSubquiver, quiver, toType, wideSubquiverHasCoeToSort	14
Theorems ext, ext_iff	2
Total	16

Quiver

Definitions

Name	Category	Theorems
Labelling 📖	CompOp	—
Total 📖	CompData	—
instBotWideSubquiver 📖	CompOp	—
instInhabitedLabelling 📖	CompOp	—
instInhabitedWideSubquiver 📖	CompOp	—
instTopWideSubquiver 📖	CompOp	—
wideSubquiverEquivSetTotal 📖	CompOp	—

Quiver.Total

Definitions

Name	Category	Theorems
hom 📖	CompOp	1 math math: ext_iff
left 📖	CompOp	1 math math: ext_iff
right 📖	CompOp	1 math math: ext_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	left right Quiver.Hom hom	—	—	—
ext_iff 📖	mathematical	—	left right Quiver.Hom hom	—	ext

WideSubquiver

Definitions

Name	Category	Theorems
quiver 📖	CompOp	—
toType 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
WideSubquiver 📖	CompOp	—
wideSubquiverHasCoeToSort 📖	CompOp	—

---

← Back to Index