iterate_mul — Mathlib

English

Iterating f by the product m · n equals iterating f m on iterates by n: f^{[m n]} = (f^{[m]})^{[n]}.

Русский

Итерация f по произведению m·n равна итерации f по m на итерациях по n: f^{[m n]} = (f^{[m]})^{[n]}.

LaTeX

$$$$f^{[m\cdot n]} = (f^{[m]})^{[n]}$$$$

Lean4

theorem iterate_mul (m : ℕ) : ∀ n, f^[m * n] = f^[m]^[n]
  | 0 => by simp only [Nat.mul_zero, iterate_zero]
  | n + 1 => by simp only [Nat.mul_succ, iterate_one, iterate_add, iterate_mul m n]

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