Theorem Rep.mkIso_hom_hom_apply

Modification history