:: deftheorem defines Adjoint_pGroup BCIALG_4:def 5 :
for X being p-Semisimple BCI-algebra
for b₂ being strict AbGroup holds
( b₂ = Adjoint_pGroup X iff ( the carrier of b₂ = the carrier of X & ( for x, y being Element of X holds the addF of b₂ . (x,y) = x \ ((0. X) \ y) ) & 0. b₂ = 0. X ) );