Theorem CategoryTheory.Iso.map_inv_hom_id_eval_app

Modification history