:: deftheorem Def3 defines -commutative-group-like GROUPP_1:def 3 :
for p being Nat
for G being Group holds
( G is p -commutative-group-like iff for a, b being Element of G holds (a * b) |^ p = (a |^ p) * (b |^ p) );