mathlib

40b15f25 - feat(algebra/direct_sum): state what it means for a direct sum to be internal (#7190)

feat(algebra/direct_sum): state what it means for a direct sum to be internal (#7190) The goal here is primarily to tick off the item in undergrad.yml. We'll want some theorems relating this statement to independence / spanning of the submodules, but I'll leave those for someone else to follow-up with. We end up needing three variants of this - one for each of add_submonoids, add_subgroups, and submodules.