basic): add lemmas about `subgroup.map` (#17894)

Commit

3 years ago

feat(group_theory/subgroup/basic): add lemmas about `subgroup.map` (#17894) Add lemmas about comparison of `map f H` and `map f K` that don't assume `injective f`.

Author

urkud

Parents

a5c51665

mathlib3 2be0e5fd - feat(group_theory/subgroup/basic): add lemmas about `subgroup.map` (#17894)

mathlib3
2be0e5fd - feat(group_theory/subgroup/basic): add lemmas about `subgroup.map` (#17894)