Theorem CategoryTheory.IsIso.hom_inv_id_assoc

Modification history