Theorem CategoryTheory.Equivalence.invFunIdAssoc_hom_app

Modification history