:: deftheorem DefDihedral defines Dihedral_group GROUP_24:def 7 :
for n being non zero ExtNat
for b₂ being strict Group holds
( b₂ = Dihedral_group n iff ( ( n = +infty implies b₂ = semidirect_product (INT.Group,(INT.Group 2),(inversions INT.Group)) ) & ( n <> +infty implies ex n1 being non zero Nat st
( n = n1 & b₂ = semidirect_product ((INT.Group n1),(INT.Group 2),(inversions (INT.Group n1))) ) ) ) );