basic): add lemmas related to map, comap, normalizer (#11637)

Commit

3 years ago

feat(group_theory/subgroup/basic): add lemmas related to map, comap, normalizer (#11637) which are useful when `H < K < G` and one needs to move from `subgroup G` to `subgroup K`

Author

nomeata

Parents

2b257230

mathlib 5472f0a7 - feat(group_theory/subgroup/basic): add lemmas related to map, comap, normalizer (#11637)

mathlib
5472f0a7 - feat(group_theory/subgroup/basic): add lemmas related to map, comap, normalizer (#11637)