Theorem CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtension.hasRightKanExtension

Modification history