Commit 2021-04-06 05:50 b05affbd

View on Github →

chore(group_theory/subgroup): translate map comap lemmas from linear_map (#6979) Introduce the analogues of linear_map.map_comap_eq and linear_map.comap_map_eq to subgroups. Also add subgroup.map_eq_comap_of_inverse which is a translation of set.image_eq_preimage_of_inverse.

Estimated changes

Modified src/group_theory/subgroup.lean

added theorem subgroup.comap_injective

added theorem subgroup.comap_map_eq

added theorem subgroup.comap_map_eq_self

added theorem subgroup.comap_map_eq_self_of_injective

added theorem subgroup.comap_mono

added theorem subgroup.ker_le_comap

added theorem subgroup.le_comap_map

added theorem subgroup.map_comap_eq

added theorem subgroup.map_comap_eq_self

added theorem subgroup.map_comap_eq_self_of_surjective

added theorem subgroup.map_comap_le

added theorem subgroup.map_eq_comap_of_inverse

added theorem subgroup.map_injective

added theorem subgroup.map_le_range

added theorem subgroup.map_mono