Free product of groups

DOI10.2478/FORMA-2025-0004MaRDI QIDQ6840592zbMATH OpenFDO

Authors Sebastian Koch

Publication date 23 March 2026

Published in Formalized Mathematics (Search for Journal in Brave)

Copyright license Creative Commons Attribution-ShareAlike 4.0 International

Full work available at URL https://doi.org/10.2478/FORMA-2025-0004

zbMATH Keywords

free groupfree productfree-abelian group

Mathematics Subject Classification ID

Free products of groups, free products with amalgamation, Higman-Neumann-Neumann extensions, and generalizations (20E06) Formalization of mathematics in connection with theorem provers (68V20)

Cites work

• Formalizing free groups in Isabelle/HOL: the Nielsen-Schreier theorem and the conjugacy problem
• Four decades of \textsc{Mizar}. Foreword
• Group cohomology in the Lean community library
• scientific article; zbMATH DE number 3875506 (Why is no real title available?)
• scientific article; zbMATH DE number 42440 (Why is no real title available?)
• Internal direct products and the universal property of direct product groups
• The directed Van Kampen theorem in Lean
• The role of the Mizar mathematical library for interactive proof development in Mizar

This page was built for publication: Free product of groups

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6840592)