Mathlib Map

Theorems · Inductive type · combinatorics

Quiver.Total

(V : Type u) → [Quiver V] → Type (max u v)

Total V is the type of _all_ arrows of V.

Defined in
Mathlib.Combinatorics.Quiver.Subquiver
Cited by
6 results in Mathlib
Foundations
Depth 1 from the axioms · uses no axioms
Assumes
Quiver
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Quiver.Total.hom · cited by 3Total.homQuiver.Total.left · cited by 2Total.leftQuiver.Total.right · cited by 2Total.rightQuiver.Total.casesOn · cited by 1Total.casesOnQuiver.Total.ext · cited by 1Total.extQuiver.Total.mk.inj · cited by 1mk.injQuiver.Total.mk.noConfusion · cited by 1mk.noConfusionQuiver.wideSubquiverEquivSetTotal · cited by 1Quiver.wideSubquiverEquiv…IsFreeGroupoid.SpanningTree.endIsFree · cited by 0SpanningTree.endIsFreeQuiver.Total.ctorIdx · cited by 0Total.ctorIdxQuiver.Total.ext_iff · cited by 0Total.ext_iffQuiver.Total.noConfusion · cited by 0Total.noConfusionQuiver.Total.noConfusionType · cited by 0Total.noConfusionTypeQuiver.Total.mk.injEq · cited by 0mk.injEqQuiver.Total.recOn · cited by 0Total.recOnQuiver · cited by 405QuiverQuiver.TotalCITED BYCITES

Cites1

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Quiverstatement · cited by 405

Cited by16

Results whose statement or proof uses this declaration.