mathlib3

1ee8921d - feat(group_theory/p_group): `card G = 1` or `p | card G`. (#17251)

feat(group_theory/p_group): `card G = 1` or `p | card G`. (#17251) The cardinality of a `p`-group is either `1` or divisible by `p` (the latter case includes the infinite case).