Theorem CategoryTheory.Functor.hasLeftExtension_iff_postcomp₁

Modification history

2024-08-12 18:29
Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean
chore: move to v4.11.0-rc2 (new `variable` command) (#15726)
Modified CategoryTheory.Functor.hasLeftExtension_iff_postcomp₁View on Github →
2024-02-11 09:45
Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean
feat(CategoryTheory): the typeclass Functor.HasRightKanExtension (#10384) …
Added CategoryTheory.Functor.hasLeftExtension_iff_postcomp₁View on Github →