coe_pow — Mathlib

English

Let α be a type and f a permutation of α. For every natural number n, the function underlying the permutation f^n is the n-fold iterate of f.

Русский

Пусть α — множество и f : Perm α — перестановка α. Для каждого n ∈ ℕ функция, лежащая в основе f^n, равна n-кратной итерации функции f.

LaTeX

$$$\\\\forall \\\\alpha, (f : \\\\mathrm{Perm} \\\\alpha), (n : \\\\mathbb{N}), \\\\operatorname{toFun}(f^n) = f^{[n]}$$$

Lean4

@[norm_cast]
theorem coe_pow (f : Perm α) (n : ℕ) : ⇑(f ^ n) = f^[n] :=
  rfl

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