Theorem CategoryTheory.Iso.comp_inv_eq_id

Modification history