Skip to content

Commit

Permalink
doc(group_theory/free_group): fix linkify (#11565)
Browse files Browse the repository at this point in the history
  • Loading branch information
ericrbg committed Jan 20, 2022
1 parent 0bb4272 commit 656372c
Showing 1 changed file with 9 additions and 8 deletions.
17 changes: 9 additions & 8 deletions src/group_theory/free_group.lean
Expand Up @@ -15,18 +15,19 @@ functor from groups to types, see `algebra/category/Group/adjunctions`.
## Main definitions
* `free_group`: the free group associated to a type `α` defined as the words over `a : α × bool `
* `free_group`: the free group associated to a type `α` defined as the words over `a : α × bool`
modulo the relation `a * x * x⁻¹ * b = a * b`.
* `mk`: the canonical quotient map `list (α × bool) → free_group α`.
* `of`: the canoical injection `α → free_group α`.
* `lift f`: the canonical group homomorphism `free_group α →* G` given a group `G` and a
function `f : α → G`.
* `free_group.mk`: the canonical quotient map `list (α × bool) → free_group α`.
* `free_group.of`: the canoical injection `α → free_group α`.
* `free_group.lift f`: the canonical group homomorphism `free_group α →* G`
given a group `G` and a function `f : α → G`.
## Main statements
* `church_rosser`: The Church-Rosser theorem for word reduction (also known as Newman's diamond
lemma).
* `free_group_unit_equiv_int`: The free group over the one-point type is isomorphic to the integers.
* `free_group.church_rosser`: The Church-Rosser theorem for word reduction
(also known as Newman's diamond lemma).
* `free_group.free_group_unit_equiv_int`: The free group over the one-point type
is isomorphic to the integers.
* The free group construction is an instance of a monad.
## Implementation details
Expand Down

0 comments on commit 656372c

Please sign in to comment.