English
Let α be a type and rels a set of relations among generators. The presented group is the quotient of the free group on α by the normal closure of rels, i.e., the group generated by symbols x ∈ α with the relations prescribed by rels.
Русский
Пусть α — множество генераторов, rels — множество отношений между ними. Представленная группа есть фактор-группа свободной группы на α по нормальному замыканию rels; она порождается элементами x из α с отношениями, заданными rels.
LaTeX
$$$\mathrm{PresentedGroup}(\mathrm{rels}) = \mathrm{FreeGroup}(\alpha) \big/ \operatorname{normalClosure}(\mathrm{rels})$$$
Lean4
/-- Given a set of relations, `rels`, over a type `α`, `PresentedGroup` constructs the group with
generators `x : α` and relations `rels` as a quotient of `FreeGroup α`. -/
def PresentedGroup (rels : Set (FreeGroup α)) :=
FreeGroup α ⧸ Subgroup.normalClosure rels
