mathlib3

d6c002c7 - feat(group_theory/p_group): finite p-groups with different p have coprime orders (#11775)