mk_eq_mk_of_inv_mul_mem — Mathlib

English

If x^{-1} y is a relator, then mk rels x = mk rels y.

Русский

Если $x^{-1}y$ относится к rels, то образы x и y совпадают в представленной группе.

LaTeX

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

Lean4

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

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