mathlib3

eb203909 - refactor(group_theory/p_group): Move lemmas to is_p_group namespace (#9188)

refactor(group_theory/p_group): Move lemmas to is_p_group namespace (#9188) Moves `card_modeq_card_fixed_points`, `nonempty_fixed_point_of_prime_not_dvd_card`, and `exists_fixed_point_of_prime_dvd_card_of_fixed_point` to the `is_p_group` namespace. I think this simplifies things, since they already had explicit `hG : is_p_group G` hypotheses anyway.