mathlib3

9b000466 - chore(algebra,group_theory,right_theory,linear_algebra): add missing lemmas (#8948)

chore(algebra,group_theory,right_theory,linear_algebra): add missing lemmas (#8948) This adds: * `sub{group,ring,semiring}.map_id` * `submodule.add_mem_sup` * `submodule.map_add_le` And moves `submodule.sum_mem_supr` and `submodule.sum_mem_bsupr` to an earlier file.