Theorem CategoryTheory.Iso.map_inv_hom_id

Modification history