[Merged by Bors] - chore(Algebra/Category/ModuleCat): rename ModuleCat.asHom to ModuleCat.ofHom#19705
Closed
Vierkantor wants to merge 1 commit intomasterfrom ModuleCat.asHom-to-ofHom
+70-70
ModuleCat.asHom to ModuleCat.ofHom#19705