Commit 2024-10-08 08:32 2f790a96

View on Github →

feat(Algebra/Category/ModuleCat/Basic): remove duplicate ofHom (#17476) We keep asHom and use that throughout, since there seems to be no need to keep both around.

Estimated changes

added theorem ModuleCat.asHom_apply
deleted def ModuleCat.ofHom
deleted theorem ModuleCat.ofHom_apply