mk_eq_mk_of_mul_inv_mem — Mathlib

English

If x and y are connected by a relator, their images are equal in the presented group.

Русский

Если x и y связаны отношениям rels, их образы равны в представленной группе.

LaTeX

$$$x y^{-1} \in \mathrm{normalClosure}(\mathrm{rels}) \Rightarrow \mathrm{mk}_{\mathrm{rels}}(x) = \mathrm{mk}_{\mathrm{rels}}(y)$$$

Lean4

theorem mk_eq_mk_of_mul_inv_mem {rels : Set (FreeGroup α)} {x y : FreeGroup α} (hx : x * y⁻¹ ∈ rels) :
    mk rels x = mk rels y :=
  eq_of_mul_inv_eq_one <| one_of_mem hx

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