mathlib3
f7135f17 - feat(group_theory/p_group): `is_p_group` is preserved by `subgroup.comap` (#9277)

Commit

4 years ago

feat(group_theory/p_group): `is_p_group` is preserved by `subgroup.comap` (#9277) If `H` is a p-subgroup, then `H.comap f` is a p-subgroup, assuming that `f` is injective.

Author

tb65536

Parents

965e457f

mathlib3 f7135f17 - feat(group_theory/p_group): `is_p_group` is preserved by `subgroup.comap` (#9277)

mathlib3
f7135f17 - feat(group_theory/p_group): `is_p_group` is preserved by `subgroup.comap` (#9277)