mathlib3

5ba41d8f - feat(algebra/direct_sum): specialize `submodule_is_internal.independent` to add_subgroup (#10108)

feat(algebra/direct_sum): specialize `submodule_is_internal.independent` to add_subgroup (#10108) This adds the lemmas `disjoint.map_order_iso` and `complete_lattice.independent.map_order_iso` (and `iff` versions), and uses them to transfer some results on `submodule`s to `add_submonoid`s and `add_subgroup`s.