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







leanprover-community/mathlib,leanprover-community/mathlib