Commit 2021-10-01 15:54 102ce303

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,