toWord_mul_sublist — Mathlib

English

The word of a product is a sublist of the concatenation of the words: (x * y).toWord <+ x.toWord ++ y.toWord.

Русский

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

LaTeX

$$$(x*y).toWord \;<+\; x.toWord ++ y.toWord$$$

Lean4

@[to_additive]
theorem toWord_mul_sublist (x y : FreeGroup α) : (x * y).toWord <+ x.toWord ++ y.toWord :=
  by
  refine Red.sublist ?_
  have : x * y = FreeGroup.mk (x.toWord ++ y.toWord) := by
    rw [← FreeGroup.mul_mk, FreeGroup.mk_toWord, FreeGroup.mk_toWord]
  rw [this]
  exact FreeGroup.reduce.red

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