# Commit 2022-05-24 14:54 28f7172e

View on Github →refactor(algebra/direct_sum/basic): use the new polymorphic subobject API (#14341) This doesn't let us deduplicate the lattice lemmas, but does eliminate the duplicate instances and definitions! This merges:

`direct_sum.add_submonoid_is_internal`

,`direct_sum.add_subgroup_is_internal`

,`direct_sum.submodule_is_internal`

into`direct_sum.is_internal`

`direct_sum.add_submonoid_coe`

,`direct_sum.add_subgroup_coe`

into`direct_sum.coe_add_monoid_hom`

`direct_sum.add_submonoid_coe_ring_hom`

,`direct_sum.add_subgroup_coe_ring_hom`

into`direct_sum.coe_ring_hom`

`add_submonoid.gsemiring`

,`add_subgroup.gsemiring`

,`submodule.gsemiring`

into`set_like.gsemiring`

`add_submonoid.gcomm_semiring`

,`add_subgroup.gcomm_semiring`

,`submodule.gcomm_semiring`

into`set_like.gcomm_semiring`

Renames`direct_sum.submodule_coe`

into`direct_sum.coe_linear_map`

`direct_sum.submodule_coe_alg_hom`

into `direct_sum.coe_alg_hom And adds:`set_like.gnon_unital_non_assoc_semiring`

, now that it doesn't need to be repeated three times! A large number of related lemmas are also renamed to match the new definition names. This was what originally motivated the`set_like`

typeclass; thanks to @Vierkantor for doing the subobject follow up I never got around to!