mathlib

b091c3fb - feat(algebra/direct_sum): the submodules of an internal direct sum satisfy `supr A = ⊤` (#8274)

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.