Commit 2021-07-13 17:32 b091c3fb

feat(algebra/direct_sum): the submodules of an internal direct sum satisfy supr A = ⊤ (#8274) The main results here are:

• direct_sum.add_submonoid_is_internal.supr_eq_top
• direct_sum.submodule_is_internal.supr_eq_top Which we prove using the new lemmas
• add_submonoid.supr_eq_mrange_dfinsupp_sum_add_hom
• submodule.supr_eq_range_dfinsupp_lsum There's no obvious way to reuse the proofs between the two, but thankfully all four proofs are quite short anyway. These should aid in shortening #8246.