let G be finite Group; :: thesis: for p being prime Nat
for a being Element of G st G is p -group & expon (G,p) = 2 & ord a = p |^ 2 holds
G is commutative
let p be prime Nat; :: thesis: for a being Element of G st G is p -group & expon (G,p) = 2 & ord a = p |^ 2 holds
G is commutative
let a be Element of G; :: thesis: ( G is p -group & expon (G,p) = 2 & ord a = p |^ 2 implies G is commutative )
assume that
A1: ( G is p -group & expon (G,p) = 2 ) and
A2: ord a = p |^ 2 ; :: thesis: G is commutative
card G = p |^ 2 by A1, Def2;
then G is cyclic by A2, GR_CY_1:19;
hence G is commutative ; :: thesis: verum