@MISC{GR_FREE0.MIZ,
  AUTHOR = {Koch, Sebastian},
  TITLE = {Free Product of Groups},
  SECTION1 = {Preliminaries},
  SECTION2 = {Free Product of Groups},
  SECTION3 = {Additional Definitions},
  DAY = {27},
  MONTH = {April},
  YEAR = {2025},
  ADDRESS1 = {Germany\\\href{mailto:fly.high.android@gmail.com}{fly.high.android@gmail.com}},
  SUMMARY = {In this article the free product of groups is formalized in the Mizar system.},
  INTRODUCTION = {The concept of free groups and the free product of groups is widely known, cf. 
  \cite{Armstrong:1997}, \cite{Kargapolov:1979}, \cite{Robinson:1995} for example.
  However, a formalization in the Mizar system (cf. \cite{BancerekJAR:2018}, \cite{FourDecades}) has not taken place until now.
  This article was primarily written as a necessary precursor to the formalization of the Seifert-Van Kampen theorem, hence the formalization
  loosely follows that of \cite{Hatcher:2002} and doesn't go into much detail about the properties of the free product or free groups.\par
  After the preliminaries the \emph{free atoms} of a family of groups $\{G_i\}_{i\in I}$ are introduced: 
  they are the set of all pairs of the form $(i,g)$
  with $i\in I$ and $g\in G_i$. This choice allows for the $G_i$ to have non-empty intersections with each other, or all be the same even.
  The typical reduction relation for free products is then defined on the set of all finite sequences of free atoms.
  Afterwards the free product naturally appears as the quotient of the finite sequences of free atoms 
   and the equivalence closure of the reduction relation.}}

@Article{BancerekJAR:2018,
  author={Bancerek, Grzegorz and Byli{\'{n}}ski, Czes{\l}aw and Grabowski, Adam and Korni{\l}owicz, Artur and Matuszewski, Roman and Naumowicz, Adam and P{\k{a}}k, Karol},
  title={The Role of the {M}izar {M}athematical {L}ibrary for Interactive Proof Development in {M}izar},
  journal={Journal of Automated Reasoning},
  year={2018},
  volume={61},
  number={1},
  pages={9--32},
  doi={10.1007/s10817-017-9440-6},
  url={https://doi.org/10.1007/s10817-017-9440-6}
}
@Article{FourDecades,
  author={Grabowski, Adam and Korni{\l}owicz, Artur and Naumowicz, Adam},
  title={Four Decades of {M}izar},
  journal={Journal of Automated Reasoning},
  year={2015},
  volume={55},
  number={3},
  pages={191--198},
  issn={1573-0670},
  doi={10.1007/s10817-015-9345-1}
}
@book{Hatcher:2002,
  TITLE = {Algebraic Topology},
  AUTHOR = {Hatcher, Allen},
  YEAR = {2001},
  PAGES = {XII, 551 p.},
  URL = {https://pi.math.cornell.edu/~hatcher/AT/AT+.pdf}
}
@book{Armstrong:1997,
  title={Groups and Symmetry},
  author={Armstrong, M.A.},
  isbn={9780387966755},
  series={Undergraduate Texts in Mathematics},
  pages={XI, 187 p.},
  url={https://link.springer.com/book/10.1007/978-1-4757-4034-9},
  year={1997},
  publisher={Springer New York}
}
@book{Kargapolov:1979,
  title={Fundamentals of the Theory of Groups},
  author={Kargapolov, M.I. and Merzljakov, J.I.},
  series={Graduate Texts in Mathematics},
  year={1979},
  pages={XVIII, 203 p.},
  publisher={Springer New York},
  url={https://link.springer.com/book/9781461299660}
}

@book{Robinson:1995,
  title={A Course in the Theory of Groups},
  author={Robinson, Derek J.S.},
  series={Graduate Texts in Mathematics},
  year={1995},
  pages={XVII, 502 p.},
  publisher={Springer New York},
  url={https://link.springer.com/book/10.1007/978-1-4419-8594-1}
}