mk_eq_one_iff — Mathlib

English

An element x of the free group maps to the identity in the presented group exactly when x lies in the normal closure of rels.

Русский

Элемент x свободной группы отображается в единицу в представленной группе тогда и только тогда, когда x принадлежит нормальному замыканию rels.

LaTeX

$$$\mathrm{mk}_{\mathrm{rels}}(x) = 1 \iff x \in \operatorname{normalClosure}(\mathrm{rels}).$$$

Lean4

theorem mk_eq_one_iff {rels : Set (FreeGroup α)} {x : FreeGroup α} : mk rels x = 1 ↔ x ∈ Subgroup.normalClosure rels :=
  QuotientGroup.eq_one_iff _

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