pow_iterate — Mathlib

English

In a monoid, for any k, the n-th iterate of the map x ↦ x^k is x ↦ x^{k^n}.

Русский

В моноиде для любого k, n-й итерат карты x ↦ x^k равен отображению x ↦ x^{k^n}.

LaTeX

$$$(\\text{pow\_iterate})\\; (k) : \\forall n, (x \\mapsto x^{k})^{[n]} = (x \\mapsto x^{k^{n}})$$$

Lean4

@[to_additive (attr := simp)]
theorem pow_iterate (k : ℕ) : ∀ n : ℕ, (fun x : M ↦ x ^ k)^[n] = (· ^ k ^ n)
  | 0 => by ext; simp
  | n + 1 => by ext; simp [pow_iterate, Nat.pow_succ', pow_mul]

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