Theorem CategoryTheory.Iso.inv_comp_eq_id

Modification history