one_of_mem — Mathlib

English

If a generator lies in the rels set, its image is the identity in the presented group.

Русский

Если генератор принадлежит rels, его образ равен единице в представленной группе.

LaTeX

$$$\forall x \in \mathrm{rels}, \mathrm{mk}_{\mathrm{rels}}(x) = 1$$$

Lean4

theorem one_of_mem {rels : Set (FreeGroup α)} {x : FreeGroup α} (hx : x ∈ rels) : mk rels x = 1 :=
  mk_eq_one_iff.mpr <| Subgroup.subset_normalClosure hx

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