mathlib

5a1cbe36 - feat(linear_algebra,algebra,group_theory): miscellaneous lemmas linking some additive monoid and module operations (#11525)

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`.