English
Let f be a degree-one circle lift. For every real x and every natural n, the n-th iterate of the translation by x equals the translation by n x.
Русский
Пусть f — подъём степени единицы на Circle. Для любых x ∈ ℝ и любого натурального n н-ая итерация переноса на x равна переносу на n x.
LaTeX
$$$ \forall x \in \mathbb{R}, \forall n \in \mathbb{N}, \left(\mathrm{translate}(\mathrm{Multiplicative.ofAdd}(x))\right)^{[n]} = \mathrm{translate}(\mathrm{Multiplicative.ofAdd}(\uparrow n \cdot x)). $$$
Lean4
@[simp]
theorem translate_iterate (x : ℝ) (n : ℕ) :
(translate (Multiplicative.ofAdd x))^[n] = translate (Multiplicative.ofAdd <| ↑n * x) := by
rw [← coe_pow, ← Units.val_pow_eq_pow_val, translate_pow]