mathlib

18dc1a18 - feat(group_theory/p_group): p-groups are preserved by isomorphisms (#9203)

feat(group_theory/p_group): p-groups are preserved by isomorphisms (#9203) Adds three lemmas about transporting `is_p_group` across injective, surjective, and bijective homomorphisms. Co-authored-by: tb65536 <tb65536@users.noreply.github.com>