@ARTICLE{GROUP_24.MIZ,
  AUTHOR = {Nelson, Alexander M.},
  TITLE = {Semidirect Products of Groups},
  ACKNOWLEDGEMENT = {The author would like to dedicate this to his grandparents. ``There are only two precious things on earth: the first is love; the second, a long way behind it, is intelligence.''},
  SECTION1 = {Preliminaries},
  SECTION2 = {Automorphism Group Results},
  SECTION3 = {Semidirect Products of Groups},
  SECTION4 = {Complementary Subgroups},
  SECTION5 = {Appendix 1: Results about Cyclic Groups},
  SECTION6 = {Appendix 2: Dihedral Groups},
  DAY = {27},
  MONTH = {May},
  YEAR = {2025},
  ADDRESS1 = {Los Angeles, California, United States of America},
  MSC = {20E22 20E99},
  KEYWORDS = {semidirect product; subgroup complement; dihedral group},
  SUMMARY = {We formalize the semidirect product of groups in Mizar,
      following \S10 of Aschbacher~\cite{aschbacher2000finite}.
      We also prove the universal property for semidirect products as
      found in Bourbaki~\cite[III \S2.10]{bourbaki2013general} Proposition 27.
      In an appendix, we define the dihdral group of the regular
      $n$-gon and the infinite dihedral group.}}


