toWord_eq_nil_iff — Mathlib

English

An element x equals the identity if and only if its word is empty: x.toWord = [] iff x = 1.

Русский

Элемент x равен единице тогда и только тогда, когда его слово пусто: x.toWord = [] тогда и только тогда, когда x = 1.

LaTeX

$$$\forall x : FreeGroup\,\alpha ,\; x.toWord = [] \iff x = 1$$$

Lean4

@[to_additive (attr := simp)]
theorem toWord_eq_nil_iff {x : FreeGroup α} : x.toWord = [] ↔ x = 1 :=
  toWord_injective.eq_iff' toWord_one

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