mathlib3

50b51c5e - refactor(group_theory/is_p_group): Generalize `is_p_group.comap_injective` (#9509)

refactor(group_theory/is_p_group): Generalize `is_p_group.comap_injective` (#9509) `is_p_group.comap_injective` (comap along injective preserves p-groups) can be generalized to `is_p_group.comap_ker_is_p_group` (comap with p-group kernel preserves p-groups). This also simplifies the proof of `is_p_group.to_sup_of_normal_right` Co-authored-by: tb65536 <tb65536@users.noreply.github.com>