Theorem CategoryTheory.Iso.map_hom_inv_id

Modification history