:: deftheorem Def1 defines MultGroup UNIROOTS:def 1 :
for R being Skew-Field
for b₂ being strict Group holds
( b₂ = MultGroup R iff ( the carrier of b₂ = NonZero R & the multF of b₂ = the multF of R || the carrier of b₂ ) );