mathlib3
d3b345df - feat(group_theory/p_group): Bottom subgroup is a p-group (#9190)

Commit

4 years ago

feat(group_theory/p_group): Bottom subgroup is a p-group (#9190) The bottom subgroup is a p-group. Name is consistent with `is_p_group.of_card`

Author

tb65536

Parents