feat(algebra/category): show categorical image in Module agrees with range (#12605)
feat(algebra/category): show categorical image in Module agrees with range (#12605)

This just follows the existing code for the same fact in `AddCommGroup`.

This PR is preparing for a better API for homological calculations in `Module R`.





Co-authored-by: Scott Morrison <63f04b4d96235eb042cc46d94f14d241d2a26722@gmail.com>

leanprover-community/mathlib,leanprover-community/mathlib