### Abstract

Free Groups are, in a sense, the most generic kind of group. They are defined over a set of generators with no additional relations in between them. They play an important role in the definition of group presentations and in other fields. This theory provides the definition of Free Group as the set of fully canceled words in the generators. The universal property is proven, as well as some isomorphisms results about Free Groups.

### License

BSD License

### History

December 11, 2011
  Added the Ping Pong Lemma.

### Topics

- Mathematics/Algebra

### Session Free-Groups

- Cancelation
- Generators
- FreeGroups
- UnitGroup
- C2
- Isomorphisms
- PingPongLemma

### Depends on

- Applicative Lifting

### Auto-related entries

- Matroids

## Cite

×

Free-Groups-AFP

    @article{Free-Groups-AFP,
      author  = {Joachim Breitner},
      title   = {Free Groups},
      journal = {Archive of Formal Proofs},
      month   = {June},
      year    = {2010},
      note    = {\url{https://isa-afp.org/entries/Free-Groups.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Dec 11, 2013 : Isabelle2013-2
- Nov 17, 2013 : Isabelle2013-1
- Feb 16, 2013 : Isabelle2013
- May 24, 2012 : Isabelle2012
- Oct 11, 2011 : Isabelle2011-1
- Feb 11, 2011 : Isabelle2011
- Jul 1, 2010 : Isabelle2009-2