Commit 2022-05-24 14:54 28f7172e

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!