Theorem CategoryTheory.Functor.IsDense.leftKanExtensionUnit_leftKanExtensionIso_hom

Modification history

2026-05-26 05:31
Mathlib/CategoryTheory/Functor/KanExtension/Dense.lean
chore(CategoryTheory/Functor): more API for dense functors (#39845) …
Added CategoryTheory.Functor.IsDense.leftKanExtensionUnit_leftKanExtensionIso_homView on Github →