toWord_injective — Mathlib

English

In the free group on α, the word representation is injective: if toWord x = toWord y then x = y.

Русский

Во свободной группе над α отображение в слова инъективно: если toWord x = toWord y, то x = y.

LaTeX

$$$\forall x,y : FreeGroup\,\alpha ,\; toWord\,x = toWord\,y \Rightarrow x = y$$$

Lean4

@[to_additive]
theorem toWord_injective : Function.Injective (toWord : FreeGroup α → List (α × Bool)) := by rintro ⟨L₁⟩ ⟨L₂⟩;
  exact reduce.exact

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