Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-04 08:16 855613ee

View on Github →

feat(linear_algebra/basic): galois insertion lemmas for map and comap (#8978)

Estimated changes

Modified src/linear_algebra/basic.lean

added theorem submodule.comap_injective_of_surjective

added theorem submodule.comap_le_comap_iff_of_surjective

added theorem submodule.comap_strict_mono_of_surjective

added def submodule.gi_map_comap

added theorem submodule.map_comap_eq_of_surjective

added theorem submodule.map_inf_comap_of_surjective

added theorem submodule.map_infi_comap_of_surjective

added theorem submodule.map_sup_comap_of_surjective

added theorem submodule.map_supr_comap_of_sujective

added theorem submodule.map_surjective_of_surjective