Theorem CategoryTheory.Iso.unop_inv_hom_id_app

Modification history