feat(algebra/direct_sum/module) : coe and internal (#10004)
This extracts the following `def`s from within the various `is_internal` properties:
* `direct_sum.add_submonoid_coe`
* `direct_sum.add_subgroup_coe`
* `direct_sum.submodule_coe`
Packing these into a def makes things more concise, and avoids some annoying elaboration issues.
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: jjaassoonn <jujian.zhang1998@out.com>
