| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
Free Groups
| Title: | Free Groups |
| Author: | Joachim Breitner (joachim /at/ cis /dot/ upenn /dot/ edu) |
| Submission date: | 2010-06-24 |
| 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. |
| Change history: | [2011-12-11]: Added the Ping Pong Lemma. |
| BibTeX: |
@article{Free-Groups-AFP,
author = {Joachim Breitner},
title = {Free Groups},
journal = {Archive of Formal Proofs},
month = jun,
year = 2010,
note = {\url{http://isa-afp.org/entries/Free-Groups.html},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
| Depends on: | Applicative_Lifting |
| Status: [ok] | This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |