English
If f semiconjugates a binary operation op with itself (i.e., f(op(a,b)) = op(f(a), f(b))) then for every n ∈ ℕ, f^{[n]} semiconjugates op with op: f^{[n]}(op(a,b)) = op(f^{[n]}(a), f^{[n]}(b)).
Русский
Если f полуподчиняет двоичную операцию op самой себе, то для каждого n ∈ ℕ f^{[n]} полуподчиняет op самой себе: f^{[n]}(op(a,b)) = op(f^{[n]}(a), f^{[n]}(b)).
LaTeX
$$$$\forall a,b,\ f(\text{op}(a,b)) = \text{op}(f(a), f(b))\ \Rightarrow\ \forall n\in\mathbb{N},\ f^{[n]}(\text{op}(a,b)) = \text{op}(f^{[n]}(a), f^{[n]}(b)). $$$$
Lean4
theorem iterate {f : α → α} {op : α → α → α} (hf : Semiconj₂ f op op) (n : ℕ) : Semiconj₂ f^[n] op op :=
Nat.recOn n (Semiconj₂.id_left op) fun _ ihn ↦ ihn.comp hf
