zpow_iterate — Mathlib

English

For any k ∈ ℤ, the n-th iterate of the map x ↦ x^k equals the map x ↦ x^{k^n}.

Русский

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

LaTeX

$$$\forall k \in \mathbb{Z},\ \forall n \in \mathbb{N},\ (\lambda x:\\ G. x^{k})^{[n]} = (\lambda x:\\ G. x^{k^{n}})$$$

Lean4

@[to_additive (attr := simp)]
theorem zpow_iterate (k : ℤ) : ∀ n : ℕ, (fun x : G ↦ x ^ k)^[n] = (· ^ k ^ n)
  | 0 => by ext; simp [Int.pow_zero]
  | n + 1 => by ext; simp [zpow_iterate, Int.pow_succ', zpow_mul]

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