mathlib

829d7733 - feat(algebra/module/submodule_lattice): add lemmas for nat submodules (#7221)

feat(algebra/module/submodule_lattice): add lemmas for nat submodules (#7221) This has been suggested by @eric-wieser (who also wrote everything) in #7200. This also: * Merges `span_nat_eq_add_group_closure` and `submodule.span_eq_add_submonoid.closure` which are the same statement into `submodule.span_nat_eq_add_submonoid_closure`, which generalizes the former from `semiring` to `add_comm_monoid`. * Renames `span_int_eq_add_group_closure` to `submodule.span_nat_eq_add_subgroup_closure`, and generalizes it from `ring` to `add_comm_group`. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>