Commit 2022-10-05 09:33 7c1d0d8e

View on Github →

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

Estimated changes

Modified src/algebra/module/equiv.lean

modified theorem linear_equiv.self_trans_symm

modified theorem linear_equiv.symm_trans_self

Modified src/linear_algebra/basic.lean

added def submodule.order_iso_map_comap

added theorem submodule.order_iso_map_comap_apply'

added theorem submodule.order_iso_map_comap_symm_apply'

Modified src/ring_theory/ideal/basic.lean

Modified src/ring_theory/simple_module.lean

added theorem is_simple_module.congr

added theorem is_simple_module_iff_is_coatom

added theorem linear_map.is_coatom_ker_of_surjective