Theorem CategoryTheory.Equivalence.counitInv_app_functor

Modification history