Theorem CategoryTheory.Iso.unop_hom_inv_id_app

Modification history