toWord_of_pow — Mathlib

English

For a generator a and n, the word of a^n is the list replicated n times with (a,true).

Русский

Для генератора a и степени n слово a^n представляет собой повторение a n раз с пометкой true.

LaTeX

$$$(\mathrm{of}~a)^n$.toWord = \mathrm{List.replicate}(n, (a, true)).$$$

Lean4

@[to_additive (attr := simp)]
theorem toWord_of_pow (a : α) (n : ℕ) : (of a ^ n).toWord = List.replicate n (a, true) :=
  by
  rw [of, pow_mk, List.flatten_replicate_singleton, toWord]
  exact reduce_replicate _ _

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