feat(group_theory/p_group): is_p_group is preserved by `subgroup.ma…

…p` (#9276)

If `H` is a p-subgroup, then `H.map f` is a p-subgroup.

src/group_theory/p_group.lean

@@ -200,4 +200,11 @@ lemma to_sup_of_normal_left' {H K : subgroup G} (hH : is_p_group p H) (hK : is_p
   (hHK : K ≤ H.normalizer) : is_p_group p (H ⊔ K : subgroup G) :=
 (congr_arg (λ H : subgroup G, is_p_group p H) sup_comm).mp (to_sup_of_normal_right' hK hH hHK)
 
+lemma map {H : subgroup G} (hH : is_p_group p H) {K : Type*} [group K]
+  (ϕ : G →* K) : is_p_group p (H.map ϕ) :=
+begin
+  rw [←H.subtype_range, monoid_hom.map_range],
+  exact hH.of_surjective (ϕ.restrict H).range_restrict (ϕ.restrict H).range_restrict_surjective,
+end
+
 end is_p_group

src/group_theory/subgroup.lean

@@ -1373,6 +1373,10 @@ monoid_hom.mk' (λ g, ⟨f g, ⟨g, rfl⟩⟩) $ λ a b, by {ext, exact f.map_mu
 @[simp, to_additive]
 lemma coe_range_restrict (f : G →* N) (g : G) : (f.range_restrict g : N) = f g := rfl
 
+@[to_additive]
+lemma range_restrict_surjective (f : G →* N) : function.surjective f.range_restrict :=
+λ ⟨_, g, rfl⟩, ⟨g, rfl⟩
+
 @[to_additive]
 lemma map_range (g : N →* P) (f : G →* N) : f.range.map g = (g.comp f).range :=
 by rw [range_eq_map, range_eq_map]; exact (⊤ : subgroup G).map_map g f