toWord_mul — Mathlib

English

The word of a product equals the reduction of the concatenation of the words: toWord(x*y) = reduce (toWord x ++ toWord y).

Русский

Слово произведения равно редукции конкатенации слов: toWord(x*y) = reduce (toWord x ++ toWord y).

LaTeX

$$$\forall x,y : FreeGroup\,\alpha ,\; toWord(x * y) = \mathrm{reduce}(toWord(x) ++ toWord(y))$$$

Lean4

@[to_additive]
theorem toWord_mul (x y : FreeGroup α) : toWord (x * y) = reduce (toWord x ++ toWord y) :=
  by
  rw [← mk_toWord (x := x), ← mk_toWord (x := y)]
  simp

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