mathlib3
b05affbd - chore(group_theory/subgroup): translate map comap lemmas from linear_map (#6979)

Commit
5 years ago
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`. Co-authored-by: Adrián Doña Mateo <43966663+AdrianDoM@users.noreply.github.com>
Author
Parents
Loading