mathlib

102ce303 - feat(linear_algebra/direct_sum): `submodule_is_internal_iff_independent_and_supr_eq_top` (#9214)

feat(linear_algebra/direct_sum): `submodule_is_internal_iff_independent_and_supr_eq_top` (#9214) This shows that a grade decomposition into submodules is bijective iff and only iff the submodules are independent and span the whole module. The key proofs are: * `complete_lattice.independent_of_dfinsupp_lsum_injective` * `complete_lattice.independent.dfinsupp_lsum_injective` Everything else is just glue. This replaces parts of #8246, and uses what is probably a similar proof strategy, but without unfolding down to finsets. Unlike the proof there, this requires only `add_comm_monoid` for the `complete_lattice.independent_of_dfinsupp_lsum_injective` direction of the proof. I was not able to find a proof of `complete_lattice.independent.dfinsupp_lsum_injective` with the same weak assumptions, as it is not true! A counter-example is included, Co-authored-by: Hanting Zhang <hantingzhang03@gmail.com>