:: deftheorem DefInversions defines inversions GROUP_24:def 6 :
for G being strict commutative Group
for b₂ being Function of (INT.Group 2),(AutGroup G) holds
( b₂ = inversions G iff ( b₂ . 0 = id G & b₂ . 1 = inverse_op G ) );