Theorem CategoryTheory.Iso.inv_hom_id_app_app

Modification history