Theorem CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.hasLeftKanExtension

Modification history