Theorem CategoryTheory.hom_inv_id_apply

Modification history