mk_surjective — Mathlib

English

The canonical map mk rels is surjective; every element of the presented group is the image of some word in the free group.

Русский

Каноническое отображение mk rels сюръективно; каждый элемент представленной группы является образом некоторого слова в свободной группе.

LaTeX

$$$\operatorname{Im}(\mathrm{mk}_{\mathrm{rels}}) = \mathrm{PresentedGroup}(\mathrm{rels})$$$

Lean4

theorem mk_surjective (rels : Set (FreeGroup α)) : Function.Surjective <| mk rels :=
  QuotientGroup.mk_surjective

Похожие утверждения