mathlib
180c7581 - feat(group_theory/p_group): `is_p_group` is preserved by `subgroup.map` (#9276)

Commit

4 years ago

feat(group_theory/p_group): `is_p_group` is preserved by `subgroup.map` (#9276) If `H` is a p-subgroup, then `H.map f` is a p-subgroup.

Author

tb65536

Parents