Commit 2022-01-18 17:08 5a1cbe36

feat(linear_algebra,algebra,group_theory): miscellaneous lemmas linking some additive monoid and module operations (#11525) This adds:

• submodule.map_to_add_submonoid
• submodule.sup_to_add_submonoid
• submodule.supr_to_add_submonoid As well as some missing add_submonoid lemmas copied from the submodule API:
• add_submonoid.closure_singleton_le_iff_mem
• add_submonoid.mem_supr
• add_submonoid.supr_eq_closure Finally, it generalizes some indices in supr and infi lemmas from Type* to Sort*. This is pre-work for removing a redundant hypothesis from submodule.mul_induction_on.