Commit 2021-04-19 14:03 829d7733

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.