Theorem CategoryTheory.ForgetEnrichment.homOf_eId

Modification history