:: deftheorem defines Dihedral_group GROUP_24:def 8 :
for n being non zero Nat holds Dihedral_group n = semidirect_product ((INT.Group n),(INT.Group 2),(inversions (INT.Group n)));