Def CategoryTheory.Functor.Elements.yonedaCocone

Modification history

2026-10-31 10:05

Mathlib/CategoryTheory/Functor/KanExtension/DenseAtYoneda.lean

refactor(CategoryTheory): colimits of representable presheaves (#42816) …

Added CategoryTheory.Functor.Elements.yonedaCocone View on Github →