mathlib3

7c1d0d8e - misc(linear_algebra, ring_theory): more simple facts about `is_simple_module` and order on submodules (#16786)

misc(linear_algebra, ring_theory): more simple facts about `is_simple_module` and order on submodules (#16786) The main result is `is_coatom_ker_of_surjective`, but I added various miscellaneous lemmas along the way