of — Mathlib · SciLib

English

The map of a generator x ∈ α to the presented group is the class of FreeGroup.of x.

Русский

Образ генератора x ∈ α в представленной группе есть класс образа FreeGroup.of x.

LaTeX

$$$\mathrm{of} : \alpha \to \mathrm{PresentedGroup}(\mathrm{rels}),\quad \mathrm{of}(x) = [\mathrm{FreeGroup}.of(x)].$$$

Lean4

/-- `of` is the canonical map from `α` to a presented group with generators `x : α`. The term `x` is
mapped to the equivalence class of the image of `x` in `FreeGroup α`. -/
def of {rels : Set (FreeGroup α)} (x : α) : PresentedGroup rels :=
  mk rels (FreeGroup.of x)

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