toWord_pow — Mathlib

English

The word of a power x^n is the reduction of n copies of the word of x: toWord(x^n) = reduce (List.replicate n x.toWord).flatten.

Русский

Слово степени x^n есть редукция n копий слова x: toWord(x^n) = reduce (List.replicate n x.toWord).flatten.

LaTeX

$$$\forall x : FreeGroup\,\alpha ,\; toWord(x^n) = \mathrm{reduce}(\mathrm{List.replicate}(n, x.toWord).flatten)$$$

Lean4

@[to_additive]
theorem toWord_pow (x : FreeGroup α) (n : ℕ) : toWord (x ^ n) = reduce (List.replicate n x.toWord).flatten :=
  by
  rw [← mk_toWord (x := x)]
  simp

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