iterate_comm — Mathlib

English

For any f and any m,n ∈ ℕ, f^[m] and f^[n] commute: f^[m] ∘ f^[n] = f^[n] ∘ f^[m].

Русский

Для любых m,n ∈ ℕ итераты f^[m] и f^[n] коммютируют: f^[m] ∘ f^[n] = f^[n] ∘ f^[m].

LaTeX

$$$$\forall f:\alpha\to\alpha,\forall m,n\in\mathbb{N},\ f^{[m]}\circ f^{[n]} = f^{[n]}\circ f^{[m]}. $$$$

Lean4

theorem iterate_comm (f : α → α) (m n : ℕ) : f^[n]^[m] = f^[m]^[n] :=
  (iterate_mul _ _ _).symm.trans (Eq.trans (by rw [Nat.mul_comm]) (iterate_mul _ _ _))

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